建筑微积分中的“反射”事物？

问题描述

在诸如 Agda ， Idris 或 Haskell 带有类型扩展，有一个 = 类型如下

In languages such as Agda, Idris, or Haskell with type extensions, there is a = type sort of like the following

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

a：〜：b 表示 a 和 b

可以在或（这是基于编程语言的结构演算）？

Can such a type be defined in the calculus of constructions or Morte (which is programming language based on the calculus of construction)?

推荐答案

标准教会编码 a：〜：b 在CoC中是：

The standard Church-encoding of a :~: b in CoC is:

(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

以上内容描述了类型之间的等价关系。对于 terms 之间的平等，：〜：关系必须带有一个附加参数 t :: * ，其中 ab :: t 。

The above formulates equality between types. For equality between terms, the :~: relation must take an additional argument t :: *, where 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

这篇关于建筑微积分中的“反射”事物？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！