And*_*ács 41 agda dependent-type idris
既阿格达和伊德里斯有效地禁止图案类型的值相匹配Type.似乎Agda总是在第一种情况下匹配,而Idris只是抛出一个错误.
那么,为什么typecase是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的更多信息.
pig*_*ker 48
人们认为类型上的模式匹配很糟糕,这真的很奇怪.无论何时我们进行宇宙构造,我们都会对编码类型的数据进行模式匹配.如果你采取Thorsten Altenkirch和我开创的方法(以及我的同志和我开始设计的那些方法),这些类型确实形成一个封闭的宇宙,所以你甚至不需要解决(坦率地说是值得解决的)计算问题打开数据类型以将类型视为数据.如果我们可以直接模式匹配类型,我们就不需要解码函数来将类型代码映射到它们的含义,这最大程度地减少了混乱,并且最多减少了通过关于解码行为的等式定律来证明和强制的需要.功能.我打算用这种方式建立一个无中间人封闭式理论.当然,您需要0级类型居住在1级数据类型中.当你构建一个归纳递归的宇宙层次结构时,这当然是理所当然的.
但是我听到你问,参数化怎么样？
首先,当我尝试编写类型通用代码时,我不想要参数化.不要强迫我参与.
其次,为什么类型应该是我们参与的唯一事物？为什么我们有时不应该在其他东西中参数化,例如,居住在数据类型但我们不希望在运行时没有的完全普通类型索引？真正令人讨厌的是,仅仅因为它们的类型而在规范中起作用的数量被迫存在.
域的类型与它的量化是否应该是参数无关.
让我们(例如,如Bernardy和朋友提出的)一个学科,其中参数/可擦除和非参数/匹配量化是不同的并且都是可用的.然后类型可以是数据,我们仍然可以说出我们的意思.
Tox*_*ris 14
许多人认为类型上的匹配是坏的,因为它打破了类型的参数.
在具有类型参数的语言中,当您看到变量时
f : forall a . a -> a
你马上就会知道很多可能的价值f.直觉:既然f是一个函数,它可以写成:
f x = body
身体需要是类型a,但是a未知,因此唯一可用的类型值a是x.如果语言允许不确定,f也可以循环.但它可以x根据值的值在循环或返回之间做出选择x吗？不,因为a未知,f不知道x要做出决定要调用哪些函数.所以真的只有两种选择:f x = x和f x = f x.这是一个关于f我们通过查看类型的行为的有力定理f.类似推理适用于具有通用量化类型变量的所有类型.
现在,如果f可以在类型上匹配,则可以a实现更多的实现f.所以我们将失去强大的定理.