Concrete data types¶

The goal of this lecture note is to describe how to declare new types in OCaml.

Resources¶

The OCaml code for the present lecture note (latest version: 30 Mar 2021).

Declaring new types in OCaml¶

OCaml also lets us declare new types for our data, be it

to alias a pre-existing type,
to name a compound type, or
to define a sum type.

This expressive power is accounted for by the following refined BNF:

<toplevel-expression> ::= <expression> | let <formal> = <definiens> | type <variable> = <type-definiens>
<type-definiens> ::= <type> | {| <constructor> {of <type>}?}
<type> ::= <variable> | <type>{ * <type>}* | <type> -> <type>

Let us study each of these constructs in turn.

Aliasing a pre-existing type¶

Say that we want to define a type to represent names, and that concretely this representation is that of strings. We could keep it in mind and mentally read “name” whenever we come across a string. However, that is not convenient since not all strings represent names. So instead, we can alias strings with the following type declaration:

type name = string;;

This declaration puts us in position to use name as a type. It extends the current type environment with a new binding, just like a let-expression extends the current value environment with a new binding.

Aliasing a compound type¶

For convenience, we can alias the type of Boolean transformers:

type boolean_transformer = bool -> bool;;

Likewise, say that we need to associate names and integers by pairing them:

name * int

For convenience, we can declare this assocation as such:

type association = name * int;;

type association_list = association list;;

More complex examples can be found in Exercise 5 of Week 04:

type triple_of_int_and_char_and_bool = int * char * bool;;

type pair_of_pair_of_int_and_bool_and_of_triple_of_char_and_string_and_char = (int * bool) * (char * string * char);;

Aliasing a polymorphic type¶

To alias a polymorphic type, one prefixes its type declaration with the corresponding type variables. For example:

type 'a singleton = 'a;;

type ('a, 'b) pair = 'a * 'b;;

type ('a, 'b, 'c) triple = 'a * 'b * 'c;;

type 'a association_list = (name * 'a) list;;

Harald: Association lists, eh?

Alfrothul: They seem strangely familiar.

Halcyon (frowning): As in – déjà vu.

Mimer (not leading at all): The environment in a typing judgment, perhaps?

Alfrothul (getting it): And in the evaluation mechanism of OCaml.

Loki (casually): Polymorphism at work. Again.

Harald: The empty list represents the empty environment.

Alfrothul: Bindings are represented as associations.

Harald: And an environment is extended by consing a new association.

Alfrothul: On the left.

Power and limitations of aliasing types¶

Aliasing types can clarify things but OCaml, left to itself, does not use our aliases unless we tell it to. To wit, the type of the swap function, fun (x, y) -> (y, x) is 'a * 'b -> 'b * 'a, not ('a, 'b) pair -> ('b, 'a) pair:

# fun (x, y) -> (y, x);;
- : 'a * 'b -> 'b * 'a = <fun>
#

As for telling OCaml, we can do that by specifying a type (say, t) next to each formal (say, x):

(x : t)

For example:

let pair_swap : ('a, 'b) pair -> ('b, 'a) pair =
  fun (a, b) -> (b, a);;

Or alternatively:

let pair_swap ((a, b) : ('a, 'b) pair) : ('b, 'a) pair =
  (b, a);;

Likewise:

let neg : boolean_transformer =
  fun b -> if b then false else true;;

Datatype constructors¶

To tell OCaml which type we mean for our data types, we declare them so that they have data constructors:

type 'a singleton =
  | Singleton of 'a;;

type ('a, 'b) pair =
  | Pair of 'a * 'b;;

type ('a, 'b, 'c) triple =
  | Triple of 'a * 'b * 'c;;

These three declarations have the effect of extending the BNF of types with three new types, and the language of terms with three new constructors:

SINGLETON	G \|- e : t
	G \|- Singleton e : t singleton

PAIR	G \|- e1 : t1	G \|- e2 : t2
	G \|- Pair (e1, e2) : (t1, t2) pair

TRIPLE	G \|- e1 : t1	G \|- e2 : t2	G \|- e3 : t3
	G \|- Triple (e1, e2, e3) : (t1, t2, t3) triple

The three type constructors Singleton, Pair, and Triple can now be used:

# Singleton 10;;
- : int singleton = Singleton 10
# Pair (true, "hello");;
- : (bool, string) pair = Pair (true, "hello")
#

And now the swap function can have a meaningful type that involves pairs without any explicit type specification:

# fun (Pair (a, b)) -> Pair (b, a);;
- : ('a, 'b) pair -> ('b, 'a) pair = <fun>
#

Analysis:

the formal parameter, (Pair (a, b)), tells OCaml that the argument is expected to be constructed with the Pair constructor, and that the components of this pair should be named a and b; and
the body of the function, Pair (b, a), tells OCaml to construct a pair out of b and a and to let this pair have the type pair.

The swap function expects a pair constructed using Pair:

# let swap (Pair (a, b)) = Pair (b, a);;
val swap : ('a, 'b) pair -> ('b, 'a) pair = <fun>
# swap (Pair (1, true));;
- : (bool, int) pair = Pair (true, 1)
#

Declaring a sum type¶

Booleans, being either true or false, provide a prototypical example of a sum type. OCaml being implemented in OCaml, the type for Booleans is initially defined as follows:

type boolean = True
             | False;;

This declaration extends the current type environment with a new binding and the language with two new data constructors: the type boolean now exists, together with its two constructors, True and False.

Notes:

in actuality, boolean is called bool and its two constructors are literals in OCaml (namely the lexical units true and false);
by lexical convention, types are written in lower case and data constructors are capitalized; and
in the definition of a sum type, the vertical bar before the first constructor is optional. So one could also write:
```
type boolean =
  | True
  | False;;
```

To decide which summand (i.e., which of True or False) one is given, one uses a match-expression. For example, here is an unparsing function for values of type boolean:

let show_boolean b =
 (* show_boolean : boolean -> string *)
  match b with
  | True -> "True"
  | False -> "False";;

And here are conversion functions between bool and boolean:

let boolean_to_bool b =
 (* boolean_to_bool : boolean -> bool *)
  match b with
  | True -> true
  | False -> false;;

let bool_to_boolean b =
 (* bool_to_boolean : bool -> boolean *)
  match b with
  | true -> True
  | false -> False;;

These two conversion functions are inverses of each other, which is another way to say that bool and boolean are isomorphic types.

The match-expression enumerates all the possible constructors, and selects which one it is being given:

# bool_to_boolean true;;
- : boolean = True
# bool_to_boolean false;;
- : boolean = False
# boolean_to_bool True;;
- : bool = true
# boolean_to_bool False;;
- : bool = false
#

Truth be told, a match-expression in OCaml is merely an abbreviation for an if-expression, so bool_to_boolean can be equivalently declared with an if-expression:

let bool_to_boolean' b =
 (* bool_to_boolean' : bool -> boolean *)
  if b
  then True
  else False;;

So for example, we can implement two versions of the negation function over values of type boolean – either directly, or indirectly by detouring via the bool type:

let test_boolean_not candidate =
 (* test_boolean_not : (boolean -> boolean) -> bool *)
  let b0 = (candidate True = False)
  and b1 = (candidate False = True)
  in b0 && b1;;

let direct_not b =
 (* direct_not : boolean -> boolean *)
  match b with
  | True -> False
  | False -> True;;

let indirect_not b =
 (* indirect_not : boolean -> boolean *)
  bool_to_boolean (not (boolean_to_bool b));;

Both versions pass the unit test:

# test_boolean_not direct_not;;
- : bool = true
# test_boolean_not indirect_not;;
- : bool = true
#

The idea of detouring is explored further in Exercise 1.

A side remark¶

In match-expressions, the vertical bar before the first constructor is optional. So each of the following definitions is syntactically correct:

let minimum i j =
 (* minimum : int -> int -> bool *)
  match i < j with
  | true -> i    (* with a vertical bar before true *)
  | false -> j;;

let maximum i j =
 (* maximum : int -> int -> bool *)
  match i < j with
    true -> j    (* without a vertical bar before true *)
  | false -> i;;

Harald (grumbling): How many more hairs are we going to split here?

Loki (serene): The gods are in the details, Harald.

A useful sum type with 3 constructors¶

Often, when comparing two ordered values v1 and v2, we need to distinguish 3 cases:

v1 < v2
v1 = v2
v1 > v2

To this end, we nest two conditional expressions, and the resulting layout is not very pleasing to the eye.

Instead, we can define a sum type that captures this comparison:

type comparison = Lt | Eq | Gt;;

let compare v1 v2 =
 (* compare : 'a -> 'a -> comparison *)
  if v1 < v2 then Lt else if v1 = v2 then Eq else Gt;;

And now the program layout is more pleasing to the eye and therefore readable:

match compare v1 v2 with
| Lt ->
   ...
| Eq ->
   ...
| Gt ->
   ...

Beware of the Turing tar-pit

in which everything is possible

but nothing of interest is easy.

—Alan Perlis‘s programming epigram #54

Interlude¶

Vigfus: How about a concrete example of using this comparison type?

Harald: Good idea, Vigfus, good idea. What do you have in mind?

Vigfus: Well, nothing. That’s why I am asking for one.

Alfrothul: OK. Say that we want to compare the length of two given lists. If they have the same length, the result is Eq. If the first is shorter than the second, the result is Lt. And if the first is longer than the second, the result is Gt.

Vigfus: So, like this:

let test_list_compare_length_int candidate =
  let b0 = (candidate           []               [] = Eq)
  and b1 = (candidate          [1]             [10] = Eq)
  and b2 = (candidate       [2; 1]         [20; 10] = Eq)
  and b3 = (candidate    [3; 2; 1]     [30; 20; 10] = Eq)
  and b4 = (candidate [4; 3; 2; 1] [40; 30; 20; 10] = Eq)
  (* ***** *)
  and b5a = (candidate        []             [10] = Lt)
  and b6a = (candidate       [2]         [20; 10] = Lt)
  and b7a = (candidate    [3; 2]     [30; 20; 10] = Lt)
  and b8a = (candidate [4; 3; 2] [40; 30; 20; 10] = Lt)
  (* ***** *)
  and b5b = (candidate          [1]           [] = Gt)
  and b6b = (candidate       [2; 1]         [20] = Gt)
  and b7b = (candidate    [3; 2; 1]     [30; 20] = Gt)
  and b8b = (candidate [4; 3; 2; 1] [40; 30; 20] = Gt)
  in b0 && b1 && b2 && b3 && b4 && b5a && b6a && b7a && b8a && b5b && b6b && b7b && b8b;;

Alfrothul: Yes, like this.

Vigfus: So, like that:

let list_compare_length_v0 v1s v2s =
  compare (List.length v1s) (List.length v2s);;

Alfrothul: Yes, like that:

# test_list_compare_length_int list_compare_length_v0;;
- : bool = true
#

Vigfus: OK.

Harald: In this implementation, both lists are completely traversed.

Vigfus: Well, yes, to compute their length.

Harald: But there is no need for that. We could traverse them together, as in the solution for Exercise 27 in Week 09, and stop as soon as we reach the end of the shortest list. Look:

let list_compare_length_v1 v1s v2s =
  let rec visit v1s v2s =
    match v1s with
    | [] ->
       (match v2s with
        | [] ->
           Eq
        | _ :: v2s' ->
           Lt)
    | _ :: v1s' ->
       (match v2s with
        | [] ->
           Gt
        | _ :: v2s' ->
           visit v1s' v2s')
  in visit v1s v2s;;

Vigfus: Just a sec:

# test_list_compare_length_int list_compare_length_v1;;
- : bool = true
#

Vigfus: OK. You were saying?

Harald: Well, in the base case, the first list is empty. If the second list is empty too, they have the same length. Otherwise, they don’t, and the first one is shorter.

Vigfus: Ah, right, and the rest of the second list is not even traversed.

Harald. That’s the point. And in the induction step, the first list is not empty. If the second list is empty, the first one is longer.

Vigfus: Right. And the rest of the first list is not traversed either.

Harald: Otherwise, we use the induction hypothesis on their tails.

Declaring a sum type, continued¶

So sum types are declared by enumerating its constructors. These constructors can be parameterized. For example, here is the sum type for integers and strings:

type integer_or_string =
| Integer of int
| String of string;;

For example, here is an unparsing function for values of type integer_or_string:

let show_integer_or_string v =
 (* show_integer_or_string : integer_or_string -> string *)
  match v with
  | Integer n -> "Integer " ^ show_int n
  | String s -> "String " ^ show_string s;;

Likewise here are two predicates to test whether a value of type integer_or_string is an integer or a string:

let is_integer v =
 (* is_integer : integer_or_string -> bool *)
  match v with
  | Integer n -> true
  | String s -> false;;

let is_string v =
 (* is_string : integer_or_string -> bool *)
  match v with
  | Integer n -> false
  | String s -> true;;

Sum types can also be polymorphic. To take an example straight out of a French restaurant:

type ('a, 'b) cheese_or_dessert =
| Cheese of 'a
| Dessert of 'b;;

Values of that type are vacuously polymorphic since the type of the other constructor is unspecified:

# Cheese "camembert";;
- : (string, 'a) cheese_or_dessert = Cheese "camembert"
# Dessert "Savarin";;
- : ('a, string) cheese_or_dessert = Dessert "Savarin"
# Dessert "Paris-Brest";;
- : ('a, string) cheese_or_dessert = Dessert "Paris-Brest"
# Cheese "Saint-Félicien";;
- : (string, 'a) cheese_or_dessert = Cheese "Saint-Félicien"
#

Vigfus: What about cheesecake?

Harald (prudent): The jury is still out on this one.

Loki (humming): “You can’t take anything you want...”

Mimer (chorusing): ”...in any French restaurant.”

The option type, revisited¶

The option type (see Chapter The polymorphic option type) is predefined in OCaml, but still here its definition anyhow, priming the names option, Some and None in order not to shadow OCaml’s names:

type 'a option' =
| Some' of 'a
| None';;

Applying the constructor Some to a value of type t yields a value of type t option:

# Some 33;;
- : int option = Some 33
# Some true;;
- : bool option = Some true
# Some "thing or other";;
- : string option = Some "thing or other"
# Some (Some (Some "stuttering"));;
- : string option option option = Some (Some (Some "stuttering"))
#

Recursive data types¶

Just as functions can be defined in a recursive fashion (i.e., in terms of themselves), types can be defined in a recursive fashion using self-reference, i.e., the name of the type we are declaring can be used on the right-hand side of the declaration:

Revisiting the section about A sound and complete representation of natural numbers in Week 02:
```
type nat =
| O
| S of nat;;
```
The resource file contains implementation of conversion functions from non-negative integers to nat and vice versa.

Revisiting the section about The onion, revisited in Week 02:
```
type onion_bulb =
| Bud
| Layer of onion_bulb;;
```

As pointed out there, these two types are isomorphic because we can write conversion functions between each of them that are inverses of each other:

let rec onion_bulb_to_nat ob =
  match ob with
  | Bud ->
     O
  | Layer ob' ->
     S (onion_bulb_to_nat ob');;

let rec nat_to_onion_bulb n =
  match n with
  | O ->
     Bud
  | S n' ->
     Layer (nat_to_onion_bulb n');;

If we were to implement a generator of random values of type nat and a generator of random onion bulbs, we could verify that

mapping a randomly generated onion bulb to a value of type nat and back yields the same onion bulb, and that
mapping a randomly generated value of type nat to an onion bulb and back yields the same value.

The list type, revisited¶

The list type is predefined in OCaml, but still here a definition anyhow:

type 'a homemade_list =
| Nil
| Cons of 'a * 'a homemade_list;;

Using these two constructors, we can construct our own lists:

# Nil;;
- : 'a homemade_list = Nil
# Cons (1, Nil);;
- : int homemade_list = Cons (1, Nil)
# Cons (2, Cons (1, Nil));;
- : int homemade_list = Cons (2, Cons (1, Nil))
# Cons ("2", Cons ("1", Nil));;
- : string homemade_list = Cons ("2", Cons ("1", Nil))
#

This home-made type is isomorphic to the type of lists since we can implement two conversion functions that map any list to a home-made list, and any home-made list to a list. These conversion functions are inverses of each other:

let rec homemade_list_to_list vs =
  match vs with
  | Nil ->
     []
  | Cons (v, vs') ->
     v :: homemade_list_to_list vs';;

let rec list_to_homemade_list vs =
  match vs with
  | [] ->
     Nil
  | v :: vs' ->
     Cons (v, list_to_homemade_list vs');;

If we were to implement a generator of random lists and a generator of random home-made lists, we could verify that

mapping a randomly generated list to a home-made list and back yields the same list, and that
mapping a randomly generated home-made list to a list and back yields the same hime-made list.

Exercise 1¶

Here is the type of polymorphic right-to-left lists (hereby: “tsils”):

type 'a tsil =
| Lin
| Snoc of 'a tsil * 'a;;

Halcyon: On behalf of all the left-handed people in the world, thank you.

For example,

evaluating Snoc (Lin, 0) gives rise to the following construct, where Lin is depicted with ][ and Snoc with a box with two entries:
evaluating Snoc (Snoc (Lin, 0), 1) gives rise to the following construct:
evaluating Snoc (Snoc (Snoc (Lin, 0), 1), 2) gives rise to the following construct:

Specify and implement a htgnel function that computes the length of a tsil in the same manner as length computes the length of a list.
Specify and implement a dneppa function that computes the concatenation of two tsils in the same manner as append computes the concatenation of two lists.
Specify and implement a tsil_pam function that maps a function to each of the elements of a tsil and construct the tsil of the results, in the same manner as list_map maps a function to each of the elements of a list and construct the corresponding list with the results.
Implement two versions of a esrever function that reverses a tsil: one without an accumulator that uses dneppa, and one with an accumulator that only uses Snoc.

Specify and implement two conversion functions list_to_tsil and tsil_to_list that convert lists to tsils and vice versa:

let test_list_to_tsil candidate =
  let b0 = (candidate [] = Lin)
  and b2 = (candidate (1 :: 0 :: []) = Snoc (Snoc (Lin, 0), 1))
  (* etc. *)
  in b0 && b2;;

let test_tsil_to_list candidate =
  let b0 = (candidate Lin = [])
  and b2 = (candidate (Snoc (Snoc (Lin, 0), 1)) = 1 :: 0 :: [])
  (* etc. *)
  in b0 && b2;;

Vigfus: It is at moments like this that I am glad we don’t have an oral exam here.

Using list_to_tsil and tsil_to_list, implement
- htgnel in terms of length,
- length in terms of htgnel,
- tsil_pam in terms of list_map, and
- list_map in terms of tsil_pam.

Time permitting, implement the tsil counterparts of list_fold_right and of list_fold_left.

Prelude¶

Harald: A prelude at the end of a lecture note, now.

Brynja: Unless this ‘lude is meant to be read before embarking on Exercise 1?

Alfrothul: That could well be, you know. That could just well be.

Brynja: Well, along the same line, and since time is short, I think we should start this exercise with its last question.

Harald (O_o): Its last question.

Brynja: Well, yes – start by implementing list_to_tsil and tsil_to_list.

Alfrothul: Why?

Brynja: Well, because tsils are the right-to-left analogue of lists – and vice versa), and therefore it only makes sense that what a function does on lists, its analogue should do on tsils, and vice versa too. Look:

let make_tsil_to_tsil_analogue f =
 (* make_tsil_to_tsil_analogue : ('a list -> 'b list) -> 'a tsil -> 'b tsil *)
  fun sv -> list_to_tsil (f (tsil_to_list sv));;

let make_list_to_list_analogue g =
 (* make_list_to_list_analogue : ('a tsil -> 'b tsil) -> 'a list -> 'b list *)
  fun vs -> tsil_to_list (g (list_to_tsil vs));;

Harald: Oh. You mean that esrever should do the analogue of reverse, for example?

Brynja: Sure do:

# make_tsil_to_tsil_analogue List.rev (Snoc (Snoc (Snoc (Lin, 3), 2), 1));;
- : int tsil = Snoc (Snoc (Snoc (Lin, 1), 2), 3)
#

Harald: I see – applying the tsil analogue of the reverse function to the tsil analogue of a list yields the tsil analogue of the reverse of this list.

Halcyon (cringing): Headache!

Vigfus (beaming): This is so convenient for writing our unit tests.

Alfrothul: Actually, the same idea works for functions that produce lists or tsils:

let make_to_tsil_analogue f =
 (* make_to_tsil_analogue : ('a -> 'b list) -> 'a -> 'b tsil *)
  fun v -> list_to_tsil (f v);;

let make_to_list_analogue f =
 (* make_to_list_analogue : ('a -> 'b tsil) -> 'a -> 'b list *)
  fun v -> tsil_to_list (f v);;

Brynja: Yup. Applying make_to_tsil_analogue to atoi, for example, yields a function that maps a non-negative integer to the tsil of its successive predecessors.

Harald: Ditto for functions that take lists as input, and tsils too:

let make_tsil_to_analogue f =
 (* make_tsil_to_analogue : ('a list -> 'b) -> 'a tsil -> 'b *)
 fun sv -> f (tsil_to_list sv);;

let make_list_to_analogue g =
  (* make_list_to_analogue : ('a tsil -> 'b) -> 'a list -> 'b *)
  fun vs -> g (list_to_tsil vs);;

Vigfus: You were right, this prelude should be read before embarking on Exercise 1.

Halcyon: Well, my headache didn’t go away.

Brynja: Commuting diagrams to the rescue. First, make_tsil_to_tsil_analogue and make_list_to_list_analogue:

_images/ditaa-32f61ca96e101b249920256be6e02b71292e8418.png

Alfrothul: Then, make_to_tsil_analogue and make_to_list_analogue:

_images/ditaa-07347e0661b6231bfebb162e61f8afc84aba155e.png

Harald: And then, make_tsil_to_analogue and make_list_to_analogue:

_images/ditaa-25416add5da41281956dae8830d6b1736068cb00.png

Vigfus: Careful with that axe, Halcyon.

Halcyon (serene): Fear not. I am getting ready for the polymorphic trees in the next chapter.

Mutually recursive data types¶

Just as functions can be defined in a mutually recursive fashion (e.g., the even / odd predicates over natural numbers are defined in terms of each other), types can be defined in a mutually recursive fashion using the and keyword:

Revisiting the section about More agricultural vagaries: the case of shallots, in Week 02, here is again the grammar of shallots, a type of onion that can contain more than one bulb inside a layer:
```
<shallot-bulb>  ::= bud | (<shallot-bulbs>)

<shallot-bulbs> ::= <shallot-bulb> | <shallot-bulb> <shallot-bulbs>
```
This BNF is implemented as an OCaml data type:
```
type shallot_bulbs =
  One of shallot_bulb
| More of shallot_bulb * shallot_bulbs
and shallot_bulb =
  Bud'
| Layer' of shallot_bulbs;;
```
(The names Bud' and Layer' are primed to distinguish them from the data constructors in onion.)

The resource file contains both an unparser and a parser for shallots.
For another example, here is an alternative representation of natural numbers with one successor constructor for even numbers and another for odd numbers:
```
type even_nat =
  ZZ
| E of odd_nat
and odd_nat =
  O of even_nat;;
```
Whereas 2 is represented as S (S Z) with type nat, it is represented as E (O ZZ) with type even_nat, and whereas 3 is represented as S (S (S Z)) with type nat, it is represented as O (E (O ZZ)) with type odd_nat. The parity of the represented number is now conveyed in the type of its representation.

The resource file contains implementation of conversion functions from non-negative integers to even_nat (resp. odd_nat) and vice versa.

Grammatical correctness as type correctness¶

The grammars from Week 02 can be implemented as OCaml data types: the grammatical correctness of a sentence corresponds to the type correctness of its OCaml representation. As a corollary, once represented in OCaml, abstract-syntax trees are well-typed and therefore well-formed—unlike some of those from Exercise 12 of Week 02, which were not well-formed.

Let us revisit the section about A BNF for regular expressions and its grammar for regular expressions:

<regexp> ::= (empty) | (atom <atom>) | (any) | (seq <regexp> <regexp>) | (disj <regexp> <regexp>) | (star <regexp>) | (plus <regexp>)
<atom> ::= ...any integer...

This BNF is implemented with the following data type:

type regexp =
  Empty
| Atom of int
| Any
| Seq of regexp * regexp
| Disj of regexp * regexp
| Star of regexp
| Plus of regexp;;

where the non-terminal is represented as the type and its productions as the constructors for this type.

Likewise, and to a first approximation (see The proof is trivial (revisited) in the next chapter), the grammar from The proof is trivial (variations on a theme) in Week 04,

<proof> ::= The proof is trivial! Just <verb> <complement1> whose elements are <complement2>
<verb> ::= view the problem as | biject it to
<complement1> ::= a continuous complexity class | an open DAG | a non-degenerate topological space | a computable hypergraph
<complement2> ::= exact monoids | skew-symmetric combinatorial games | dihedral rings | semi-decidable homeomorphisms | closed Cayley graphs

is implemented with the following data types:

type verb =
  Verb1
| Verb2;;

type complement1 =
  Complement11
| Complement12
| Complement13
| Complement14;;

type complement2 =
  Complement21
| Complement22
| Complement23
| Complement24
| Complement25;;

type proof =
  Proof of verb * complement1 * complement2;;

where the non-terminals is represented as types and their productions as the constructors for these types.

A proof is unparsed with the following OCaml functions:

let show_verb v =
  match v with
  | Verb1 ->
     "view the problem as"
  | Verb2 ->
     "biject it to";;

let show_complement1 c1 =
  match c1 with
  | Complement11 ->
     "a continuous complexity class"
  | Complement12 ->
     "an open DAG"
  | Complement13 ->
     "a non-degenerate topological space"
  | Complement14 ->
     "a computable hypergraph";;

let show_complement2 c2 =
  match c2 with
  | Complement21 ->
     "exact monoids"
  | Complement22 ->
     "skew-symmetric combinatorial games"
  | Complement23 ->
     "dihedral rings"
  | Complement24 ->
     "semi-decidable homeomorphisms"
  | Complement25 ->
     "closed Cayley graphs";;

let show_proof p =
  match p with
  | Proof (v, c1, c2) ->
     "The proof is trivial!  Just " ^ show_verb v ^ " " ^ show_complement1 c1 ^ " whose elements are " ^ show_complement2 c2;;

Resources¶

The OCaml code for the present lecture note (latest version: 30 Mar 2021).

Version¶

Tightened the Interlude about comparing lists [01 Apr 2021]

Added the Interlude about comparing lists [30 Mar 2021]

Added the section about Grammatical correctness as type correctness as well as a parser and an unparser for shallots in the resource file [29 Mar 2021]

Adjusted the narrative and the BNFs of proofs [29 Mar 2021]

Named the fold functions appropriately in the resource file, thanks to Marcellinus Jerricho’s ever-watchful eye [28 Mar 2021]

Added the commuting diagrams and completed the section about mutually recursive types [28 Mar 2021]

Created [27 Mar 2021]

PAIR	G \|- e1 : t1	G \|- e2 : t2
	G \|- Pair (e1, e2) : (t1, t2) pair

TRIPLE	G \|- e1 : t1	G \|- e2 : t2	G \|- e3 : t3
	G \|- Triple (e1, e2, e3) : (t1, t2, t3) triple

Concrete data types¶

Resources¶

Declaring new types in OCaml¶

Aliasing a pre-existing type¶

Aliasing a compound type¶

Aliasing a polymorphic type¶

Power and limitations of aliasing types¶

Datatype constructors¶

Declaring a sum type¶

A side remark¶

A useful sum type with 3 constructors¶

Interlude¶

Declaring a sum type, continued¶

The option type, revisited¶

Recursive data types¶

The list type, revisited¶

Exercise 1¶

Prelude¶

Mutually recursive data types¶

Grammatical correctness as type correctness¶

Resources¶

Version¶

Table Of Contents

Previous topic

Next topic

Navigation

Concrete data types¶

Resources¶

Declaring new types in OCaml¶

Aliasing a pre-existing type¶

Aliasing a compound type¶

Aliasing a polymorphic type¶

Power and limitations of aliasing types¶

Datatype constructors¶

Declaring a sum type¶

A side remark¶

A useful sum type with 3 constructors¶

Interlude¶

Declaring a sum type, continued¶

The option type, revisited¶

Recursive data types¶

The list type, revisited¶

Exercise 1¶

Prelude¶

Mutually recursive data types¶

Grammatical correctness as type correctness¶

Resources¶

Version¶

Table Of Contents

Previous topic

Next topic

Quick search

Navigation