Signed-off-by: Jim Pryor <profjim@jimpryor.net>
---------------
0. Recall that the S combinator is given by \x y z. x z (y z).
---------------
0. Recall that the S combinator is given by \x y z. x z (y z).
- Give two different typings for this function in OCAML.
+ Give two different typings for this function in OCaml.
To get you started, here's one typing for K:
# let k (y:'a) (n:'b) = y;;
To get you started, here's one typing for K:
# let k (y:'a) (n:'b) = y;;
-1. Which of the following expressions is well-typed in OCAML?
+1. Which of the following expressions is well-typed in OCaml?
For those that are, give the type of the expression as a whole.
For those that are not, why not?
For those that are, give the type of the expression as a whole.
For those that are not, why not?
The following expression is an attempt to make explicit the
behavior of `if`-`then`-`else` explored in the previous question.
The idea is to define an `if`-`then`-`else` expression using
The following expression is an attempt to make explicit the
behavior of `if`-`then`-`else` explored in the previous question.
The idea is to define an `if`-`then`-`else` expression using
-other expression types. So assume that "yes" is any OCAML expression,
-and "no" is any other OCAML expression (of the same type as "yes"!),
+other expression types. So assume that "yes" is any OCaml expression,
+and "no" is any other OCaml expression (of the same type as "yes"!),
and that "bool" is any boolean. Then we can try the following:
"if bool then yes else no" should be equivalent to
and that "bool" is any boolean. Then we can try the following:
"if bool then yes else no" should be equivalent to
match x with None -> None | Some n -> f n;;
match x with None -> None | Some n -> f n;;
-Booleans, Church numbers, and Church lists in OCAML
+Booleans, Church numbers, and Church lists in OCaml
---------------------------------------------------
These questions adapted from web materials written by some smart dude named Acar.
The idea is to get booleans, Church numbers, "Church" lists, and
---------------------------------------------------
These questions adapted from web materials written by some smart dude named Acar.
The idea is to get booleans, Church numbers, "Church" lists, and
-binary trees working in OCAML.
+binary trees working in OCaml.
Recall from class System F, or the polymorphic λ-calculus.
Recall from class System F, or the polymorphic λ-calculus.
encoding above, the result of that iteration can be any type α, as long as you have a base element z : α and
a function s : α → α.
encoding above, the result of that iteration can be any type α, as long as you have a base element z : α and
a function s : α → α.
- **Excercise**: get booleans and Church numbers working in OCAML,
- including OCAML versions of bool, true, false, zero, succ, add.
+ **Excercise**: get booleans and Church numbers working in OCaml,
+ including OCaml versions of bool, true, false, zero, succ, add.
Consider the following list type:
Consider the following list type:
map : (σ → τ ) → σ list → τ list
:= λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
map : (σ → τ ) → σ list → τ list
:= λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
- **Excercise** convert this function to OCAML. Also write an `append` function.
+ **Excercise** convert this function to OCaml. Also write an `append` function.
Test with simple lists.
Consider the following simple binary tree type:
Test with simple lists.
Consider the following simple binary tree type:
-OCAML has type inference: the system can often infer what the type of
+OCaml has type inference: the system can often infer what the type of
an expression must be, based on the type of other known expressions.
For instance, if we type
an expression must be, based on the type of other known expressions.
For instance, if we type
# (3) = 3;;
- : bool = true
# (3) = 3;;
- : bool = true
-though OCAML, like many systems, refuses to try to prove whether two
+though OCaml, like many systems, refuses to try to prove whether two
functional objects may be identical:
# (f) = f;;
functional objects may be identical:
# (f) = f;;
-Booleans in OCAML, and simple pattern matching
+Booleans in OCaml, and simple pattern matching
----------------------------------------------
Where we would write `true 1 2` in our pure lambda calculus and expect
----------------------------------------------
Where we would write `true 1 2` in our pure lambda calculus and expect
-it to evaluate to `1`, in OCAML boolean types are not functions
+it to evaluate to `1`, in OCaml boolean types are not functions
(equivalently, are functions that take zero arguments). Selection is
accomplished as follows:
(equivalently, are functions that take zero arguments). Selection is
accomplished as follows:
Unit and thunks
---------------
Unit and thunks
---------------
-All functions in OCAML take exactly one argument. Even this one:
+All functions in OCaml take exactly one argument. Even this one:
# let f x y = x + y;;
# f 2 3;;
# let f x y = x + y;;
# f 2 3;;
After we've given our `f` one argument, it returns a function that is
still waiting for another argument.
After we've given our `f` one argument, it returns a function that is
still waiting for another argument.
-There is a special type in OCAML called `unit`. There is exactly one
+There is a special type in OCaml called `unit`. There is exactly one
object in this type, written `()`. So
# ();;
object in this type, written `()`. So
# ();;
# (fun x -> true) omega;;
- : bool = true
# (fun x -> true) omega;;
- : bool = true
-OCAML declined to try to evaluate the argument before applying the
+OCaml declined to try to evaluate the argument before applying the
functor. But remember that `omega` is a function too, so we can
reverse the order of the arguments:
functor. But remember that `omega` is a function too, so we can
reverse the order of the arguments:
So the integer division operation presupposes that its second argument
(the divisor) is not zero, upon pain of presupposition failure.
So the integer division operation presupposes that its second argument
(the divisor) is not zero, upon pain of presupposition failure.
-Here's what my OCAML interpreter says:
+Here's what my OCaml interpreter says:
# 12/0;;
Exception: Division_by_zero.
So we want to explicitly allow for the possibility that
division will return something other than a number.
# 12/0;;
Exception: Division_by_zero.
So we want to explicitly allow for the possibility that
division will return something other than a number.
-We'll use OCAML's option type, which works like this:
+We'll use OCaml's option type, which works like this:
# type 'a option = None | Some of 'a;;
# None;;
# type 'a option = None | Some of 'a;;
# None;;
Beautiful, just what we need: now we can try to divide by anything we
want, without fear that we're going to trigger any system errors.
Beautiful, just what we need: now we can try to divide by anything we
want, without fear that we're going to trigger any system errors.
-I prefer to line up the `match` alternatives by using OCAML's
+I prefer to line up the `match` alternatives by using OCaml's
built-in tuple type:
<pre>
built-in tuple type:
<pre>
doesn't trigger any presupposition of its own, so it is a shame that
it needs to be adjusted because someone else might make trouble.
doesn't trigger any presupposition of its own, so it is a shame that
it needs to be adjusted because someone else might make trouble.
-But we can automate the adjustment. The standard way in OCAML,
+But we can automate the adjustment. The standard way in OCaml,
Haskell, etc., is to define a `bind` operator (the name `bind` is not
well chosen to resonate with linguists, but what can you do):
Haskell, etc., is to define a `bind` operator (the name `bind` is not
well chosen to resonate with linguists, but what can you do):