Towards OCaml

• So languages are characterized by grammars.

• Regarding the three linguistic layers of characters, words, and sentences:

  • the legal characters are typically enumerated (e.g., letters, digits, punctuation marks, etc.), along with which ones are separators;
  • legal words are sequences of characters, as per the lexical structure of the language; and
  • legal sentences are sequences of words, as per the grammatical structure of the language.

  While this layering is descriptive in a natural language, it is prescriptive in a programming language.

• In emacs, typing M-x run-ocaml starts a read-eval-print loop (also known as a toplevel loop) where one types an OCaml expression, punctuated by ;; and the Enter key; the systems then reads this expression. Then, to a first approximation:

  • if this expression is grammatically incorrect, an error message is displayed and the read-eval-print loop is resumed;
  • if this expression is grammatically correct, it is evaluated:
    • if this evaluation yields an error, an error message is displayed and the read-eval-print loop is resumed;
    • if this evaluation requires more time resources than we have (e.g., because it is silently diverging), nothing happens until we type C-c C-c (i.e., simultaneously press the control key (as one would press the shift key) and the key c, twice); an error message is then displayed and the read-eval-print loop is resumed;
    • if this evaluation requires more space resources than what is available in our computer, an error message is displayed and the read-eval-print loop is resumed; and
    • if this evaluation completes with a result, this result is displayed and the read-eval-print loop will be resumed.

  Typing C-c C-d stops OCaml.

• OCaml is a language of expressions.

• Through the toplevel loop, these expressions are evaluated and yield values. These values have a type: integer, boolean, string, etc.

  This notion of type is not only specific to values: it characterizes the expressions that gave rise to these values.

  Furthermore, this notion of type is not only specific to OCaml expressions: it characterizes the OCaml programming language itself.

  Well-typed programs cannot go wrong.

  —Robin Milner

  OCaml is a statically typed programming language in that only expressions that are syntactically correct and that are type-correct too are evaluated. All the other expressions (i.e., the syntactically incorrect expressions and the syntactically correct but type-incorrect expressions) are rejected. The benefit of this syntactic discipline is that only grammatically correct expressions are considered (which avoids a world of confusions). The benefit of this typing discipline is that running an OCaml program never gives rise to a type error.

  Type systems have been developed “bottom up”, i.e., as increased abstractions of desired computational behaviors. So it is something of a surprise that they also have a logical content, but this topic is out of scope here.

Binary relations – a reminder

To quote the Wikipedia entry about binary relations, in mathematics, a binary relation over two sets A and B is a set of ordered pairs (a, b) consisting of elements a in A and b in B.

For example, the relation “is greater than” over the set of integers Z is the set of pairs of integers (i, j) for which there exists a positive integer k such that i = j + k. This particular relation is often represented using a set comprehension: {(i, j) | i belongs to the set of integers Z, j belongs to Z, and there exists a positive integer k such that i = j + k}.

Mathematical functions – a reminder

To quote the Wikipedia entry about functions, in mathematics, a function is a relation between two sets – the domain of the function and its codomain – that maps each element of the domain to at most one element of the codomain.

Examples:

• The “successor” function over the set of integers Z is the relation {(i, j) | i + 1 = j}. Here, both the domain and the codomain of the successor function are Z.
• The “absolute value” function maps a negative integer -i to the natural number i and a non-negative integer i to the natural number i. Here, the domain is Z (the set of integers) and the codomain is N (the set of natural numbers).

A function is often represented with its graph in that the pairs in its relation are the Cartesian coordinates of points in the Euclidean plane, a geometric rendition of the enumeration of these pairs. For example, the successor function over natural numbers is enumerated with {(0, 1), (1, 2), (2, 3), ...} and the square function over natural numbers with {(0, 0), (1, 1), (2, 4), (3, 9), ...}.

A predicate is a function whose codomain is the set of Booleans.

Examples:

• A function that maps any negative integer to false and any non-negative integer to true.
• A function that maps any even integer to true and any odd integer to false.

Total functions – a reminder

A function is total when it maps each element of its domain to one element of its codomain. The successor function over natural numbers, for example, is total.

Partial functions – a reminder

A function is partial when it does not map each element of its domain to an element of its codomain. The predecessor function over natural numbers, for example, is partial because while it maps any natural number n+1 to n, it does not map 0 to any natural number. For another example, a function that is only defined over non-negative integers is also partial.

Functions in Computer Science

Macroscopically, programs compute functions that map input data to output data.

Microscopically, we can implement functions in OCaml.

Version

Added the reminders about relations and functions [02 Apr 2020]

Added the quote by Robin Milner [31 Jan 2020]

Fixed a typo in the narrative, thanks to Yunjeong Lee’s eagle eye [30 Mar 2019]

Created [28 Jan 2019]