Encoding Tuples and Variants in System F

23 Nov 2015

In System F, it’s possible to represent tuple types and variant types without any special syntacic forms. To see the expressive power of System F, let’s first see how pairs can be represented.

Pair X Y = ∀R. (X -> Y -> R) -> R

pair = λX. λY. λx:X. λy:Y. (λR. λp:X->Y->R. p x y)

fst = λX. λY. λp: Pair X Y. p [X] (λx:X. λy:Y. x)

snd = λX. λY. λp: Pair X Y. p [Y] (λx:X. λy:Y. y)

Extend the representation to tuple of any size is straight-forward. Following example is an encoding of tuples of size three.

Tuple3 X Y Z = ∀R. (X -> Y -> Z -> R) -> R

tuple3 = λX. λY. λZ. λx:X. λy:Y. λz:Z. λR. λp:X->Y->Z->R. p x y z

fst = λX. λY. λZ. λp: Tuple3 X Y Z. p [X] (λx:X. λy:Y. λz:Z. x)

snd = λX. λY. λZ. λp: Tuple3 X Y Z. p [Y] (λx:X. λy:Y. λz:Z. y)

thrd = λX. λY. λZ. λp: Tuple3 X Y Z. p [Z] (λx:X. λy:Y. λz:Z. z)

Of course, we could also represent tuples based on the encoding of pairs, e.g. Tuple3 X Y Z = Pair X (Pair Y Z). Cardelli(1992) discovered an encoding of records based on pairs. The idea is to map field labels to natural number indexes, thus record types can be represented by tuple types and record terms by tuple terms.

{T1, T2, ..., Tn} = Pair T1 (Pair T2 ... (Pair Tn Top) ... )

{t1, t2, ..., tn} = pair t1 (pair t2 ... (pair tn top) ... )

t.n = fst (snd (snd ... (snd t) ... )

The usage of Top and top is essential to restore the subtyping relations between record types, as Top is the supertype of any types.

What’s more interesting is the representation of variants. Let’s first see how to represent sum types and then extend it to variants. Following is an encoding of sum types:

Sum X Y = ∀R. (X -> R) -> (Y -> R) -> R

left = λX. λY. λx:X. λR. λl:X->R.  λr:Y->R. l x

right = λX. λY. λy:Y. λR. λl:X->R.  λr:Y->R. r y

match = λX. λY. λt:Sum X Y. λR. λl:X->R.  λr:Y->R. t [R] l r

The encoding above allows us to write following code(type application omitted for brevity):

match (left 5 as (Sum Nat Bool)) (λx:Nat. x) (λx:Bool. 3)

match (right false as (Sum Nat Bool)) (λx:Nat. x) (λx:Bool. 3)

More generally, how can we encode a variant type, such as following?

Temperature :=
  | average Nat
  | range Nat Nat
  | triple Nat Nat Nat

Without much effort, we can generalize the scheme of sum types to represent Temperature as follows:

Temperature = ∀R. (Nat -> R) -> (Nat -> Nat -> R) -> (Nat -> Nat -> Nat -> R) -> R

average = λx:Nat. λR. λa:Nat->R. λb:Nat->Nat->R. λc:Nat->Nat->Nat->R. a x

range = λx:Nat. λy:Nat. λR. λa:Nat->R. λb:Nat->Nat->R. λc:Nat->Nat->Nat->R. b x y

triple = λx:Nat. λy:Nat. λz:Nat. λR. λa:Nat->R. λb:Nat->Nat->R. λc:Nat->Nat->Nat->R. c x y z

match = λt:Temperature. λR. λa:Nat->R. λb:Nat->Nat->R. λc:Nat->Nat->Nat->R. t [R] a b c

Then it’s possible to write following code(type application omitted for clarity):

match (range 5 10) (λx:Nat. x) (λx:Nat. λy:Nat. x + y)  (λx:Nat. λy:Nat. λz:Nat. x + y + z)

It’s also possible to encode existential types in system F. A term \(t\) of the existential type \(\exists X.T\) means \(t\) takes the type \(T\) for some unknown type \(X\). One application of existential type is to model abstract data type(ADT), where the concrete implementation is hidden in the type \(X\).

To create a term of an existential type, we need to specify the quantified type \(X\) explicitly:

{*S, t} as ∃X.T

To use a term of an existential type, we need to unpack the term:

let {X,x}=t1 in t2

It’s important to note that the unpacked type \(X\) can’t appear in the resulting type of \(t_2\).

It turns out that existential types can be encoded in system F as follows(cf. TAPL Chap 24):

∃X.T                 =       ∀Y. (∀X.T -> Y) -> Y.
{*S, t} as ∃X.T      =       λY. λf:(∀X.T -> Y). f [S] t
let {X,x}=t1 in t2   =       t1 [T2] (λX. λx:T11. t2).

A curious mind would naturally ask: how to encode recursive types? The same trick carries over for recursive types. For example, following is a representation of IntList.

IntList  = ∀R. (Int -> R -> R) -> (Unit -> R) -> R

nil = λR. λf:Int->R->R. λg:Unit->R. g unit

cons = λx:Int. λl:IntList. λR. λf:Int->R->R. λg: Unit->R. f x (l [R] f g)

isNil = λl:IntList. l [Bool] (λx:Int. λb:Bool. false) (λ_:Unit. true)

length = λl:IntList. l [Int] (λx:Int. λacc:Int. acc + 1) (λ_:Unit. 0)

fold = λl:IntList. λR. λf:Int->R->R. λg:Unit->R. l [R] f g

Fengyun Liu

Encoding Tuples and Variants in System F