We have programmed several partial functions – functions that are only defined over part of their input (see Section Partial functions – a reminder in the lecture notes of Week 03). For example, the factorial function and the fibonacci function are only defined over non-negative integers. We implemented these partial functions as impure functions in OCaml, using assert:
let fac n =
(* fac : int -> int *)
let () = assert (n >= 0) in
let rec loop n a =
if n = 0
then a
else loop (pred n) (n * a)
in loop n 1;;
let fib n =
(* fib : int -> int *)
let () = assert (n >= 0) in
let rec visit n =
if n = 0
then (0, 1)
else let n' = n - 1
in let (fib_n', fib_n) = visit n'
in (fib_n, fib_n' + fib_n)
in let (fib_n, fib_succ_n) = visit n
in fib_n;;
Applying them to a negative integer raises an error.
OCaml’s type system does not help us here because it only offers the type of integers, not the type of natural numbers.
But what if it could?
OCaml offers a polymorphic type construct called an “option type” to account for such partial functions and implement them as total functions (see Section Total functions – a reminder in the lecture notes of Week 03). The option type has two constructors, None, which is nullary (i.e., that takes no arguments), and Some, which is unary (i.e., that takes one argument). This type is predefined in OCaml, and its typing rule reads as follows, where G stands for <type_environment>, e stands for <expression>, and t stands for <type>:
| None | ||
| G |- None : 'a option | ||
| Some | G |- e : t | |
| G |- Some e : t option |
So applying the constructor Some to a value of type t yields a value of type t option. For example,
the expression Some 0 has type int option – the type of an optional integer – since the expression 0 has type int:
# Some 0;;
- : int option = Some 0
#
the expression Some true has type bool option – the type of an optional Boolean – since the expression true has type bool:
# Some true;;
- : bool option = Some true
#
As for the expression None, it has a polymorphic type – the type of an optional polymorphic value:
# None;;
- : 'a option = None
#
Using the option type, we can implement total versions of the factorial and fibonacci functions as pure OCaml functions:
let total_fac n =
(* total_fac : int -> int option *)
if n < 0
then None
else Some (fac n);;
let total_fib n =
(* total_fib : int -> int option *)
if n < 0
then None
else Some (fib n);;
Whereas fac has type int -> int, total_fac has type int -> int option, and it is well defined on all integers, whether negative, zero, or positive. (“Well defined” means that applying fac to any integer will return a value.)
Implement a function that returns the first element of a list, if any:
let test_list_first_int candidate =
let b0 = (candidate [] = None)
and b1 = (candidate [1] = Some 1)
and b2 = (candidate [1; 2] = Some 1)
and b3 = (candidate [1; 2; 3] = Some 1)
(* etc. *)
in b0 && b1 && b2 && b3;;
The goal of this exercise is to implement a function that returns the last element of a list, if any:
let test_list_last_int candidate =
let b0 = (candidate [] = None)
and b1 = (candidate [1] = Some 1)
and b2 = (candidate [1; 2] = Some 2)
and b3 = (candidate [1; 2; 3] = Some 3)
(* etc. *)
in b0 && b1 && b2 && b3;;
Alfrothul: I know! I know!
Halcyon: Ah, Cloud Atlas...
Anton (patiently): What do you know now?
Alfrothul: I know how to program this function, look:
let list_last_int vs_given =
let rec visit vs =
match vs with
| [] ->
None
| v :: vs' ->
if vs' = []
then Some v
else visit vs'
in visit vs_given;;
Pablito (helpful as ever): And it passes the unit test too:
# test_list_last_int list_last_int;;
- : bool = true
#
Anton: What’s the type of your function?
Alfrothul: Easy-peasy:
# list_last_int;;
- : 'a list -> 'a option = <fun>
#
Anton: It’s a polymorphic type.
Alfrothul: Well, yes.
Anton: So why the name list_last_int?
Alfrothul: Drat. Right, the first unit-test function is named test_list_last_int, but of course that is because it has to be monomorphic. OK, let me rename this function, and add another unit-test function to boot:
let list_last vs_given =
let rec visit vs =
match vs with
| [] ->
None
| v :: vs' ->
if vs' = []
then Some v
else visit vs'
in visit vs_given;;
let test_list_last_char candidate =
let b0 = (candidate [] = None)
and b1 = (candidate ['a'] = Some 'a')
and b2 = (candidate ['a'; 'b'] = Some 'b')
and b3 = (candidate ['a'; 'b'; 'c'] = Some 'c')
(* etc. *)
in b0 && b1 && b2 && b3;;
Pablito: Good news, it still passes the first unit test, and it passes the new unit test too:
# test_list_last_int list_last;;
- : bool = true
# test_list_last_char list_last;;
- : bool = true
#
Alfrothul: Thank you very much.
Anton: Your definition doesn’t look right.
Alfrothul: Well, it passes the unit tests.
Anton: For sure, but it is testing vs' in the cons-case.
Alfrothul: Well, yes it does. It’s, like, its raison d’être.
Halcyon: Alfrothul, you are so full of joie de vivre.
Jacques Clouseau (suspicious): What is all this French speaking all of a sudden?
Mimer: Chief-Inspector Clouseau! Thanks for coming by!
Anton (heedlessly): How would you write it using list_fold_right? What is its inductive specification?
Alfrothul: Give me a chance:
let list_last vs =
let rec visit vs =
match vs with
| [] ->
None
| v :: [] ->
Some v
| v :: vs' ->
visit vs'
in visit vs;;
Anton: Three clauses now? But there are only two list constructors. Plus, match-expressions are desugared into nested if-expressions, so your two definitions are the same.
Alfrothul: Harrumph.
Dana: Hi guys. You look challenged.
Halcyon: Only temporarily.
Anton: We need to define the last element of the list denoted by vs by structural induction over this list.
Dana: I see.
Alfrothul: The base case: vs = [] first. There is no element in the empty list, and therefore no last element either. So the result must be None.
Dana: The induction step: vs = v :: vs' now. The induction hypothesis over vs' is either Some v' (in which case the last element of vs' is v') or None (in which case vs' has no last element). And then the question is, in each case, what is the last element of v :: vs'?
Anton: Well, under the hypothesis that the last element of vs' is v', I guess that the last element of v :: vs' is still v'. The last shall remain the last, or something. So the result must also be Some v'.
Alfrothul: And under the hypothesis that vs' has no element, v is not only the first element of v :: vs', but its only element, and therefore also its last. The first shall be the last in a singleton list, or something. So the result must be Some v.
Pablito: And that’s it?
Halcyon: Je vous l’avais bien dit les gars.
Alfrothul: Yes, you had told us, but still, let me see:
let list_last vs =
let rec visit vs =
match vs with
| [] ->
None
| v :: vs' ->
match visit vs' with
| None ->
Some v
| Some v' ->
Some v'
in visit vs;;
Pablito (swift): Good news, it passes the unit tests:
# test_list_last_int list_last;;
- : bool = true
# test_list_last_char list_last;;
- : bool = true
#
Anton: And now it is simple to express using list_fold_right, look:
let list_last_alt vs =
list_fold_right None
(fun v ih ->
match ih with
| None ->
Some v
| Some v' ->
Some v')
vs;;
Pablito: Well, believe it or not, this one also passes the unit tests:
# test_list_last_int list_last_alt;;
- : bool = true
# test_list_last_char list_last_alt;;
- : bool = true
#
Alfrothul: So that’s the solution?
Mimer: That’s a solution. But is it a nice solution?
Dana: I guess not, considering the option-typed value that is tested each time visit returns. So, only a mechanism?
Anton: You mean there is a solution where visit directly returns the last element, not the last element, optionally?
Mimer: Yup.
Dana: Can you be less elliptic?
Mimer: Yes.
Dana: Pray be.
Mimer: Less elliptic?
Dana: Less elliptic.
Mimer: Well, look at the unit-test function.
Dana (soberly): Looking here:
let test_list_last_char candidate =
let b0 = (candidate [] = None)
and b1 = (candidate ['a'] = Some 'a')
and b2 = (candidate ['a'; 'b'] = Some 'b')
and b3 = (candidate ['a'; 'b'; 'c'] = Some 'c')
(* etc. *)
in b0 && b1 && b2 && b3;;
Mimer: And?
Dana: Well, there are two cases.
Pablito (helpfully): The result is optional, so yes, there are two cases: None or Some v, where v is the last element of the given list.
Anton: None is used when the given list is empty, and Some when the given list is not empty.
Alfrothul: Guys, that’s something we can do a priori:
let list_last vs_given =
match vs_given with
| [] ->
None
| v_given :: vs'_given ->
Some ...;;
Halcyon (cleverly): You just wrote an ellipsis. Is that less elliptic?
Anton (heedless): Ah... Now we can declare and use a recursive function that traverses the tail of given list, since it is nonempty.
Alfrothul: And this recursive function takes two arguments – the current tail of the given list, to be traversed, and the element that precedes this current list in the given list:
let list_last vs_given =
match vs_given with
| [] ->
None
| v_given :: vs'_given ->
Some (let rec visit vs v =
...
in visit vs'_given v_given;;
Mimer: You guys are doing good. Keep thinking. A suggestion though: to answer Question c. in the exercise, have the initial call to visit be with vs_given rather than with vs'_given:
let list_last vs_given =
match vs_given with
| [] ->
None
| v_given :: vs'_given ->
Some (let rec visit vs v =
...
in visit vs_given v_given;;
Mimer: The unmodified implementation and the modified implementation are observationally equivalent, but the answer will be clearer.
The goal of this exercise is to implement several versions of an OCaml function that given a list of comparable elements, yields the minimum element and the maximum element of this list, if these elements exist. (So yes, this function is partial.)
The goal of this exercise is to implement an OCaml function that given a list of comparable elements, tests whether this list is sorted in strictly increasing order.
Food for thought:
Can you express your answer to Question b. using either list_fold_right or list_fold_left?
Here are two unit-test functions:
let test_list_sortedp_in_increasing_order_int candidate =
let b0 = (candidate [] = true)
and b1 = (candidate [9] = true)
and b2 = (candidate [8; 9] = true)
and b3 = (candidate [7; 8; 9] = true)
and b4 = (candidate [10; 7; 8; 9] = false)
and b5 = (candidate [4; 5; 6; 10; 7; 8; 9] = false)
and b6 = (candidate [0; 0] = false)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
let test_list_sortedp_in_increasing_order_char candidate =
let b0 = (candidate [] = true)
and b1 = (candidate ['y'] = true)
and b2 = (candidate ['x'; 'y'] = true)
and b3 = (candidate ['w'; 'x'; 'y'] = true)
and b4 = (candidate ['z'; 'w'; 'x'; 'y'] = false)
and b5 = (candidate ['a'; 'b'; 'c'; 'z'; 'w'; 'x'; 'y'] = false)
and b6 = (candidate ['h'; 'h'] = false)
in b0 && b1 && b2 && b3 && b4 && b5 && b6;;
Implement a total version of String.get.
Dana: Well, since String.get has type string -> int -> char, its total counterpart should have type string -> int -> char option.
Anton: Right. And if the given index is within bounds, the result should be Some c, where c is the character in the given string at the given index:
let test_total_string_get candidate =
let b0 = (candidate "0123" 0 = Some '0')
and b1 = (candidate "0123" 1 = Some '1')
and b2 = (candidate "0123" 2 = Some '2')
and b3 = (candidate "0123" 3 = Some '3')
in b0 && b1 && b2 && b3;;
Alfrothul: Whereas if the given index is out of bounds, the result should be None. If I may:
let test_total_string_get candidate =
let b0 = (candidate "0123" 0 = Some '0')
and b1 = (candidate "0123" 1 = Some '1')
and b2 = (candidate "0123" 2 = Some '2')
and b3 = (candidate "0123" 3 = Some '3')
and b4 = (let n = Random.int 100 + String.length "0123"
in candidate "0123" n = None)
and b5 = (let n = 0 - (Random.int 100 + 1)
in candidate "0123" n = None)
in b0 && b1 && b2 && b3 && b4 && b5;;
Anton: Nice. Any index beyond the last index, i.e., equal to or larger than the length of the tested string, is out of scope.
Alfrothul: And so is any negative index.
Halcyon (swinging in, and bursting into a rapturous song): HEIGH-HO!
Pablito (bursting too): HEIGH-HO!
Anton (facepalming): Oh no.
Halcyon and Pablito (chorusing): Heigh-ho, heigh-ho, to-tal string get we go:
let total_string_get s i =
let ls = String.length s
in if 0 <= i && i < ls
then Some (String.get s i)
else None;;
Alfrothul: Good job, guys.
Halcyon (modestly): Thank you. We rehearsed first.
Alfrothul: Ah, right, the singing. Yes. But I meant the implementation.
Pablito (modestly): Thank you. See how it passes the unit test?
Dana: I am curious. Could we trace the call to String.length?
Pablito: By all means.
Dana: First, a traced version of String.length:
let traced_string_length s =
let ls = String.length s
in let () = Printf.printf "String.length \"%s\" -> %n\n" s ls in
ls;;
Pablito: OK:
# traced_string_length "abc";;
String.length "abc" -> 3
- : int = 3
#
Dana: And now a traced version of total_string_get:
let traced_total_string_get s i =
let ls = traced_string_length s
in if 0 <= i && i < ls
then Some (String.get s i)
else None;;
Pablito: OK:
# traced_total_string_get "abc" 0;;
String.length "abc" -> 3
- : char option = Some 'a'
#
Dana: Can you try with the same string but another index? Doesn’t matter which.
Pablito: Sure thing:
# traced_total_string_get "abc" 10;;
String.length "abc" -> 3
- : char option = None
#
Dana: So the length is computed each time the function is applied.
Anton: Well, yes.
Dana: Even if it is the same string, look:
# (traced_total_string_get "abc" 0, traced_total_string_get "abc" 2, traced_total_string_get "abc" 4);;
String.length "abc" -> 3
String.length "abc" -> 3
String.length "abc" -> 3
- : char option * char option * char option = (Some 'a', Some 'c', None)
#
Halcyon: It’s hard to see that OCaml evaluates from right to left here, but we have to take the bad with the good.
Dana: Er, right. But the point I am trying to make here is that total_string_get is curried.
Alfrothul: I see you coming, Dana—you want to compute the length of the given string as soon as total_string_get is applied to this string.
Dana: And return a function that maps the index to the result, yes:
let traced_total_string_get' s =
let ls = traced_string_length s
in fun i -> if 0 <= i && i < ls
then Some (String.get s i)
else None;;
Anton: I see. The length will be computed only once with your implementation:
# let index'_abc = traced_total_string_get' "abc";;
String.length "abc" -> 3
val index'_abc : int -> char option = <fun>
# (index'_abc 0, index'_abc 2, index'_abc 4);;
- : char option * char option * char option = (Some 'a', Some 'c', None)
#
Pablito: Oh. The length will be computed every time with our implementation:
# let index_abc = traced_total_string_get "abc";;
val index_abc : int -> char option = <fun>
# (index_abc 0, index_abc 2, index_abc 4);;
String.length "abc" -> 3
String.length "abc" -> 3
String.length "abc" -> 3
- : char option * char option * char option = (Some 'a', Some 'c', None)
#
Alfrothul: So index_abc and index'_abc are versions of the indexing function that are specialized with respect to the string "abc", but one version computes the length of the given string repeatedly whereas the other computes it once and for all. S-m-n theorem much, Dana?
Dana: Well, this way you only YOLO once.
Loki: And you only YOYOLOO once too.
Halcyon (struck by lightning): YOYOYOLOOO!
Mimer (kindly): You are getting there, Halcyon. You are getting there.
Halcyon and Pablito (harmonizing while gracefully departing): YOLO, YOLO, Kleene Curry we go, YOLO YOLO, YOLO YOLO, YOLO, YOLO.
Anton: There is a lesson here.
Alfrothul: That is usually the case. What is the lesson here?
Anton: Well, assuming that e stands for an OCaml expression that doesn’t involve x, compare the two following function abstractions:
fun x -> e + x
let v = e
in fun x -> v + x
Alfrothul: Right – evaluating the first yields a function where e is evaluated each time this function is applied, whereas evaluating the second only evaluates e once. The result is a function that uses the result of this evaluation.
Anton: It’s like e has been factored from the first function abstraction.
Dana: Yup.
Mimer: When functional programming was young, this factorization was known as lambda-hoisting.
Masato Takeichi: Indeed it was, thanks for remembering.
Mimer: Prof. Takeichi! Thanks for passing by!
As a continuation of Exercise 09 in Week 08, implement an OCaml function that zips a pair of lists into a list of pairs.
Ponder about the subsidiary question of Exercise 09 in Week 08. Is the zip function total? Are the types 'a list * 'b list and ('a * 'b) list isomorphic?
Mimer: First of all, what is the context of Exercise 38?
Anton: It is in a chapter about The polymorphic option type.
Halcyon (Who Now Gets It): Which is the present chapter. That is what we call a self-reference.
Mimer: Thanks, Halcyon. Now what do we use the option type for?
Alfrothul: To make partial functions total.
Mimer: What is a total function?
Dana: A function that is defined on all of its input.
Mimer: And what is a partial function?
Dana: A function that is not defined on all of its input.
Mimer: Is the unzip function partial or total?
Alfrothul: It is total, since any list of pairs can be unzipped into a pair of lists.
Mimer: Anything special about these two lists in the resulting pair?
Anton: They have the same length as the given list of pairs.
Mimer: Is the zip function partial or total?
Dana: It is partial because it is only defined given two lists that have the same length.
Mimer: So how should it be programmed?
Dana: With an option type in the result: Some of a list of pairs should be returned for lists that have the same length, and None should be returned for lists that do not have the same length.
Mimer: Should the zip function first compute the lengths of its two given lists?
Alfrothul (virtuously): Not necessarily. First, it should be specified by induction on its input.
Anton: But the input is a pair of lists.
Alfrothul: OK, by induction on either list then, e.g., the first one.
Mimer: What should the base case be?
Pablito: In the base case, the first list is empty.
Alfrothul: Then if the second list is empty, the result should be Some []. Otherwise, it should be None.
Mimer: Good. And what should the induction step be?
Pablito: In the induction step, the first list is nonempty.
Alfrothul: Then if the second list is empty, the result should be None. Otherwise, it depends on the induction hypothesis (i.e., on the result of the recursive call on the tails of these two nonempty lists). Either it is Some of a list of pairs, or it is None.
Mimer: Is it obvious now?
Alfrothul: Yes.
Mimer: And does the implementation need to compute the length of the two given lists?
Anton: Harrumph. No. If the result if None, the two given lists did not have the same length.
Dana (suspicious): Can the zip function be expressed using list_fold_right?
Mimer: Well, it is specified by induction on one list and then by cases on the other, so what do you think?
Implement a function that given two lists, returns the one that is strictly the shortest. This implementation should satisfy the following unit tests:
let test_shortest_list_int candidate =
let b0 = (candidate [] [] = None)
and b1 = (candidate [1] [10] = None)
and b2 = (candidate [2; 1] [20; 10] = None)
and b3 = (candidate [3; 2; 1] [30; 20; 10] = None)
and b4 = (candidate [4; 3; 2; 1] [40; 30; 20; 10] = None)
(* ***** *)
and b5a = (candidate [] [10] = Some [])
and b6a = (candidate [2] [20; 10] = Some [2])
and b7a = (candidate [3; 2] [30; 20; 10] = Some [3; 2])
and b8a = (candidate [4; 3; 2] [40; 30; 20; 10] = Some [4; 3; 2])
(* ***** *)
and b5b = (candidate [1] [] = Some [])
and b6b = (candidate [2; 1] [20] = Some [20])
and b7b = (candidate [3; 2; 1] [30; 20] = Some [30; 20])
and b8b = (candidate [4; 3; 2; 1] [40; 30; 20] = Some [40; 30; 20])
in b0 && b1 && b2 && b3 && b4 && b5a && b6a && b7a && b8a && b5b && b6b && b7b && b8b;;
Anton: Well, this seems simple enough, if we use the compare predefined function that returns -1 if its first argument is strictly smaller than its second argument, 0 if they are equal, and 1 if its first argument is strictly greater than its second argument:
let shortest_list_v0 v1s v2s =
match compare (List.length v1s) (List.length v2s) with
| -1 ->
Some v1s
| 0 ->
None
| _ ->
Some v2s;;
Pablito: And it passes the unit tests too:
# test_shortest_list_int shortest_list_v0;;
- : bool = true
#
Alfrothul: Right. And the two lists are completely traversed, even though one could be a lot shorter than the second. Let’s traverse the two lists in parallel and stop at the end of the shortest. Look:
let shortest_list_v1 v1s_given v2s_given =
let rec visit v1s v2s =
match v1s with
| [] ->
(match v2s with
| [] ->
None
| _ :: v2s' ->
Some v1s_given)
| _ :: v1s' ->
(match v2s with
| [] ->
Some v2s_given
| _ :: v2s' ->
visit v1s' v2s')
in visit v1s_given v2s_given;;
Pablito: And it passes the unit tests too:
# test_shortest_list_int shortest_list_v1;;
- : bool = true
#
Anton: Clever use of lexical scope, Alfrothul.
Alfrothul: Thanks.
Pablito: Beg pardon?
Dana: The names of the formal parameters of shortest_list_v1 are v1s_given and v2s_given, and the names of the formal parameters of visit are v1s and v2s. So when reaching the end of either list, the names of the given lists are visible, and so we can return either of them without continuing to traverse the other.
Anton: Well, since we talk about visibility, how about we traverse the two lists more visibly together until the end of the shortest one?
Pablito: More visibly together until the end of the shortest one.
Anton: Well, yes, by pairing them and matching the pair, look:
let shortest_list_v2 v1s_given v2s_given =
let rec visit v1s v2s =
match (v1s, v2s) with
| ([], []) ->
None
| ([], _ :: v2s') ->
Some v1s_given
| (_ :: v1s', []) ->
Some v2s_given
| (_ :: v1s', _ :: v2s') ->
visit v1s' v2s'
in visit v1s_given v2s_given;;
Pablito (cautiously): OK, this implementation passes the unit tests:
# test_shortest_list_int shortest_list_v2;;
- : bool = true
#
Anton: And it is clearer too, with the 4 cases nil and nil, nil and cons, cons and nil, and cons and cons. If both lists are empty, they have the same length and so the result should be None.
Pablito: I see. And if either list is empty, the corresponding given list is the shortest.
Anton: And if both lists are nonempty, we defer to the induction hypothesis about their tail. So, the implementation is clearer.
Alfrothul (thoughtfully): It is also a bit more wasteful too, since each a pair is constructed each time visit is called.
Halcyon (out of the blue): What if we don’t put the parentheses?
Pablito: Don’t put the parentheses.
Halcyon: Well, yes, look:
let shortest_list_v3 v1s_given v2s_given =
let rec visit v1s v2s =
match v1s, v2s with
| [], [] ->
None
| [], _ :: v2s' ->
Some v1s_given
| _ :: v1s', [] ->
Some v2s_given
| _ :: v1s', _ :: v2s' ->
visit v1s' v2s'
in visit v1s_given v2s_given;;
Halcyon: And this implementation passes the unit tests too:
# test_shortest_list_int shortest_list_v3;;
- : bool = true
#
Alfrothul: Actually, not putting parentheses is just a syntactic convenience. The pair is still constructed.
Anton: Why am I reminded of Lisp?
Alfrothul: Probably because Lisp programmers are supposed to be enlightened when they don’t see the parentheses anymore.
John McCarthy: Well, it did seem like a good idea at the time.
Mimer: Prof. McCarthy! Thanks for stopping by!
Dana: Actually, constructing pairs for constructing pairs, why don’t we uncurry visit?
Anton: Uncurry visit.
Dana: Well, yes, look:
let shortest_list_v4 v1s_given v2s_given =
let rec visit p =
match p with
| ([], []) ->
None
| ([], _ :: v2s') ->
Some v1s_given
| (_ :: v1s', []) ->
Some v2s_given
| (_ :: v1s', _ :: v2s') ->
visit (v1s', v2s')
in visit (v1s_given, v2s_given);;
Pablito (diligent): And this implementation passes the unit tests too:
# test_shortest_list_int shortest_list_v4;;
- : bool = true
#
Anton: I see. The type of visit is now 'a list * 'a list -> 'a list option instead of 'a list -> 'a list -> 'a list option. So, uncurried instead of curried indeed.
Implement a function that given two lists, returns the one that is strictly the longest. This implementation should satisfy the following unit tests:
let test_longest_list_int candidate =
let b0 = (candidate [] [] = None)
and b1 = (candidate [1] [10] = None)
and b2 = (candidate [2; 1] [20; 10] = None)
and b3 = (candidate [3; 2; 1] [30; 20; 10] = None)
and b4 = (candidate [4; 3; 2; 1] [40; 30; 20; 10] = None)
(* ***** *)
and b5a = (candidate [] [10] = Some [10])
and b6a = (candidate [2] [20; 10] = Some [20; 10])
and b7a = (candidate [3; 2] [30; 20; 10] = Some [30; 20; 10])
and b8a = (candidate [4; 3; 2] [40; 30; 20; 10] = Some [40; 30; 20; 10])
(* ***** *)
and b5b = (candidate [1] [] = Some [1])
and b6b = (candidate [2; 1] [20] = Some [2; 1])
and b7b = (candidate [3; 2; 1] [30; 20] = Some [3; 2; 1])
and b8b = (candidate [4; 3; 2; 1] [40; 30; 20] = Some [4; 3; 2; 1])
in b0 && b1 && b2 && b3 && b4 && b5a && b6a && b7a && b8a && b5b && b6b && b7b && b8b;;
Simplified Exercise 34 and Exercise 36 [07 Apr 2023]
Quantified the variables in the type-inference rules [23 Jan 2023]
Created [13 Oct 2022]