如何在Morte上代表任意GADT?
Posted
tags:
篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了如何在Morte上代表任意GADT?相关的知识,希望对你有一定的参考价值。
表达正常数据类型(如列表和nat)非常简单,并且有很多示例。但是,翻译GADT的通用程序是什么?将典型类型(如Vector和依赖产品)从Idris转换为Morte的一些示例将非常具有说明性。
您不能获得依赖于数据类型元素的消除器,但您可以定义依赖于数据类型元素索引的消除器。因此,Vector
s是可表示的(代码在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)
为了定义没有归纳类型的从属对,你需要非常/ insanely dependent types(sigma是here),它允许函数的结果取决于定义的同一个函数。当然,莫特没有这个。
可以表示的所有内容都记录在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没有归纳类型。
需要明确的是,通过归纳,我的意思是对于某种类型,可以推导出对应于结构诱导原理的函数。这些是折叠的一般化,其中输出类型可能取决于输入值。对于某些自然数字类型Nat : *
与suc : Nat -> Nat
和zero : 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
,我们只有非依赖性折叠(又名“递归”)而不是可能改变类型的折叠(又称“归纳”)。
是。例如,this answer展示了如何编写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?的主要内容,如果未能解决你的问题,请参考以下文章