• 沒有找到結果。

A Lightweight Implementation of Generics and Dynamics

N/A
N/A
Protected

Academic year: 2022

Share "A Lightweight Implementation of Generics and Dynamics"

Copied!
25
0
0

加載中.... (立即查看全文)

全文

(1)

A Lightweight Implementation of Generics and Dynamics

James Cheney and Ralf Hinze

February 12, 2009

(2)

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?

(3)

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?

(4)

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

(5)

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

(6)

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

(7)

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?

(8)

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 τ = α × β

(9)

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 τ = α × β

(10)

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 :: ∀φ.φ α → φ β}

(11)

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 :: ∀φ.φ α → φ β}

(12)

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 :: ∀φ.φ α → φ β}

(13)

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?

(14)

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

(15)

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

(16)

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

(17)

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

(18)

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?

(19)

Type safe dynamic value (existential types)

data Dynamic = ∀α.Dyn (Rep α) α

unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2) rCast :: ∀τ.Reg τ → Dynamic → τ

(20)

Type safe dynamic value (existential types)

data Dynamic = ∀α.Dyn (Rep α) α

unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2)

rCast :: ∀τ.Reg τ → Dynamic → τ

(21)

Type safe dynamic value (existential types)

data Dynamic = ∀α.Dyn (Rep α) α

unify :: ∀τ1 τ2.Reg τ1→ Rep τ2 → Maybe (τ1 ↔ τ2) rCast :: ∀τ.Reg τ → Dynamic → τ

(22)

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?

(23)

How can we use it?

I Safe type cast without type class

I Passing type representation around (∀ types, functions)

I Storing type representation (∃ types)

(24)

How can we use it?

I Safe type cast without type class

I Passing type representation around (∀ types, functions)

I Storing type representation (∃ types)

(25)

How can we use it?

I Safe type cast without type class

I Passing type representation around (∀ types, functions)

I Storing type representation (∃ types)

參考文獻

相關文件

Abstract In this paper, we consider the smoothing Newton method for solving a type of absolute value equations associated with second order cone (SOCAVE for short), which.. 1

Mathematical theories explain the relations among patterns; functions and maps, operators and morphisms bind one type of pattern to another to yield lasting

• An algorithm is any well-defined computational procedure that takes some value, or set of values, as input and produces some value, or set of values, as output.. • An algorithm is

• A cell array is a data type with indexed data containers called cells, and each cell can contain any type of data. • Cell arrays commonly contain either lists of text

The relationship between these extra type parameters, and the types to which they are associated, is established by parameteriz- ing the interfaces (Java generics, C#, and Eiffel)

• use Chapter 4 to: a) develop ideas of how to differentiate the classroom elements based on student readiness, interest and learning profile; b) use the exemplars as guiding maps to

Microphone and 600 ohm line conduits shall be mechanically and electrically connected to receptacle boxes and electrically grounded to the audio system ground point.. Lines in

this: a Sub-type reference variable pointing to the object itself super: a Base-type reference variable pointing to the object itself. same reference value, different type