《蝉语手册》（语言的主要文档）： https://readonly.link/manuals/gitlab.com/cicada-lang/cicada
《蝉语独白》（一个模仿 Little Book 的小册子）： https://readonly.link/books/github.com/xieyuheng/cicada-monologues
项目主页： https://cicada-lang.org
 | 1 xieyuheng OP 欢迎大家转发给可能会感兴趣的朋友捏～ |
 | 2 iamzuoxinyu 2022-01-15 19:48:35 +08:00 via Android 厉害，虽然我觉得这里的没几个知道什么是 DT 的… |
 | 3 cmdOptionKana 2022-01-15 20:09:55 +08:00 非常优秀！《蝉语独白》简直可以作为编程的启蒙教材，逻辑清晰得不得了，深入浅出，行文流畅且有文采，页面设计也完全符合平面设计的基本原则，牛人啊。 |
 | 4 lance6716 2022-01-15 23:05:16 +08:00 via Android 催更 |
 | 5 xarthur 2022-01-15 23:45:49 +08:00 via iPhone 厉害，之前在推特上看到了。 希望辅助证明的工具越多越好，不过现在看来最大的问题还是学者不大接受这类工具 |
 | 6 GeruzoniAnsasu 2022-01-16 00:27:11 +08:00 我看了半天 「断言」的定义 但全文没有讲到「断言有什么用」，语言中也没有与断言相关的语法 |
 | 7 afutureus 2022-01-16 00:36:10 +08:00 via iPhone 好强 |
| 8 GeruzoniAnsasu 2022-01-16 01:24:08 +08:00 我又反复看了几遍那篇《蝉语独白》 然后又看了半天英文那版文档…… 本来还想直接从单测里找 examples 的但源码里居然没有测试 > We can use check! <exp>: <type>, to make assertion about an expression's type. 看起来「 make assertion 」的含义跟既往理解没什么区别，就是判断一个命题是否正确 但下面的正文里写的意思好像说 「我能为<exp>:<type>下定义」（「我能定义一个<exp>:<type>为真」） 一样。 列举的所有 !check <exp>:<type>我都没看到结论，即断言为真还是假，搞得我一头雾水 -------- 然后在「 built-in types 」这章里塞了 Equal ，本来还以为有什么可等性的定义方法，或者可等类型是什么特殊类型 然而似乎也不是 是说 Equal 这个三元组是一个抽象类型？ 但是又有一句 > If the two elements are actually not the same, we can still use Equal to create a Type, but we can not construct elements of this type …………我就搞不懂了如果「 Equal(X,Y,Z)三元组」这个类型是抽象的，那么去哪，谁来判定 Y 和 Z 是不是相等的？能不能 construct 它的实例到底是怎么判定的？ -------- > If Nat is the most basic datatype, List is the next basic datatype. 我猜原意是「如果说自然数算是最基础的类型，那么 List 可以说是第二基础的」 这个 if 就很没逻辑…… 然后 List( 这个括号里的参数是一个类型对吧，换言之 List(T)是一个泛型，T 作为构造类型的一部分？ 那这样理解的话 Equal()也是一个泛型，List 的参数列表是类型，Equal 里却可以有表达式……为什么？规范是啥…… 然后这一节还似乎想讲讲 list 上的归纳法 我 ctrl+f 了一下没看到 return induction ( 这个 induction 函数是哪讲的就放弃了 我的耐心仅够支撑我研究到这，抱歉…… p.s. 话说启发点是 coq ？文档全文也没看出来如何 prove something ，甚至如何定义公理都没讲明白，更别说推导机制…… |
 | 9 Ultraman 2022-01-16 11:01:30 +08:00 via Android Emmm 哪位老哥用它来证明一下勾股定理让菜鸡如我理解一下？ |
 | 10 wzzzx 2022-01-16 12:13:06 +08:00 有意思 |
 | 11 imKiva 2022-01-16 17:28:26 +08:00 @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 |
| 12 xieyuheng OP |
| 13 xieyuheng OP |
| 14 xieyuheng OP @GeruzoniAnsasu 源码里有非常完备的测试哦。 详情请见这里的 `tests/`： https://github.com/cicada-lang/cicada/tree/master/docs 另外，其中的 `manual/` 和 `articles/` 也算是带有文档的测试，运行测试的时候会跑到的。 |
| 15 xieyuheng OP @GeruzoniAnsasu 感谢你的反馈！我会仔细思考你提到的点，逐步改进我的文档的。 |
| 16 lance6716 2022-01-17 19:16:28 +08:00 博客有 rss 吗 |
| 17 xieyuheng OP |
| 18 xieyuheng OP 加了一个 sponsors 页面 https://cicada-lang.org/sponsors |
Select Language