如何在Morte上代表任意GADT？

Question

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

Answer 1

您不能获得依赖于数据类型元素的消除器,但您可以定义依赖于数据类型元素索引的消除器.因此,Vectors是可表示的(代码在Agda中):

Nat = (P : Set) -> (P -> P) -> P -> P

zero : Nat
zero = ? P f z -> z

suc : Nat -> Nat
suc = ? n P f z -> f (n P f z) 

plus : Nat -> Nat -> Nat
plus = ? n m P f z -> n P f (m P f z)

Vec = ? (A : Set) (n : Nat) ->
  (P : Nat -> Set) -> (? n -> A -> P n -> P (suc n)) -> P zero -> P n

nil : ? A -> Vec A zero
nil = ? A P f z -> z

cons : ? A n -> A -> Vec A n -> Vec A (suc n)
cons = ? A n x xs P f z -> f n x (xs P f z)

concat : ? A n m -> Vec A n -> Vec A m -> Vec A (plus n m)
concat = ? A n m xs ys P f z -> xs (? n -> P (plus n m)) (? n -> f (plus n m)) (ys P f z)

这些与Church编码列表非常相似,您只需创建一个类型,您可以根据所定义的数据类型的索引进行消除,并更改归纳假设以反映数据类型的构造函数的结构.即你有

cons : ? A n -> A -> Vec A n -> Vec A (suc n)

所以相应的归纳假设是

? n -> A -> P n -> P (suc n)

为了定义没有归纳类型的从属对,你需要非常/ 疯狂的依赖类型(sigma在这里),它允许函数的结果取决于定义的同一个函数.当然,莫特没有这个.