Curry Howard Isomorphism -> (Leibniz Equality * Programming By Refinement)
Abstract：这文章旨意用Coq介绍一下Leibniz Equality，并慢慢引出Curry Howard Isomorphism。 前置知识：Haskell 首先，一些设置： {-# LANGUAGE MonomorphismRestriction, Rank2Types #-} module Main ( main ) where import Prelude hiding(EQ) main :: IO () main = return () 会给出一定的Haskell代码以辅助理解Coq。 Set Implicit Arguments. Set Universe Polymorphism. 第零行开启Coq中的隐式参数。 第一行开启了Universe Polymorphism，详情见Universes，The Coq Proof Assistant，Girard悖论是什么？ - 雾雨魔理沙的回答 - 知乎。不知道这是啥不会影响你的阅读。 当我们认为两个Type相等的时候，我们在说什么？ Monad的创始人（雾，此Monad非彼Monad，不过玄乎程度有过之而不及）Leibniz给出了一个很优雅的解释：当A=B的时候，如果一个命题为真，把里面的任意A替换成B，依然为真。用更formal的话说， Given any x and y, x = y if and only if, given any predicate P, P(x) if and only if P(y). -Equality (mathematics)...