È possibile creare una rappresentazione a livello di carattere di ADT generici?

Question

Utilizzando la codifica Church, è possibile rappresentare qualsiasi tipo di dati algebrico arbitrario senza utilizzare il sistema ADT incorporato. Ad esempio, può essere rappresentato Nat (esempio in Idris) come:

-- 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 può essere rappresentato come:

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

E così via. Ora, scrivere quei tipi, costruttori, abbinatori è un compito molto meccanico. La mia domanda è: sarebbe possibile rappresentare un ADT come una specifica a livello di tipo, quindi derivare i tipi stessi (cioè, Nat/Par), nonché i costruttori/distruttori automaticamente da quelle specifiche? Allo stesso modo, potremmo usare queste specifiche per derivare i farmaci generici? Esempio:

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

Per iniziare, ecco qualche codice Idris che rappresenta funtori polinomi:

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 

Ecco un'interpretazione dei dati a base dei loro punti fissi (si veda ad esempio 3.2 in http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf per ulteriori dettagli)

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 

ed ecco un'interpretazione basata rappresentazione Chiesa:

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 

Quindi possiamo fare ad es.

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

ma anche

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

descrizioni indicizzate non sono più duro di funtori polinomi. Considerate questa semplice forma di 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 

π è come Emb seguita da |*|, ma permette al resto della descrizione dipende da un valore di tipo A. _⊕_ è la stessa cosa di |+|. ind è come Rec seguito da |*|, ma riceve anche l'indice di un sottordine futuro. ret termina una descrizione e specifica l'indice di un termine costruito. Ecco un esempio immediato:

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

Il primo costruttore di vec non contiene dati e costruisce un vettore di lunghezza 0, quindi abbiamo messo ret 0. Il secondo costruttore riceve la lunghezza (n) di un subvector, un elemento di tipo A e un subvector e costruisce un vettore di lunghezza suc n.

Costruire punti fissi di descrizioni è simile a quelli di funtori polinomiali troppo

⟦_⟧ : ∀ {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 è semplicemente

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

precedenza era adt Rec t = t, ma ora termini sono indicizzati, quindi t vengono indicizzati troppo (Si chiama B sopra). ind i D riporta l'indice di un sottotema i a cui viene applicato quindi μ D. Pertanto, quando si interpreta il secondo costruttore di vettori, Vec A viene applicato alla lunghezza di un subvettore n (da ind n $ ...), quindi un sottotermino ha tipo Vec A n.

Nel caso finale ret i è necessario che un termine costruito abbia lo stesso indice (i) come previsto (j).

Derivazione eliminatori per tali tipi di dati è leggermente più complicato:

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 

ho elaborato i dettagli elsewhere.

Può essere utilizzato in questo modo:

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) 

Derivazione di uguaglianza decidibile è più prolisso, ma non di più: è solo una questione di che richiede che ogni Set che π riceve ha uguaglianza decidibile. Se tutto il contenuto non ricorsivo del tuo tipo di dati ha uguaglianza decidibile, allora il tuo tipo di dati lo ha pure.

The code.