A Lightweight Implementation of Generics and Dynamics
James Cheney and Ralf Hinze
February 12, 2009
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
Replace dictionary by type representation
I (==) :: ∀α.(Eq α) ⇒ α → α → Bool
I rEqual :: ∀α.Rep α → α → α → Bool
I elem :: ∀α.(Eq α) ⇒ α → [α] → Bool
I Records precisely on which overloaded function elem depends.
I Signature will change if using more overloaded functions.
I rElem :: ∀α.Rep α ⇒ α → [α] → Bool
Replace dictionary by type representation
I (==) :: ∀α.(Eq α) ⇒ α → α → Bool
I rEqual :: ∀α.Rep α → α → α → Bool
I elem :: ∀α.(Eq α) ⇒ α → [α] → Bool
I Records precisely on which overloaded function elem depends.
I Signature will change if using more overloaded functions.
I rElem :: ∀α.Rep α ⇒ α → [α] → Bool
Replace dictionary by type representation
I (==) :: ∀α.(Eq α) ⇒ α → α → Bool
I rEqual :: ∀α.Rep α → α → α → Bool
I elem :: ∀α.(Eq α) ⇒ α → [α] → Bool
I Records precisely on which overloaded function elem depends.
I Signature will change if using more overloaded functions.
I rElem :: ∀α.Rep α ⇒ α → [α] → Bool
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
Encoding types as values
data 1 = Unit
data α + β = Inl α | Inr β data α × β = α : × : β
data Rep τ = RInt with τ = Int
| R1 with τ = 1
| ∀α β.R+ (Rep α) (Rep β) with τ = α + β
| ∀α β.R× (Rep α) (Rep β) with τ = α × β
Encoding types as values
data 1 = Unit
data α + β = Inl α | Inr β data α × β = α : × : β
data Rep τ = RInt with τ = Int
| R1 with τ = 1
| ∀α β.R+ (Rep α) (Rep β) with τ = α + β
| ∀α β.R× (Rep α) (Rep β) with τ = α × β
Encoding types as values
data 1 = Unit
data α + β = Inl α | Inr β data α × β = α : × : β
data Rep τ = RInt (τ ↔ Int)
| R1 (tau ↔ 1)
| ∀α β.R+ (Rep α) (Rep β) (τ ↔ α + β)
| ∀α β.R× (Rep α) (Rep β) (τ ↔ α × β)
data α ↔ β = EP{from :: α → β, to :: β → α}
data α ↔ β = EP{unEP :: ∀φ.φ α → φ β}
Encoding types as values
data 1 = Unit
data α + β = Inl α | Inr β data α × β = α : × : β
data Rep τ = RInt (τ ↔ Int)
| R1 (tau ↔ 1)
| ∀α β.R+ (Rep α) (Rep β) (τ ↔ α + β)
| ∀α β.R× (Rep α) (Rep β) (τ ↔ α × β)
data α ↔ β = EP{from :: α → β, to :: β → α}
data α ↔ β = EP{unEP :: ∀φ.φ α → φ β}
Encoding types as values
data 1 = Unit
data α + β = Inl α | Inr β data α × β = α : × : β
data Rep τ = RInt (τ ↔ Int)
| R1 (tau ↔ 1)
| ∀α β.R+ (Rep α) (Rep β) (τ ↔ α + β)
| ∀α β.R× (Rep α) (Rep β) (τ ↔ α × β)
data α ↔ β = EP{from :: α → β, to :: β → α}
data α ↔ β = EP{unEP :: ∀φ.φ α → φ β}
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
Type case as pattern matching on values
rEqual :: ∀τ.Rep τ → τ → τ → Bool
rEqual (RInt ep) t1 t2 = from ep t1 == from ep t2 rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of
(Unit, Unit) → True
rEqual (R+ rα rβ ep) t1 t2 = case (from ep t1, from ep t2) of (Inl a1, Inl a2) → rEqual rα a1 a2
(Inr b1, Inr b2) → rEqual rβ b1 b2
→ False
Type case as pattern matching on values
rEqual :: ∀τ.Rep τ → τ → τ → Bool
rEqual (RInt ep) t1 t2 = from ep t1 == from ep t2
rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of (Unit, Unit) → True
rEqual (R+ rα rβ ep) t1 t2 = case (from ep t1, from ep t2) of (Inl a1, Inl a2) → rEqual rα a1 a2
(Inr b1, Inr b2) → rEqual rβ b1 b2
→ False
Type case as pattern matching on values
rEqual :: ∀τ.Rep τ → τ → τ → Bool
rEqual (RInt ep) t1 t2 = from ep t1 == from ep t2 rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of
(Unit, Unit) → True
rEqual (R+ rα rβ ep) t1 t2 = case (from ep t1, from ep t2) of (Inl a1, Inl a2) → rEqual rα a1 a2
(Inr b1, Inr b2) → rEqual rβ b1 b2
→ False
Type case as pattern matching on values
rEqual :: ∀τ.Rep τ → τ → τ → Bool
rEqual (RInt ep) t1 t2 = from ep t1 == from ep t2 rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of
(Unit, Unit) → True
rEqual (R+ rα rβ ep) t1 t2 = case (from ep t1, from ep t2) of (Inl a1, Inl a2) → rEqual rα a1 a2
(Inr b1, Inr b2) → rEqual rβ b1 b2
→ False
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
Type safe dynamic value (existential types)
data Dynamic = ∀α.Dyn (Rep α) α
unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2) rCast :: ∀τ.Reg τ → Dynamic → τ
Type safe dynamic value (existential types)
data Dynamic = ∀α.Dyn (Rep α) α
unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2)
rCast :: ∀τ.Reg τ → Dynamic → τ
Type safe dynamic value (existential types)
data Dynamic = ∀α.Dyn (Rep α) α
unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2) rCast :: ∀τ.Reg τ → Dynamic → τ
Outline
What’s their work
Replace dictionary by type representation Encoding types as values
Type case as pattern matching on values Type safe dynamic value (existential types)
How can we use it?
How can we use it?
I Safe type cast without type class
I Passing type representation around (∀ types, functions)
I Storing type representation (∃ types)
How can we use it?
I Safe type cast without type class
I Passing type representation around (∀ types, functions)
I Storing type representation (∃ types)
How can we use it?
I Safe type cast without type class
I Passing type representation around (∀ types, functions)
I Storing type representation (∃ types)