标签: morte

在语言,如Agda,Idris或Haskell用类型扩展,有一种=像以下类型排序

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

a :~: b意味着a和b是一样的.

可以在构造计算或Morte(这是基于构造计算的编程语言)中定义这样的类型吗？

我试图通过Morte项目探索和理解建筑微积分的领域.我知道可以在Agda中表示这样的数据类型,但是对于我来说如何在这样的极简主义环境中表示它并不明显.怎么可能这样呢？我的意思是这个数据类型,在Idris中:

data Tree : Nat -> Type -> Type where
    Leaf : a -> Tree Z a
    (::) : Tree k a -> Tree k a -> Tree (S k) a

这是zipWithMorte中几乎有效的定义:

zipWith
  =  ? (u : *)
  -> ? (f : (u -> u -> u))
  -> ? (a : (#List u))
  -> ? (b : (#List u))
  -> ? (List : *)
  -> ? (cons : (u -> List -> List))
  -> ? (nil : List)
  -> ((? (A:*) -> ? (B:*) ->
  (a (B -> List)
    (? (h:u) -> ? (t : (B -> List) -> ? k : B -> (k h t)))
    (? (k:B) …

表达正常的数据类型(如列表和nat)非常简单,并且有很多例子.但是,翻译GADT的通用程序是什么？将典型类型(如Vector和依赖产品)从Idris转换为Morte的一些示例将非常具有说明性.