Ist es möglich, eine Typ-Level-Darstellung generischer ADTs zu erstellen?

Question

Mithilfe der Church-Codierung kann jeder beliebige algebraische Datentyp ohne Verwendung des integrierten ADT-Systems dargestellt werden. Zum Beispiel kann Nat dargestellt (in Idris Beispiel) werden als:

-- 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) 

Und so weiter:

-- 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 kann dargestellt werden. Jetzt ist das Schreiben dieser Typen, Konstruktoren, Matcher eine sehr mechanische Aufgabe. Meine Frage ist: Wäre es möglich, eine ADT als Spezifikation auf der Typ-Ebene darzustellen, dann die Typen selbst (d. H. Nat/Par), sowie die Konstruktoren/Destruktoren automatisch aus diesen Spezifikationen abzuleiten? Können wir diese Spezifikationen auch verwenden, um Generika abzuleiten? Beispiel:

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

Sie begonnen haben, hier zu bekommen ist etwas Idris Code, der Polynom functors darstellt:

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 

Hier ist eine datenbasierte Interpretation ihrer Fixpunkte (siehe zB 3.2 in http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf für weitere Details)

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 

und hier ist eine Kirche Darstellung basierte Interpretation:

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 

So können wir z.B.

-- 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) 

aber auch

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

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

Answer 2

Indexed Beschreibungen sind nicht härter als Polynom functors. Betrachten Sie diese einfache Form der propositional descriptions:

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 

π ist wie Emb von |*| gefolgt, aber es ermöglicht es dem Rest der Beschreibung sind abhängig von einem Wert vom Typ A. _⊕_ ist das gleiche wie |+|. ind ist wie Rec gefolgt von |*|, aber es erhält auch den Index eines zukünftigen Unterbegriffs. ret beendet eine Beschreibung und gibt den Index eines konstruierten Terms an. Hier ist ein unmittelbares Beispiel:

vec : Set -> Desc ℕ 
vec A = ret 0 
     ⊕ π ℕ λ n -> π A λ _ -> ind n $ ret (suc n) 

Der erste Konstruktor vec keine Daten enthält und konstruiert einen Vektor der Länge 0, daher setzen wir ret 0. Der zweite Konstruktor erhält die Länge (n) eines Subvektors, ein Element vom Typ A und einen Subvektor und er konstruiert einen Vektor der Länge suc n.

Fixpunkte Beschreibungen Constructing ist ähnlich denen von Polynom functors zu

⟦_⟧ : ∀ {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 einfach war es

Vec : Set -> ℕ -> Set 
Vec A = μ (vec A) 

Zuvor adt Rec t = t, aber jetzt sind Begriffe indiziert, daher t auch indiziert (es heißt B oben). ind i D trägt den Index eines Unterbegriffs i, auf den dann μ D angewendet wird. Wenn also der zweite Konstruktor von Vektoren interpretiert wird, wird Vec A auf die Länge eines Untervektors n (von ind n $ ...) angewendet, daher hat ein Unterbegriff den Typ .

Im letzten ret i Fall ist es erforderlich, dass ein konstruierter Begriff denselben Index hat (i) wie erwartet (j).

Ableitung Eliminatoren für solche Datentypen ist etwas komplizierter:

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 

ich die Details elsewhere erarbeitet.

Es kann wie folgt verwendet werden:

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) 

Ableitung entscheidbar Gleichheit ist ausführlicher, aber nicht härter: es ist nur eine Frage der verlangt, dass jeder Set die π erhält entscheidbar Gleichheit hat. Wenn der gesamte nicht rekursive Inhalt Ihres Datentyps eine entscheidbare Gleichheit aufweist, hat Ihr Datentyp dies ebenfalls.

The code.