-ω Ω λ Λ ≡ α β
+<!-- λ Λ ∀ ≡ α β ω Ω -->
+
+This is a long and substantial assignment. On the one hand, it doesn't have any stumpers like we gave you in past weeks, such as defining `pred` or mutual recursion. (Well, we *do* ask you to define `pred` again, but now you understand a basic strategy for doing so, so it's no longer a stumper.) On the other hand, there are a bunch of problems; many of them demand a modest amount of time; and this week you're coming to terms with both System F *and* with OCaml or Haskell. So it's a lot to do.
+
+The upside is that there won't be any new homework assigned this week, and you can take longer to complete this assignment if you need to. As always, don't get stuck on the "More challenging" questions if you find them too hard. Be sure to send us your work even if it's not entirely completed, so we can see where you are. And consult with us (over email or in person on Wednesday) about things you don't understand, especially issues you're having working with OCaml or Haskell, or with translating between System F and them. We will update this homework page with clarifications or explanations that your questions prompt.
+
+We will also be assigning some philosophy of language readings for you to look at before this Thursday's seminar meeting.
+
+Those, and lecture notes from this past week, will be posted shortly.
+
+
## Option / Maybe Types ##
-You've already defined and worked with `map` as a function on lists. Now we're going to work instead with the type OCaml defines like this:
+You've already (in [[assignment1]] and [[/topics/week2 encodings]]) defined and worked with `map` as a function on lists. Now we're going to work instead with the type OCaml defines like this:
type ('a) option = None | Some of 'a
Just y -> ...
}
- Some other tips: In OCaml you write recursive functions using `let rec`, in Haskell you just use `let` (it's already assumed to be recursive). In OCaml when you finish typing something and want the interpreter to parse it, check and display its type, and evaluate it, type `;;` and then return. You may want to review the [[Rosetta pages here]] and also read some of the tutorials we linked to [[for OCaml]] or [[for Haskell]]. [WHERE]
+ Some other tips: In OCaml you write recursive functions using `let rec`, in Haskell you just use `let` (it's already assumed to be recursive). In OCaml when you finish typing something and want the interpreter to parse it, check and display its type, and evaluate it, type `;;` and then return. In Haskell, if you want to display the type of an expression `expr`, type `:t expr` or `:i expr`.
+
+ You may want to review [[Rosetta pages|/rosetta1]] and also read some of the tutorials we linked to for [[/learning OCaml]] or [[/learning Haskell]].
2. Next write a `maybe_map2` function. Its type should be:
data Color = Red | Green | Blue | ... deriving (Eq, Show)
data Color_tree a = Leaf a | Branch (Color_tree a) Color (Color_tree a) deriving (Show)
-These trees always have colors labeling their inner branching nodes, and will have elements of some type 'a labeling their leaves. `(int) color_tree`s will have `int`s there, `(bool) color_tree`s will have `bool`s there, and so on. The `deriving (Eq, Show)` part at the end of the Haskell declarations is boilerplate to tell Haskell you want to be able to compare the colors for equality, and also that you want the Haskell interpreter to display colors and lists to you when they are the result of evaluating an expression.
+These trees always have colors labeling their inner branching nodes, and will have elements of some type `'a` labeling their leaves. `(int) color_tree`s will have `int`s there, `(bool) color_tree`s will have `bool`s there, and so on. The `deriving (Eq, Show)` part at the end of the Haskell declarations is boilerplate to tell Haskell you want to be able to compare the colors for equality, and also that you want the Haskell interpreter to display colors and trees to you when they are the result of evaluating an expression.
Here's how you create an instance of such a tree:
Branch _ c _ -> c == Red
}
-These expressions query whether `t` is a branching `color_tree` (not a leaf) whose root is labeled `Red`.
+These expressions query whether `t` is a branching `color_tree` (that is, not a leaf) whose root is labeled `Red`.
+
+Notice that for equality, you should use single `=` in OCaml and double `==` in Haskell. (Double `==` in OCaml will often give the same results, but it is subtly different in ways we're not yet in a position to explain.) *In*equality is expressed as `<>` in OCaml and `/=` in Haskell.
Choose one of these languages and write the following functions.
-3. Define a function `tree_map` whose type is (as shown by OCaml): `('a -> 'b) -> ('a) color_tree -> ('b) color_tree`. It expects a function `f` and an `('a) color_tree`, and returns a new tree with the same structure and inner branch colors as the original, but with all of its leaves now having had `f` applied to their original value. So for example, `map (2*) t1` would return `t1` with all of its leaf values doubled.
+3. Define a function `tree_map` whose type is (as shown by OCaml): `('a -> 'b) -> ('a) color_tree -> ('b) color_tree`. It expects a function `f` and an `('a) color_tree`, and returns a new tree with the same structure and inner branch colors as the original, but with all of its leaves now having had `f` applied to their original value. So for example, `map (fun x->2*x) t1` would return `t1` with all of its leaf values doubled.
-4. Define a function `tree_foldleft` that accepts an argument `g : 'z -> 'a -> 'z` and a seed value `z : 'z` and a tree `t : ('a) color_tree`, and returns the result of applying `g` first to `z` and `t`'s leftmost leaf, and then applying `g` to *that result* and `t`'s second-leftmost leaf, and so on, all the way across `t`'s fringe. Only the leaf values affect the result; the inner branch colors are ignored.
+4. Define a function `tree_foldleft` that accepts an argument `g : 'z -> 'a -> 'z` and a seed value `z : 'z` and a tree `t : ('a) color_tree`, and returns the result of applying `g` first to `z` and `t`'s leftmost leaf, and then applying `g` to *that result* and `t`'s second-leftmost leaf, and so on, all the way across `t`'s fringe. In our examples, only the leaf values affect the result; the inner branch colors are ignored.
5. How would you use the function defined in problem 4 (the previous problem) to sum up the values labeling the leaves of an `(int) color_tree`?
## More Map2s ##
-Above, you defined `maybe_map2` [WHERE]. Before we encountered `map2` for lists. There are in fact several different approaches to mapping two lists together.
+In question 2 above, you defined `maybe_map2`. [[Before|assignment1]] we encountered `map2` for lists. There are in fact several different approaches to mapping two lists together.
11. One approach is to apply the supplied function to the first element of each list, and then to the second element of each list, and so on, until the lists are exhausted. If the lists are of different lengths, you might stop with the shortest, or you might raise an error. Different implementations make different choices about that. Let's call this function:
* In the `map2` functions, whether for lists or for `option`/`Maybe`s or for trees, and whether done in the "zipping" style or in the "crossing" style, the structure of the result may be a bit different from the structure of the arguments. But the *structure* of the arguments is enough to determine the structure of the result; you don't have to look at the specific list elements or labels on a tree's leaves or nodes to know what the *structure* of the result will be.
-* We can imagine more radical transformations, where the structure of the result *does* depend on what specific elements the original structure(s) had. For example, what if we had to transform a tree by turning every leaf into a subtree that contained all of those leaf's prime factors? Or consider our problem from last week [WHERE] where you converted `[3, 2, 0, 1]` not into `[[3,3,3], [2,2], [], [1]]` --- which still has the same structure, that is length, as the original --- but rather into `[3, 3, 3, 2, 2, 1]` --- which doesn't.
- (Some of you had the idea last week to define this last transformation in Haskell as `[x | x <- [3,2,0,1], y <- [0..(x-1)]]`, which just looks like a cross product, that we counted under the *previous* bullet point. However, in that expression, the second list's structure depends upon the specific values of the elements in the first list. So it's still true, as I said, that you can't specify the structure of the output list without looking at those elements.)
+* We can imagine more radical transformations, where the structure of the result *does* depend on what specific elements the original structure(s) had. For example, what if we had to transform a tree by turning every leaf into a subtree that contained all of those leaf's prime factors? Or consider our problem from [[assignment3]] where you converted `[3, 1, 0, 2]` not into `[[3,3,3], [1], [], [2,2]]` --- which still has the same structure, that is length, as the original --- but rather into `[3, 3, 3, 1, 2, 2]` --- which doesn't.
+ (Some of you had the idea last week to define this last transformation in Haskell as `[x | x <- [3,1,0,2], y <- [0..(x-1)]]`, which just looks like a cross product, that we counted under the *previous* bullet point. However, in that expression, the second list's structure depends upon the specific values of the elements in the first list. So it's still true, as I said, that you can't specify the structure of the output list without looking at those elements.)
These three levels of how radical a transformation you are making to a structure, and the parallels between the transformations to lists, to `option`/`Maybe`s, and to trees, will be ideas we build on in coming weeks.
In Haskell, you'd define it instead like this:
type Identifier = String
- data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________
+ data Lambda_term = Var Identifier | Abstract Identifier _____ | App ________ deriving (Show)
-15. Again, we've left some gaps. Choose one of these languages and fill in the gaps to complete the definition.
+Again, we've left some gaps. (The use of `type` for the first line in Haskell and `data` for the second line is not a typo. The first specifies that `Identifier` will be just a shorthand for an already existing type. The second introduces a new datatype, with its own variant/constructor tags.)
+
+15. Choose one of these languages and fill in the gaps to complete the definition.
16. Write a function `occurs_free` that has the following type:
<!-- These questions are adapted from web materials by Umut Acar. Were at <http://www.mpi-sws.org/~umut/>. Now he's moved to <http://www.umut-acar.org/> and I can't find the page anymore. -->
-
-(For the System F questions, you can either work on paper, or download and compile Pierce's evaluator for system F to test your work [WHERE].)
+(For the System F questions, you can either work on paper, or [download and compile](http://www.cis.upenn.edu/~bcpierce/tapl/) Pierce's evaluator for system F to test your work. Under the "implementations" link on that page, you want to use Pierce's `fullpoly` or the `fullomega` code. The Chapters of Pierce's book *Types and Programming Languages* most relevant to this week's lectures are 22 and 23; though for context we also recommend at least Chapters 8, 9, 11, 20, and 29. We don't expect most of you to follow these recommendations now, or even to be comfortable enough yet with the material to be *able* to. We're providing the pointers as references that some might conceivably pursue now, and others later.)
Let's think about the encodings of booleans, numerals and lists in System F,
times. In the polymorphic encoding above, the result of that iteration can be
any type `α`, as long as your function is of type `α -> α` and you have a base element of type `α`.
-18. Translate these encodings of booleans and Church numbers into OCaml or Haskell, implementing versions of `sysf_bool`, `sysf_true`, `sysf_false`, `sysf_nat`, `sysf_zero`, `sysf_iszero` (this is what we'd earlier write as `zero?`, but you can't use `?`s in function names in OCaml or Haskell), `sysf_succ`, and `sysf_pred`. We include the `sysf_` prefixes so as not to collide with any similarly-named native functions or values in these languages. Keep in mind the capitalization rules. In OCaml, types are written `sysf_bool`, and in Haskell, they are capitalized `Sysf_bool`. In both languages, variant/constructor tags (like `None` or `Some`) are capitalized, and function names start lowercase. But for this problem, you shouldn't need to use any variant/constructor tags. To get you started, here is how to define `sysf_bool` and `sysf_true` in OCaml:
+
+18. Translate these encodings of booleans and Church numbers into OCaml or Haskell, implementing versions of `sysf_bool`, `sysf_true`, `sysf_false`, `sysf_nat`, `sysf_zero`, `sysf_iszero` (this is what we'd earlier write as `zero?`, but you can't use `?`s in function names in OCaml or Haskell), `sysf_succ`, and `sysf_pred`. We include the `sysf_` prefixes so as not to collide with any similarly-named native functions or values in these languages. The point of the exercise is to do these things on your own, so avoid using the built-in OCaml or Haskell booleans and integers.
+
+ Keep in mind the capitalization rules. In OCaml, types are written `sysf_bool`, and in Haskell, they are capitalized `Sysf_bool`. In both languages, variant/constructor tags (like `None` or `Some`) are capitalized, and function names start lowercase. But for this problem, you shouldn't need to use any variant/constructor tags.
+
+ To get you started, here is how to define `sysf_bool` and `sysf_true` in OCaml:
type ('a) sysf_bool = 'a -> 'a -> 'a
let sysf_true : ('a) sysf_bool = fun y n -> y
And here in Haskell:
- type Sysf_bool a = a -> a -> a -- this is a case where Haskell does use `type` instead of `data`
- -- Now, to my mind the natural thing to write here would be:
+ type Sysf_bool a = a -> a -> a -- this is another case where Haskell uses `type` instead of `data`
+ -- To my mind the natural thing to write next would be:
let sysf_true :: Sysf_bool a = \y n -> y
-- But for complicated reasons, that won't work, and you need to do this instead:
let { sysf_true :: Sysf_bool a; sysf_true = \y n -> y }
-- Or this:
let sysf_true = (\y n -> y) :: Sysf_bool a
- Note that in both OCaml and the Haskell code, `sysf_true` can be applied to further arguments directly:
+ Note that in both OCaml and the Haskell code, the generalization `∀'a` on the free type variable `'a` is implicit. If you really want to, you can supply it explicitly in Haskell by saying:
+
+ :set -XExplicitForAll
+ let { sysf_true :: forall a. Sysf_bool a; ... }
+ -- or
+ let { sysf_true :: forall a. a -> a -> a; ... }
+
+ You can't however, put a `forall a.` in the `type Sysf_bool ...` declaration. The reasons for this are too complicated to explain here.
+
+ Note also that `sysf_true` can be applied to further arguments directly:
sysf_true 10 20
You don't do anything like System F's `true [int] 10 20`. The OCaml and Haskell interpreters figure out what type `sysf_true` needs to be specialized to (in this case, to `int`), and do that automatically.
- It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in the lambda library accessible from the main wiki page. [WHERE] The point of the exercise is to do these things on your own, so avoid using the built-in OCaml or Haskell booleans and integers.
+ It's especially useful for you to implement a version of a System F encoding `pred`, starting with one of the (untyped) versions available in [[assignment3 answers]].
type ('a) my_list = Nil | Cons of 'a * 'a my_list
-- Haskell
- data My_list a = Nil | Cons a (My_list a)
+ data My_list a = Nil | Cons a (My_list a) deriving (Show)
-We can encode that type into System F as a right-fold, just as we did in the untyped Lambda Calculus, like this:
+We can encode that type into System F in terms of its right-fold, just as we did in the untyped Lambda Calculus, like this:
list_T ≡ ∀α. (T -> α -> α) -> α -> α
nil_T ≡ Λα. λc:T -> α -> α. λn:α. n
cons_T ≡ λx:T. λxs:list_T. Λα. λc:T -> α -> α. λn:α. c x (xs [α] c n)
-As with `Nat`s, the natural recursion is built into our encoding of the list datatype.
+As with `Nat`s, the natural recursion on the type is built into our encoding of it.
-There is some awkwardness here, because System F doesn't have any parameterized types like OCaml's `('a) list` or Haskell's `[a]`. For those, we need to use a more complex system called System F_ω. System F *can* already define a more general polymorphic list type:
+There is some awkwardness here, because System F doesn't have any parameterized types like OCaml's `('a) list` or Haskell's `[a]`. For those, we need to use a more complex system called System F<sub>ω</sub>. System F *can* already define a more polymorphic list type:
list ≡ ∀β. ∀α. (β -> α -> α) -> α -> α
(S -> T) -> list [S] -> list [T]
-Yet we haven't given ourselves the capacity to talk about `list [S]` and so on as a type. Hence, I'll just use the more clumsy, ad hoc specification of `map`'s type as:
+Yet we haven't given ourselves the capacity to talk about `list [S]` and so on as a type in System F. Hence, I'll just use the more clumsy, ad hoc specification of `map`'s type as:
- FIXME qua
(S -> T) -> list_S -> list_T
<!--
= λf:S -> T. λxs:list. xs [S] [list [T]] (λx:S. λys:list [T]. cons [T] (f x) ys) (nil [T])
-->
-19. Convert this list encoding and the `map` function to OCaml or Haskell. Call it `sysf_list`, `sysf_nil` and so on, to avoid collision with the names for native lists in these languages. (In OCaml and Haskell you *can* say `('a) sysf_list` or `Sysf_list a`.)
+19. Convert this list encoding and the `map` function to OCaml or Haskell. Again, call the type `sysf_list`, and the functions `sysf_nil`, `sysf_cons`, and `sysf_map`, to avoid collision with the names for native lists and functions in these languages. (In OCaml and Haskell you *can* say `('a) sysf_list` or `Sysf_list a`.)
-20. Also give us the type and definition for a `sysf_head` function. Think about what value to give back if its argument is the empty list. Ultimately, we might want to make use of the `option`/`Maybe` technique explored in questions 1--2, but for this assignment, just pick a strategy, no matter how clunky.
+20. Also give us the type and definition for a `sysf_head` function. Think about what value to give back if its argument is the empty list. It might be cleanest to use the `option`/`Maybe` technique explored in questions 1--2, but for this assignment, just pick a strategy, no matter how clunky.
-21. Modify the implementation of the predecessor function [[given in the class notes|topics/week5_system_f]] [WHERE] to implement a `sysf_tail` function for your lists.
+21. Modify your implementation of the predecessor function for Church numerals, above, to implement a `sysf_tail` function for your lists.
Be sure to test your proposals with simple lists. (You'll have to `sysf_cons` up a few sample lists yourself; don't expect OCaml or Haskell to magically translate between their native lists and the ones you've just defined.)
# k 1 true ;;
- : int = 1
- If you can't understand how one term can have several types, recall our discussion in this week's notes [WHERE] of "principal types".
+ If you can't understand how one term can have several types, recall our discussion in this week's notes of "principal types". (WHERE?)
if true then 1 else 2
- evaluates to 1, and
+ evaluates to `1`, and
let b = true in let y = 1 in let n = 2 in
match b with true -> y | false -> n
- also evaluates to 1. Likewise,
+ also evaluates to `1`. Likewise,
if false then 1 else 2
let b = false in let y = 1 in let n = 2 in
match b with true -> y | false -> n
- both evaluate to 2.
+ both evaluate to `2`.
However,
does not terminate. Incidentally, using the shorter `match bool with true -> yes | false -> no` rather than the longer `let b = bool ... in match b with ...` *would* work as we desire. But your assignment is to control the evaluation order *without* using the special evaluation order properties of OCaml's native `if` or of its `match`. That is, you must keep the `let b = ... in match b with ...` structure in your answer, though you are allowed to adjust what `b`, `y`, and `n` get assigned to.
- [[hints/assignment 5 hint 1]] WHERE
+ Here's a [[hint|assignment5 hint1]].