标签: curry-howard

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ? false) -> CoNat

open CoNat public

我定义zero和plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ? iszero n
pred (plus m n) _ with iszero m | inspect iszero m …

通过Curry-Howard同构 Scala Unit对应逻辑真和Nothing逻辑假.逻辑真实被任何东西暗示的事实由一个简单的函数见证,该函数只是抛弃了这个论点:

def toUnit[A](x: A): Unit = { }

是否有一个函数可以证明逻辑错误意味着什么,这是类型的函数Nothing => A？或者是否有一种惯用的方法来构建一个？

人们可以总是这样做

def fromNothing[A](n: Nothing): A = throw new RuntimeException();

但这只是丑陋 - 它没有使用Nothing没有价值的事实.应该有一种方法如何做到没有例外.

前段时间我读到函数类型a -> b对应的关系a ? b,或者是a ? b吗？这对我来说是有道理的,因为如果我们之间有双射(即(a ? b) ? (a -> b, b -> a))两种类型是同构的.同样地,(a = b) ? (a ? b) ? (a ? b).

我知道这不是Curry-Howard-Lambek的对应关系(即类型理论,逻辑和范畴理论之间的对应关系).它是类型理论与其他东西之间的对应关系.我想知道更多关于这种信件的信息.有人能指出我正确的方向吗？

我知道这似乎不是一个编程问题,但它与编程有关,我希望一些函数式程序员能够更多地了解它并指出我正确的方向.

我在Haskell实施了四个De Morgan定律中的三个:

notAandNotB :: (a -> c, b -> c) -> Either a b -> c
notAandNotB (f, g) (Left x)  = f x
notAandNotB (f, g) (Right y) = g y

notAorB :: (Either a b -> c) -> (a -> c, b -> c)
notAorB f = (f . Left, f . Right)

notAorNotB :: Either (a -> c) (b -> c) -> (a, b) -> c
notAorNotB (Left f)  (x, y) = f x
notAorNotB (Right g) …