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

| R_{1} 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

| R_{1} with τ = 1

| ∀α β.R_{+} (Rep α) (Rep β) with τ = α + β

| ∀α β.R_{×} (Rep α) (Rep β) with τ = α × β

### Encoding types as values

data 1 = Unit

data α + β = Inl α | Inr β data α × β = α : × : β

data Rep τ = R_{Int} (τ ↔ 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 τ = R_{Int} (τ ↔ 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 τ = R_{Int} (τ ↔ 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 (R_{Int} ep) t_{1} t_{2} = from ep t_{1} == from ep t_{2}
rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of

(Unit, Unit) → True

rEqual (R_{+} r_{α} r_{β} ep) t_{1} t_{2} = case (from ep t_{1}, from ep t_{2}) 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 (R_{Int} ep) t_{1} t_{2} = from ep t_{1} == from ep t_{2}

rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of (Unit, Unit) → True

rEqual (R_{+} r_{α} r_{β} ep) t_{1} t_{2} = case (from ep t_{1}, from ep t_{2}) 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 (R_{Int} ep) t_{1} t_{2} = from ep t_{1} == from ep t_{2}
rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of

(Unit, Unit) → True

rEqual (R_{+} r_{α} r_{β} ep) t_{1} t_{2} = case (from ep t_{1}, from ep t_{2}) 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 (R_{Int} ep) t_{1} t_{2} = from ep t_{1} == from ep t_{2}
rEqual (R1 ep) t1 t2 = case (from ep t1, from ep t2) of

(Unit, Unit) → True

_{+} r_{α} r_{β} ep) t_{1} t_{2} = case (from ep t_{1}, from ep t_{2}) 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)