haskell - 如何在 Morte 上表示任意 GADT？

Question

表达普通数据类型(例如列表和 nats)非常简单，并且有很多示例。不过，翻译 GADT 的通用程序是什么？将 Vector 等典型类型和相关产品从 Idris 转换为 Morte 的一些示例非常具有说明性。

Answer 1

您无法获得依赖于数据类型元素的消除器，但您可以定义依赖于数据类型元素索引的消除器。因此，Vector 是可表示的(代码在 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 编码列表非常相似，您只需创建一个类型，根据正在定义的数据类型的索引进行消除，并更改归纳假设以反射(reflect)数据类型构造函数的结构。 IE。你有

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

所以对应的归纳假设是

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

为了定义没有归纳类型的依赖对，您需要非常/insanely dependent types (西格玛是 here )，它允许函数的结果取决于定义的同一函数。当然，Morte 没有这个。