构造微积分中的“Refl”东西？

Question

在 Agda、Idris 或 Haskell 等具有类型扩展的语言中，有一种 = 类型类似于以下

data a :~: b where
  Refl :: a :~: a

a :~: b表示a和b是一样的

calculus of constructions or Morte（基于构造演算的编程语言）可以定义这样的类型吗？

Answer 1

CoC 中 a :~: b 的标准 Church 编码是：

(a :~: b) =
   forall (P :: * -> * -> *).
      (forall c :: *. P c c) ->
      P a b

Refl 正在

Refl a :: a :~: a
Refl a =
   \ (P :: * -> * -> *)
     (h :: forall (c::*). P c c) ->
     h a

以上公式表示类型之间的相等性。对于项之间的相等性，:~: 关系必须采用附加参数 t :: *，其中 a b :: t.

((:~:) t a b) = 
   forall (P :: t -> t -> *).
      (forall c :: t. P c c) ->
      P a b

Refl t a :: (:~:) t a a
Refl t a =
   \ (P :: t -> t -> *)
     (h :: forall (c :: t). P c c) ->
     h a

Answer 2

id : \/a : *. a -> a
id = \a : *. \x : a. x

eqn : \/a : *. a -> a -> *
eqn = \a : *. \x : a. \y : a. \/p : (a -> *). p x -> p y

refl : \/a : *. \/x : a. eqn a x x
refl = \a : *. \x : a. \p : (a -> *). id (p x)

其中 \/ 是 pi 构造函数，\ 是 lambda 构造函数。

我认为Church-Scott Encoding的思想是定义一个类型作为它的淘汰规则，它的构造函数作为它的引入规则。

either 是一个很好的例子：

either : * -> * -> *
either = \a : *. \b : *. \/r : *. (a -> r) -> (b -> r) -> r 

left : \/a : *. \/b : *. a -> either a b
left = \a : *. \b : *. \x : a. \r : *. \left1 : (a -> r). \right1 : (b -> r). left1 x

right : \/a : *. \/b : *. b -> either a b
right = \a : *. \b : *. \y : b. \r : *. \left1 : (a -> r). \right1 : (b -> r). right1 y

either定义为析取消元规则

按此思路，eqn a x y必须定义为利布尼兹法则\/p : (a -> *). p x -> p y，因为方程的消去法则就是利布尼兹法则

+) 1 != 0 的证明：

bottom : *
bottom = \/r : *. r

nat : *
nat = \/r : *. r -> (r -> r) -> r

zero : nat
zero = \r : *. \z : r. \s : (r -> r). z

succ : nat -> nat
succ = \n : nat. \r : *. \z : r. \s : (r -> r). s (n r z s)

id : \/a : *. a -> a
id = \a : *. \x : a. x

eqn : \/a : *. a -> a -> *
eqn = \a : *. \x : a. \y : a. \/p : (a -> *). p x -> p y

refl : \/a : *. \/x : a. eqn a x x
refl = \a : *. \x : a. \p : (a -> *). id (p x)

goal : eqn nat (succ zero) zero -> bottom
goal = \one_is_zero : (\/p : (nat -> *). p (succ zero) -> p zero). \r : *. one_is_zero (\n : nat. n * r (\a : *. r -> a)) (id r)

构造微积分中的“Refl”东西？

`Refl` thing in Calculus of Constructions?

haskell

functional-programming

equality

dependent-type

morte