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:È possibile creare una rappresentazione a livello di carattere di ADT generici?
-- 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
Si noti che, per quel che ne so, queste codifiche ecclesiastiche mancano di eliminazioni dipendenti. Per esempio. se 'Bool = (A: Type) -> A -> A -> A', e' tru, fls' sono definiti di conseguenza, non puoi provare '(b: Bool) -> (b = tru \/b = fls) ', mentre potevi con tipi induttivi. – chi
È possibile farlo per un sistema di tipo molto più espressivo: tipi completi dipendenti + famiglie induttive. Derivato 'Nat' quindi è un eliminatore' Nat = (P: Nat -> Tipo) -> (per tutti n Pn -> P (succ n)) -> P 0 -> forall n. P n'. Ho scritto un [post di blog] (http://effectfully.blogspot.com/2016/06/deriving-eliminators-of-described-data.html) a riguardo. 'EqType' è [derivable] (https://github.com/effectfully/Generic/blob/master/Property/Eq.agda) (un [esempio] (https://github.com/effectfully/Generic/blob /master/Examples/Eq.agda)). Quanti tipi vuoi coprire? Solo i tipi di sistema F e nessun GADT? – user3237465
@chi: in effetti, questa sembra essere una fonte che conferma la tua affermazione: [L'induzione non è derivabile nella teoria del tipo dipendente secondo ordine] (https://scholar.google.com.sg/scholar?cluster=4467817914024141350&hl=it&as_sdt=0 , 5) – Cactus