是否可以创建通用ADT的类型级表示？

Question

使用Church编码,可以在不使用内置ADT系统的情况下表示任意代数数据类型.例如,Nat可以表示(例如在Idris中):

-- Original type

data Nat : Type where
    natSucc : Nat -> Nat
    natZero : Nat

-- Lambda encoded representation

Nat : Type
Nat = (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat

natSucc : Nat -> Nat
natSucc pred n succ zero = succ (pred n succ zero)

natZero : Nat
natZero n succ zero = zero

Pair 可以表示为:

-- Original type
data Pair_ : (a : Type) -> (b : Type) -> Type where
    mkPair_ : (x:a) -> (y:b) -> Pair_ a b

-- Lambda encoded representation

Par : Type -> Type -> Type
Par a b = (t:Type) -> (a -> b -> t) -> t

pair : (ta : Type) -> (tb : Type) -> (a:ta) -> (b:tb) -> Par ta tb
pair ta tb a b k t = t a b

fst : (ta:Type) -> (tb:Type) -> Par ta tb -> ta
fst ta tb pair = pair ta (\ a, b => a)

snd : (ta:Type) -> (tb:Type) -> Par ta tb -> tb
snd ta tb pair = pair tb (\ a, b => b)

等等.现在,编写这些类型,构造函数,匹配器是一项非常机械的任务.我的问题是:是否可以将ADT表示为类型级别的规范,然后从这些规范中自动派生类型本身(即Nat/ Par)以及构造函数/析构函数？同样,我们可以使用这些规范来推导泛型吗？例:

NAT : ADT
NAT = ... some type level expression ...

Nat : Type
Nat = DeriveType NAT

natSucc : ConstructorType 0 NAT
natSucc = Constructor 0 NAT

natZero : ConstructorType 1 NAT
natZero = Constructor 1 NAT

natEq : EqType NAT
natEq = Eq NAT

natShow : ShowType NAT
natShow = Show NAT

... and so on

Answer 1

索引描述并不比多项式仿函数更难.考虑这种简单形式的命题描述:

data Desc (I : Set) : Set? where
  ret : I -> Desc I
  ?   : (A : Set) -> (A -> Desc I) -> Desc I
  _?_ : Desc I -> Desc I -> Desc I
  ind : I -> Desc I -> Desc I

?就像Emb后面一样|*|,但它允许描述的其余部分取决于类型的值A._?_是一样的|+|.ind就像Rec后面一样|*|,但它也接收未来子项的索引.ret完成描述并指定构造术语的索引.这是一个直接的例子:

vec : Set -> Desc ?
vec A = ret 0
      ? ? ? ? n -> ? A ? _ -> ind n $ ret (suc n)

第一个构造函数vec不包含任何数据并构造一个长度向量0,因此我们放置ret 0.第二个构造函数接收子n向量的length(),类型的某个元素A和子向量,并构造一个length的向量suc n.

构造固定的描述点也类似于多项式算子的那些

?_? : ? {I} -> Desc I -> (I -> Set) -> I -> Set
? ret i   ? B j = i ? j
? ? A D   ? B j = ? ? x -> ? D x ? B j
? D ? E   ? B j = ? D ? B j ? ? E ? B j
? ind i D ? B j = B i × ? D ? B j

data ? {I} (D : Desc I) j : Set where
  node : ? D ? (? D) j -> ? D j

Vec 很简单

Vec : Set -> ? -> Set
Vec A = ? (vec A)

以前它是adt Rec t = t,但现在条款被索引,因此也t被索引(它在B上面被称为).ind i D携带subterm的索引i,其? D被施加然后.因此,当解释向量的第二个构造函数时,Vec A将应用于子向量n(from ind n $ ...)的长度,因此子项具有类型Vec A n.

在最后ret i一种情况下,要求构造的术语具有与i预期(j)相同的索引().

为这些数据类型派生消除器稍微复杂一些:

Elim : ? {I B} -> (? {i} -> B i -> Set) -> (D : Desc I) -> (? {j} -> ? D ? B j -> B j) -> Set
Elim C (ret i)   k = C (k refl)
Elim C (? A D)   k = ? x -> Elim C (D x) (k ? _,_ x)
Elim C (D ? E)   k = Elim C D (k ? inj?) × Elim C E (k ? inj?)
Elim C (ind i D) k = ? {y} -> C y -> Elim C D (k ? _,_ y)

module _ {I} {D? : Desc I} (P : ? {j} -> ? D? j -> Set) (f? : Elim P D? node) where
  mutual
    elimSem : ? {j}
            -> (D : Desc I) {k : ? {j} -> ? D ? (? D?) j -> ? D? j}
            -> Elim P D k
            -> (e : ? D ? (? D?) j)
            -> P (k e)
    elimSem (ret i)    z       refl    = z
    elimSem (? A D)    f      (x , e)  = elimSem (D x) (f  x) e
    elimSem (D ? E)   (f , g) (inj? x) = elimSem D f x
    elimSem (D ? E)   (f , g) (inj? y) = elimSem E g y
    elimSem (ind i D)  f      (d , e)  = elimSem D (f (elim d)) e

    elim : ? {j} -> (d : ? D? j) -> P d
    elim (node e) = elimSem D? f? e

我在其他地方详细阐述了细节.

它可以像这样使用:

elimVec : ? {n A}
        -> (P : ? {n} -> Vec A n -> Set)
        -> (? {n} x {xs : Vec A n} -> P xs -> P (x ? xs))
        -> P []
        -> (xs : Vec A n)
        -> P xs
elimVec P f z = elim P (z , ? _ -> f)

派生可判定的平等是更冗长,但不是很难:它只是一个要求,每一个的事Set,其?接收具有可判定的平等.如果数据类型的所有非递归内容具有可判定的相等性,那么您的数据类型也具有可判定的相等性.

代码.

Answer 2

为了帮助您入门，这里有一些表示多项式函子的 Idris 代码：

infix 10 |+|
infix 10 |*|

data Functor : Type where
  Rec : Functor
  Emb : Type -> Functor
  (|+|) : Functor -> Functor -> Functor
  (|*|) : Functor -> Functor -> Functor

LIST : Type -> Functor
LIST a = Emb Unit |+| (Emb a |*| Rec)

TUPLE2 : Type -> Type -> Functor
TUPLE2 a b = Emb a |*| Emb b

NAT : Functor
NAT = Rec |+| Emb Unit

这是对其固定点的基于数据的解释（有关更多详细信息，请参见http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf中的 3.2）

adt : Functor -> Type -> Type
adt Rec t = t
adt (Emb a) _ = a
adt (f |+| g) t = Either (adt f t) (adt g t)
adt (f |*| g) t = (adt f t, adt g t)

data Mu : (F : Functor) -> Type where
  Fix : {F : Functor} -> adt F (Mu F) -> Mu F

这是基于教会代表的解释：

Church : Functor -> Type
Church f = (t : Type) -> go f t t
  where
    go : Functor -> Type -> (Type -> Type)
    go Rec t = \r => t -> r
    go (Emb a) t = \r => a -> r
    go (f |+| g) t = \r => go f t r -> go g t r -> r
    go (f |*| g) t = go f t . go g t

所以我们可以做例如

-- Need the prime ticks because otherwise clashes with Nat, zero, succ from the Prelude...
Nat' : Type
Nat' = Mu NAT

zero' : Nat'
zero' = Fix (Right ())

succ' : Nat' -> Nat'
succ' n = Fix (Left n)

但是也

zeroC : Church NAT
zeroC n succ zero = (zero ())

succC : Church NAT -> Church NAT
succC pred n succ zero = succ (pred n succ zero)