View Full Document

# Homework

View Full Document
View Full Document

4 views

Unformatted text preview:

6 5 Exercises 131 llist2A 1 A Here we can observe directly if the list is empty or not but not the head or tail which remains unevaluated llist3A 1 A Here we can observe directly if the list is empty or not and the head of the list is non empty However we cannot see the tail llist4A 1 A Here the list is always eager but the elements are lazy This is the same as list A llist5A 1 AN Here we can see if the list is empty or not but we can access only either the head or tail of list but not both infStreamA A This is the type of infinite streams that is lazy lists with no nil constructor Functions such as append map etc can also be written for lazy lists see Exercise 6 15 Other types such as trees of various kinds are also easily represented using similar ideas However the recursive types even without the presence of the fixpoint operator on terms introduce terms which have no normal form In the pure untyped calculus the classical examples of a term with no normal form is x x x x x x which reduces to itself in one step In the our typed calculus linear or intuitionistic this cannot be assigned a type because x is used as an argument to itself However with recursive types and the fold and unfold constructors we can give a type to a version of this term which reduces to itself in two steps x unfold x x Then fold unfold fold fold fold At teach step we applied the only possible reduction and therefore the term can have no normal form An attempt to evaluate this term will also fail resulting in an infinite regression see Exercise 6 16 6 5 Exercises Exercise 6 1 Prove that if M A and M A0 then A A0 Draft of November 8 2001 132 Linear Calculus Exercise 6 2 A function in a functional programming language is called strict if it is guaranteed to use its argument Strictness is an important concept in the implementation of lazy functional languages since a strict function can evaluate its argument eagerly avoiding the overhead of postponing its evaluation and later memoizing its

Unlocking...