TAPL exercises

Writing down answers from the Types and Programming Languages book.

5.2.1

{- logical or -}
or = λa. λb. a tru b

{-
| a   | b   | or a b            |
|-----+-----+-------------------|
| tru | tru | tru tru tru = tru |
| tru | fls | tru tru fls = tru |
| fls | tru | fls tru tru = tru |
| fls | fls | fls tru fls = fls |
-}

{- logical and -}
and = λa. λb. a b fls

{-
| a   | b   | and a b           |
|-----+-----+-------------------|
| tru | tru | tru tru fls = tru |
| tru | fls | tru fls fls = fls |
| fls | tru | fls tru fls = fls |
| fls | fls | fls fls fls = fls |
-}

{- logical not -}
and = λa. a fls tru

{-
| a   | not a             |
|-----+-------------------|
| tru | tru fls tru = fls |
| fls | fls fls tru = tru |
-}

6.1.1

Named term (question) de-Bruijn index term (answer)
λs. λz. z; λ.λ. 0;
λs. λz. s (s z); λ.λ. 1 (1 0);
λm. λn. λs. λz. m s (n z s); λ.λ.λ.λ. 3 1 (2 0 1);
λf. (λx. f (λy. (x x) y)) (λx. f (λy. (x x) y)); λ. (λ. 1 (λ. (1 1) 0)) (λ. 1 (λ. (1 1) 0));
(λx. (λx. x)) (λx. x); (λ. (λ. 0)) (λ. 0);

DONE 6.2.2

  1. ↑² (λ.λ. 1 (0 2))
    • ↑²₀ (λ.λ. 1 (0 2))
    • λ. ↑²₁(λ. 1 (0 2))
    • λ. λ. ↑²₂(1 (0 2))
    • λ. λ. (↑²₂ 1) (↑²₂ (0 2))
    • λ. λ. 1 (↑²₂ (0 2))
    • λ. λ. 1 ((↑²₂ 0) (↑²₂ 2))
    • λ. λ. 1 (0 4)
  2. ↑² (λ. 0 1 (λ. 0 1 2))
    • ↑²₀ (λ. 0 1 (λ. 0 1 2))
    • λ. ↑²₁ (0 1 (λ. 0 1 2))
    • λ. [↑²₁ (0 1)] [↑²₁ ((λ. 0 1 2))]
    • λ. (0 3) [↑²₁ ((λ. 0 1 2))]
    • λ. (0 3) (λ. [↑²₂ (0 1 2)])
    • λ. (0 3) (λ. (0 1 4))

13.1.1

Question

Draw a similar diagram showing the effects of evaluating the expressions a = {ref 0, ref 0} and b = (λx: Ref Nat. {x, x}) (ref 0).

Answer

a = {ref 0, ref 0}


a = { _, _}
      |  |
      ↓  ↓
    +---+---+
    |   |   |
    +---+---+

where the two elements of the record point to different memory locations.

And

b = (λx: Ref Nat. {x, x}) (ref 0)


b = { _, _}
      |  |
      ↓  ↓
      ↘  ↙
        ↓ 
      +---+
      |   |
      +---+

where both elements of the record point to the same memory location.

15.2.1

Question

Draw a derivation showing that {x:Nat, y:Nat, z:Nat} is a subtype of {y:Nat}.

Answer

{x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat, z:Nat} (S-Refl)
{x:Nat, y:Nat, z:Nat} <: {x:Nat, y:Nat} (S-RcdWidth, k=1)
{x:Nat, y:Nat, z:Nat} <: {y:Nat, x:Nat} (S-RcdPerm)
{x:Nat, y:Nat, z:Nat} <: {y:Nat} (S-RcdWidth, k=1)

DONE 22.2.3

λx:X. λy:Y. λz:Z. (x z) (y z)

Type of bound variables are like:

x:_ -> _ -> _
y:_ -> _
z:_

y has to return something which x z can accept

x:A -> X -> _
y:A -> X
z:A

Rest can be anything.

x:A -> X -> B
y:A -> X
z:A

Some possible type unifiers:

DONE 22.4.3