Written Assignment 2

We will work with the lambda calculus with booleans. The syntax of types, values, expressions, and contexts are de ned as follows.

t ::= Bool j t1 ! t2

v ::= x j x : t: e j true j false

e ::= x j x : t: e j e1 e2 j true j false j if e1 then e2 else e3
G ::=  j G; x : t

Note that we have made a small tweak in the syntax for functions (lambdas): each function includes a type annotation describing the type of its input. Also note that we do not have the xed point construct x f: e; do not use this construct in any of your answers. The typing rules are given as follows.


G(x) = t


G; x : t1 ‘ e : t2


G ‘ e1 : t1 ! t2
G ‘ e2 : t1


G ‘ x : t
G ‘ x : t1: e : t1 ! t2



G ‘ e1 e2 : t2








G ‘ e1 : Bool
G ‘ e2 : t
G ‘ e3 : t
G ‘ true : Bool
G ‘ false : Bool

G ‘ if
e1 then e2 else e3 : t

Throughout this assignment, we will work with a call-by-value operational semantics, i.e., we use the small-step rules:



e1 ! e10




e2 ! e20








e
1
e
2
!
e0
e
2

( x : t: e
) e
2
!
( x : t: e ) e0

( x : t: e
) v
!
e
[x
v]





1


1



1
2
1


1

7!

    • Types, Terms, and Contexts (5)

1.1    Fill in the Types

Find a context G and a type t that makes the given program well-typed. For example, for G ‘    x : Bool:y : t,
you could    nd the context G = y : Bool and the type t = Bool ! Bool for the entire expression. Or, you

could take G = y : (Bool ! Bool) and t = Bool ! (Bool ! Bool).

Remember: all free variables in a program must be listed in the context, along with their types. (But variables in the context do not all need to appear in the program.)

    (a) G ‘ if x then x else y : t

    (b) G ‘ x y : t

    (c) G ‘ x : Bool: x : t

    (d) G ‘ x : Bool ! Bool: y x true : t


1

    (e) G ‘ x : Bool ! Bool: y (x true) : t

    (f) G ‘ x : Bool: if y then x else y : t

    (g) G ‘ x : Bool:  y : Bool:  z : Bool: if z then x else y : t

1.2    Fill in the Terms

Find a program e that has the indicated type under the given context. (Note:    is the empty context.)

    (a) ‘ e : Bool ! Bool

    (b) ‘ e : Bool ! Bool ! Bool

    (c) ‘ e : (Bool ! Bool) ! Bool

    (d) ‘ e : (Bool ! Bool ! Bool) ! Bool

    (e) x : Bool; y : Bool ! (Bool ! Bool) ‘ e : Bool ! Bool

    • Inhabitants of a Type (10)

2.1    How Many Programs?

    (a) There are in nitely many closed programs of type Bool, but how many di erent closed values are there of type Bool? List them out.

    (b) How many di erent closed values are there of type Bool ! Bool? List them out. For the purposes
of this exercise, consider two functions f; g to be equal if f x and g x reduce to equal Booleans for

x 2 ftrue; falseg

    (c) More generally, suppose that there are m di erent values of type X and n di erent values of type Y . How many di erent closed values are there of type X ! Y ? You don’t need to list them out. (The function type X ! Y is sometimes written Y X .)

2.2    Programs as Proofs

Suppose we add a few more types to our lambda calculus.

t ::=    j P j Q j R j t1    t2 j t1 + t2

where    and + are the product and sum types we saw in class, and we have corresponding constructors

e ::=    j (e1; e2) j left(e) j right(e)

and destructors:
e ::=    j fst(e) j snd(e) j case e of fleft(x) ! el; right(y) ! erg

Do not assume that there are programs of type P , Q, or R|our language has no constants for these types, like true; false for the booleans. Find a closed program e that has the indicated type under the given context.

    (a) ‘ e : P ! P

    (b) ‘ e : P   Q ! P

    (c) ‘ e : P   Q ! Q  P


2

    (d) ‘ e : P ! (P + Q)

    (e) ‘ e : P   (P ! Q) ! Q

    (f) ‘ e : P ! (Q ! P )

    (g) ‘ e : (P ! Q) (Q ! R) ! (P ! R) Are there programs of the following types?

    (a) ‘ e : P ! Q

    (b) ‘ e : (P + Q) ! P

    (c) ‘ e : (P ! Q) ! P

To get a hint of what is going on here, think of + as \or", as \and", and ! as \implies". What is common across the rst group? What about the second group? (We are not looking for a very formal answer here.)

    • Adding Triples (15)

To get some practice with modeling types, we are going to extend the lambda calculus with booleans with types for triples. Recall that we need to provide three ingredients to model any new type: (1) we need to describe the grammar of the new type, (2) we need to extend the program grammar with things to construct/introduce programs of the new type, and (3) we need to extend the program grammar with things to eliminate/use/take apart/destruct programs of the new type.

There are (at least) two typical ways to incorporate products into a language, di ering in how to elim-inate/destruct products: via projections, or via pattern matching/case analysis. These choices are not mutually exclusive|modern functional languages like Haskell support both operations. To gain a better idea how these features work, you will model both of them for triples.

The    rst part is easiest: we add a new type for triples:

t ::=    j (t1; t2; t3)

You will do the second and third parts.

3.1    Projections

    (a) Extend the program grammar to give a way to construct triples, and also project out from triples. You can pick any reasonable syntax, e.g., (e1; e2; e3) and fst(e); snd(e); thd(e).

    (b) Provide typing rules for each of your new constructs. Hint: there should be four new typing rules in

all: one for the constructor, and one for each of the three projections.

    (c) Provide a small-step operational semantics for your extensions under call-by-value (eager) evaluation: each component of a triple should be rst evaluated all the way to a value before projecting out. Hint: you do this with nine rules: three for the triple, and two for each of the projections.

3.2    Pattern matching

A di erent kind of construct for taking triples apart is pattern matching.

    (a) Extend the program grammar to eliminate triples by pattern matching. You will add one new construct to the language, which should allow the programmer to write (a) the expression we want to take apart,

(b) three variable names, to refer to the three components of the triple, and (c) a body expression that can mention the variable names. Again, you can pick whatever reasonable syntax you like. (Note: take a look at the case analysis construct above. Your case construct will have just a single case, and there is nothing wrong with that.)


3

    (b) Provide one typing rule for your destructor.

    (c) Provide a small-step operational semantics for your extension, still under call-by-value (eager) evalua-tion. Hint: you can do this with ve rules: three for the triple, and two for the pattern match.

As we have discussed in class, Haskell is not a CBV language so the triples that you have added don’t behave exactly like the triples in Haskell (both under projection and under pattern matching). Open up GHCi and see if you nd a program using triples in Haskell that does not behave like the eager triples you added. It is not hard to modify the operational semantics to model lazy triples, which do not evaluate all the way to values when eliminating. There are multiple kinds of lazy triples, which di er in how far they evaluate before eliminating.



















































4