标签: injective-function

以下所有工作:

{-# LANGUAGE TypeFamilies #-}

type family TF a
type instance TF Int = String
type instance TF Bool = Char

data family DF a
data instance DF Int = DFInt String
data instance DF Bool = DFBool Char

type family CTF a where
  CTF Int = String
  CTF Bool = Char
  CTF a = Double     -- Overlap OK!

......但这不是(截至GHC-8.2):

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double …

根据这个课程,所有构造函数(对于归纳类型)都是单射的和不相交的:

...类似的原则适用于所有归纳定义的类型:所有构造函数都是单射的,并且由不同构造函数构建的值永远不会相等.对于列表,cons构造函数是单射的,nil与每个非空列表不同.对于布尔,真假都是不平等的.

(以及inversion基于这种假设的策略)

我只是想知道我们怎么知道这个假设成立了？

我们怎么知道,例如,我们不能基于定义自然数

1)一个继承者,也许是像这样的"双"构造函数:

Inductive num: Type :=
   | O : num
   | S : num -> num
   | D : num -> num.

和

2)一些plus功能,以便2通过两个不同的序列/路由构造函数可以达到一个数字,S (S O)并且D (S O)？

Coq的机制是什么,以确保上述内容永远不会发生？

PS我不是建议上面的num例子是可能的.我只是想知道是什么让它变得不可能.

谢谢

Idris语言教程有一个简单易懂的依赖类型概念示例:http: //docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types

这是代码:

isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False = List Int

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Int
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

我决定花更多的时间在这个例子上.让我困扰的sum是我需要明确地将single : Bool值传递给函数.我不想这样做,我希望编译器猜测这个布尔值应该是什么.因此,我只传递Int或List Int向 …