如何在 Morte 上表示任意 GADT？

Question

表达正常的数据类型，如列表和 nats 很简单，周围有很多例子。不过，翻译 GADT 的一般程序是什么？一些将典型类型（例如 Vector 和从属产品）从 Idris 转换为 Morte 的示例非常具有说明性。

Answer 1

所有可表示的内容都记录在 Morte tutorial 中。 GADT 和（更普遍的）索引类型不存在，事实上它们是不可能的。

（编辑：GADT 实际上可以表示；请参阅 user3237465 的其他答案）

Vector 类型本身可以编码，但它的值用处不大。 Vector n A 是 n 嵌套对 A-s:

Unit   = \(A : *) -> A -> A
Pair   = \(A B : *) -> (P : *) -> (A -> B -> P) -> P
Nat    = (N : *) -> (N -> N) -> N -> N
Vector = \(n : Nat)(A : *) -> n * (\(t : *) -> Pair A t) Unit

但是为 Vector n A 编写任何有用的函数都需要对其 n 长度进行归纳，但是 Morte 没有归纳类型。

需要说明的是，我所说的归纳是指对于某种类型，对应于结构归纳原理的函数是可推导的。这些是折叠的概括，其中输出类型可能取决于输入值。对于某些具有 suc : Nat -> Nat 和 zero : Nat 的自然数类型 Nat : * 归纳具有以下类型：

natInd : 
      (N : Nat -> *)                   -- a predicate,
   -> ((n : Nat) -> N n -> N (suc n))  -- if it's preserved by suc
   -> N zero                           -- and holds for zero,
   -> (n : Nat) -> N n                 -- holds for every Nat

折叠Vector时，类型随长度变化（因为前者依赖于后者）。然而，对于 Church Nat，我们只有非依赖折叠（aka "recursion"）而不是可能的类型改变折叠（aka "induction"）。

Answer 2

您无法获得依赖于数据类型元素的消除器，但您可以定义依赖于数据类型元素索引的消除器。因此，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-encoded 列表非常相似，您只需创建一个类型，然后根据定义的数据类型的索引将其消除，并更改归纳假设以反映数据构造函数的结构类型。 IE。你有

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

所以对应的归纳假设是

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

为了定义没有归纳类型的依赖对，你需要非常/insanely dependent types (sigmas are here)，它允许函数的结果依赖于被定义的同一个函数。莫尔特当然没有这个。

Answer 3

是的。例如，显示了如何编写 Refl 类型。

假设我们要构建一个简单的 DSL。 Ti 的操作方法如下：

Expr t = forall (E :: * -> *). forall
    (IntLit :: Integer -> E Integer),
    (IntVar :: Char -> E Integer),
    (Add :: E Integer -> E Integer -> E Integer),
    (Mult :: E Integer -> E Integer -> E Integer),
    (Neg :: E Integer -> E Integer),
    (IntEq :: E Integer -> E Integer -> E Bool),
    (Lt :: E Integer -> E Integer -> E Bool),
    (And :: E Bool -> E Bool -> E Bool),
    (Or :: E Bool -> E Bool -> E Bool),
    (Not :: E Bool -> E Bool),
    (If :: (forall x :: *. E Bool -> E x -> E x -> E x)).
    E t

如何在 Morte 上表示任意 GADT？

How to represent arbitrary GADTs on Morte?

haskell

gadt

idris

morte