@
GeruzoniAnsasu #8
> 列举的所有 !check <exp>:<type>我都没看到结论,即断言为真还是假,搞得我一头雾水
这个 check! 的意思是要求编译器进行类型检查,即 check <exp> against <type>,如果 <exp> 确实是 <type> 的 inhabitant (或者说 <exp> 具有 <type> 类型),则检查通过。否则应该产生一个类型错误。
> 本来还以为有什么可等性的定义方法,或者可等类型是什么特殊类型。然而似乎也不是。是说 Equal 这个三元组是一个抽象类型?我就搞不懂了如果「 Equal(X,Y,Z)三元组」
「相等类型」相关的内容非常复杂,与这门语言选择的类型论有关。我太菜了,可能回答不了这个问题。
> 那这样理解的话 Equal()也是一个泛型,List 的参数列表是类型,Equal 里却可以有表达式……为什么?规范是啥……
这是 dependent type (依值类型),即类型可以依赖值。在 DT 的语言中,类型和值并没有什么不同。
> ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了
这个 induction 可以视为「模式匹配」,是编译器内建的操作(比如 rust 的 match ),是一种对归纳数据类型(比如 Nat 类型)归纳证明的一种方法。你可以理解为「分类讨论」。
> 文档全文也没看出来如何 prove something ,甚至如何定义公理都没讲明白
文档这一部分:
https://readonly.link/manuals/gitlab.com/cicada-lang/cicada/-/datatype/01.1-proving-theorems-about-nat.md以加法交换律为例展示了证明,即:add_commute(x: Nat, y: Nat,): Equal(Nat, add(x, y), add(y, x))
这个函数签名的意思是:对于任意两个自然数 x y ,都有 x + y = y + x
而这个函数的 body 就是对这个命题的证明。
关于这个问题,更多可以参考:
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence