依值类型下模式匹配的完全性检查
那一天, 类型论说:"我来事了", 自那时起, 我便知道 coverage check
的重要性
近日写完了 ShiTT
的 coverage check, 我已经几乎可以声称我实现了一个定理证明器了,
虽然有些许 bug. 但瑕不掩瑕, 我觉得我还是很棒的.
Coverage check 是确保模式匹配安全的重要机制, 确保你的模式不会侧漏.
虽然我觉得这篇文章的有效读者(如果他们存
依值类型下的归纳类型和模式匹配的实现笔记
依值类型下的归纳类型和模式匹配的实现笔记
完整源码见此
最近在试图实现一个支持模式匹配的依值类型系统, 期间踩了些许坑,
重写了一次才把代码搞到勉强能看的地步(但是大概还需要再重写一次).
我意识到这方面几乎没有中文内容, 于是打算写一篇笔记来记录一下.
归纳类型和模式匹配主要参考的 Ulf Norell 的 Towards a practical
programming langua
用Haskell实现一些简单的类型系统的酷酷方法
总所周知, 类型论的操作语义可以用一堆写成大横线的规则来表示,
这篇文章会教你如何把大横线转换成haskell代码.
先从STLC开始, 首先是两颗语法树, 一个代表项, 一个代表类型,
12345678910type Id = Stringdata Type = Int | Type :-> Type deriving (Show, Eq)data Term = Lam Id Ty
如何形式化验证一场技术面试
完整代码可见https://github.com/KonjacSource/NQueens.
标题捏自https://aphyr.com/posts/342-typing-the-technical-interview,
这里有一篇中文翻译https://zhuanlan.zhihu.com/p/84634204, 不会写小作文,
所以只偷个名字😢.
本文意图展示一下如何确保正确性地编写
写给一般计算机人的Lean4安利
本文主要给有计算机背景(起码懂一门强类型编程语言,
如果读者懂函数式编程或者 Rust 就更好了)的人介绍一下 Lean4
(作为一个编程语言而不是证明助手).
环境配置不在本文介绍范围内, 请参考https://lean-lang.org/lean4/doc/setup.html或者参考这里https://zhuanlan.zhihu.com/p/656770107.
另外由于 Mark