% Created 2020-09-18 Fri 22:23
% Intended LaTeX compiler: pdflatex
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{grffile}
\usepackage{longtable}
\usepackage{wrapfig}
\usepackage{rotating}
\usepackage[normalem]{ulem}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{amssymb}
\usepackage{capt-of}
\usepackage{hyperref}
\author{Brett Gilio}
\date{\textit{<2020-08-29 Sat 15:28>}}
\title{Why learn OCaml?}
\hypersetup{
pdfauthor={Brett Gilio},
pdftitle={Why learn OCaml?},
pdfkeywords={},
pdfsubject={},
pdfcreator={Emacs 27.1 (Org mode 9.4)},
pdflang={English}}
\begin{document}
\maketitle
\tableofcontents
\begin{center}
This article is an overview of the features of OCaml and the rich
type system it uses. The target audience of the article is for people
who have familiarity with programming in a statically-typed environment,
and understand at least conceptually what a type system is used for.
This is \emph{not} an introduction to functional programming, nor the core
syntax/libraries of OCaml. Knowledge of type theory is not assumed,
but you will be well-served to approach some of the type-theoretic
concepts used in this article with an open mindset.
\end{center}
\section{What is OCaml?}
\label{sec:org3fa289d}
In formal terms, OCaml\footnote{\url{https://ocaml.org/}} is an implementation of the Caml dialect, started
by Xavier Leroy with the INRIA Gallium\footnote{\url{http://gallium.inria.fr/}}
research team. Influenced primarily by Standard ML\footnote{\url{https://smlfamily.github.io/}}
and LISP (as well as C and Pascal for their imperative qualities), OCaml
was initiated as a functional programming language designed to offer
stellar performance, strong static typing, Hindley-Milner (and later
bidirectional HM-successor-style) type inference. Eventually the Caml
dialect, in the style of Standard ML, took the extension of an impure and
effectful I/O system and implemented a class-based object system which
still conformed to the strong type system.
OCaml is most widely recognized, as with most ML/Haskell dialects, for
their exceptional use in implementing compilers and type systems. Many
successful proof assistants, compiler toolchains, static analyzers, and
SMT-style solvers have been implemented in OCaml. For example, the Coq\footnote{\url{https://coq.inria.fr/}}
proof assistant is well known for implementing MLTT-influenced Cartesian closed\footnote{\url{https://ncatlab.org/nlab/show/cartesian+closed+category}}
dependent types in OCaml, as well as being one of the more
prominent examples of an interactive proof assistant used by formal
mathematicians and verification-focused programmers today. Additionally,
OCaml has found prominent success in commercial areas, such as
Jane Street\footnote{\url{https://www.janestreet.com/}} and their in-house trading
system which manages upwards of millions of stock trades every day.
While OCaml does not feature full formal specification at the type level
like Standard ML, it does offer a high degree of both determinism,
inferencing, and expression at the type-system level. Many who work on
OCaml may feel that while formal specification is nice, as it unifies
and codifies an implementation's behavior in a mathematical
and logically-sound way (guaranteeing soundness of the type system), the
result can slow progress of the language and prevent it from keeping
up-to-date with the needs of current programmers. For example, while
the Standard ML '97 revision\footnote{\url{https://smlfamily.github.io/sml97-defn.pdf}}
does not feature Unicode support, and neither does the Standard ML
Basis Library\footnote{\url{https://smlfamily.github.io/Basis/}} this has not
been an issue for OCaml. What OCaml lacks in a formal specification,
it readily makes up for in having a quality type-system,
pseudo/partial-specification, and set of libraries to implement
\texttt{UTF-8}, \texttt{UTF-16}, \texttt{UTF-32} strings and other encodings.
Where there is negative reaction toward OCaml, particularly from people
first approaching the language (typically from environments like Racket\footnote{\url{https://racket-lang.org/}},
Haskell, or even Python) is that the standard library for OCaml is
quite small. This, however, is intentional! OCaml has taken inspiration
from C in this regard, the core components, syntax, and implementation
of OCaml is highly portable and readily extensible. There are many
visible APIs for working with OCaml from other languages
(with C-runtimes) precisely because the implementation is succinct.
Admittedly, however, the standard library of OCaml has shown its age
in recent years and many components have been implemented or reworked
to bring the OCaml standard library up-to-date (but this still
seems to be a work in progress\footnote{\url{https://github.com/ocaml/ocaml/issues/7812}}).
In my opinion, when it comes to OCaml and its object-oriented system
(and perhaps contrary to other people, like Scala\footnote{\url{https://www.scala-lang.org/}}
fans), I feel the object/class system is well designed and considered.
The consistent rebuke I hear to this is that it feels like an
after-thought, given that the progression was from Caml -> OCaml with
the addition of the object/class system. However, I personally disagree
with this assessment. To me, the Java (and subsequently Scala) style
of objects, classes, constructors, inheritance, overloading, and
polymorphism is not as precise or elegant as what is offered by OCaml.
Additionally, the type safety (while greatly improved in Scala) is not
as implicit, nor as secure in Java where object constructions routinely
lead to errors from downcasting (which OCaml prohibits!).
\subsection{A look at [Objective] Caml}
\label{sec:org6164cae}
To continue the previous section, and using (probably the best top-level
in all of programming) \texttt{utop}\footnote{\url{https://github.com/ocaml-community/utop}},
we can take a look at some of the basics of object-oriented programming
using the OCaml environment.
\begin{verbatim}
class point =
object
val mutable x = 0
method get_x = x
method move d = x <- x + d
end;;
(* class point :
object val mutable x : int method get_x : int method move : int -> unit end *)
\end{verbatim}
The above source code should be rather self explanatory. We are defining
a point class with a mutable object \texttt{x}. We can see the type signature
below the declared class defining many of the implicit types of each
of the objects, as well as the methods. Using this class we can now
instantiate the class from the definition above, and then use the
methods of the class to perform some computations.
\begin{verbatim}
let instance = new point;;
(* val instance : point = *)
instance#get_x;;
(* - : int = 0 *)
instance#move 5;;
(* - : unit = () *)
instance#get_x;;
(* - : int = 5 *)
\end{verbatim}
However, classes do not have to be used to create objects. An object
can be constructed immediately without going through a class, where
inheritance is not preferred, or where references to expliticly bound
\texttt{self} may be preferred. Additionally, type abbreviations are not
permitted in immediate objects, which can lead to problematic
type references (which OCaml responsibly dictates and prevents at
compile-time).
\begin{verbatim}
let ints = ref [];;
(* val ints : '_weak1 list ref = {contents = []} *)
class external_reference_self =
object (self)
method n = 1
method register = ints := self :: !ints
end;;
(* Error: This expression has type < n : int; register : 'a; .. >
but an expression was expected of type 'weak1
Self type cannot escape its class *)
\end{verbatim}
The issue above, as stated, is that when \texttt{self} is placed within
the external reference to immediately created object \texttt{ints}, what is
created is an unfavorable and unsound situation where we can not
extend \texttt{ints} using the \texttt{self} reference (as there is a mismatched
type). The ability of the OCaml type system to not only recognize,
but also understand the implicit types of the above class and (failed)
attempt at inheritance prevents a situation where object classes
could very well allocate information to objects in (or, outside rather)
of the class which would not be properly handled for computation.
This could further lead to core dumps in insecure language runtimes
where this problem is not identified at compile-time.
OCaml does have a resolution to this situation (as expected
if you have ever used C++ or Java), coercions\footnote{\url{https://caml.inria.fr/pub/docs/manual-ocaml/objectexamples.html\#s\%3Ausing-coercions}}\textsuperscript{,}\,\footnote{\url{http://docs.cascading.org/cascading/2.6/userguide/html/ch07s02.html}}\textsuperscript{,}\,\footnote{\url{https://www.learncpp.com/cpp-tutorial/implicit-type-conversion-coercion/}}.
More detailed examples of object-oriented programming in OCaml can be
found \href{https://ocaml.org/learn/tutorials/objects.html}{here}.
\subsection{How \emph{strong} is this strong static typing?}
\label{sec:org252dc8e}
In today's world, it is not uncommon to have strong typing with your
favorite programming language. The obvious exclusions here are C/C++,
but even with the right compiler extensions (or static analyzers), you
can get some of the same guarantees of strongly typed languages in
traditionally weakly typed environments. Taking the example above of
insecure languages, where undefined behavior is routine and type security
is missing (or not as strong as LISP/ML/Haskell-family languages); the
result of misattributing types, passing data between incompatible
objects and methods, or incorrect memory behavior mangling the references
to live/dead objects can be disasterous and hard to debug.
People who have not experienced the beauty of a static type system
like the one in OCaml will find themselves unaware of the beauty beneath
it. It is particularly common (though gradually changing) that people
with experience in strong, statically typed programming languages have
not gotten a feel for the benefits of Hindley-Milner type inference.
The result of this is that programmers in systems like Java feel
as though their job can have a cumbersome task akin to bookkeeping
and accounting.
While nowadays programming languages like Java and Python have some
level of annotation-less type inferencing, it is not nearly as powerful
as the level of abstraction one can attain using OCaml.
\subsubsection{Damas-Hindley-Milner in a ``nutshell''}
\label{sec:org07b4505}
The DHM (or just HM) type system in slightly technical terms is an
abstraction for providing a typed lambda calculus. In other words, you
can take the functional (in a mathematical sense) aspects of a particular
syntax and make formal rules about their behavior; expressing all
forms of computations\footnote{\url{https://plato.stanford.edu/entries/church-turing/}}.
The Hindley-Milner implementation offers the logical correctness of
parametric typing rules to the structure of the lambda calculus. From
this combination of typed logical correctness, and deterministic behavior
we can derive the type of any expression (or term) from a specified
environment. This feature is called the ``principle type''. Perhaps the
most famous of proven algorithms that offers this level of type inferencing
is ``Algorithm W''.
A lot of the notions of type theory, and type inferencing can be very
daunting to people looking to get into more formal, and type correct
programming languages. As explained by Martin Grabmüller\footnote{\url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733\&rep=rep1\&type=pdf}},
this business is often inflated with high categorical and type theoretic
mathematics that make the task of understanding \emph{what} is happening
harder than it is at the core.
So, taking a look at the core principle behind Algorithm W, without
the (too much) mathematical jargon or notation we have two components:
\begin{itemize}
\item An input to Algorithm W, an expression and an environment. This is simply any and all information about the function/object/parameter and the modules/function-use we are working in.
\end{itemize}
This results in\ldots{}
\begin{itemize}
\item An output of a type for that given expression, and the return of a principle (overall) type.
\end{itemize}
The result of this algorithm, detailed using function expressions,
should result in the appropriate types for each expression based
on the syntax of that expression and its environment. (Note:
the expression in the first example below shows a mapping of
\texttt{int -> 'a}, in OCaml and Standard ML \texttt{'a} is used here to designate
a generic type.)
\begin{verbatim}
fun f -> f 3;;
(* - : (int -> 'a) -> 'a = *)
fun f -> f (f 3);;
(* - : (int -> int) -> int = *)
fun f -> f (f "OCaml!");;
(* - : (string -> string) -> string = *)
\end{verbatim}
Combining these elements together we are able to logically derive the
type of complex abstractions, such as functors\footnote{\url{https://www.math3ma.com/blog/what-is-a-functor-part-1}},
mappings, pattern matching, or simple functions. This example of Algorithm W as offered
by Robin Milner has been extended many times. If you are interested
in type theory, I suggest the following:
\begin{itemize}
\item \href{https://www.cis.upenn.edu/\~bcpierce/papers/lti-toplas.pdf}{Pierce-Turner: Bidirectional, Local Type Inference}
\item \href{https://arxiv.org/pdf/1306.6032.pdf}{Dunfield-Krishnaswami: Bidirectional, Higher-Rank Polymorphic Typing}
\end{itemize}
Parts of these modifications can also be found in programming languages
such as Rust which offers a modified HM-algorithm using some of the
Dunfield-Krishnaswami (and accordingly Pierce-Turner) research to
implement subtyping, local/region inference, and higher-ranked types.
The influence of languages like OCaml has been seen extended to Rust,
and despite my personal reservations about many of the claims of that
language it is astounding to see progress made in expressive type
systems being mainstreamed.
\subsection{Unification and Pattern Matching}
\label{sec:orgdc09f36}
Many of the impressive advantages of OCaml can be felt in features you
will not find in other ``strong'' statically typed languages. Picking
up where we left off, type inference offers many advantages when it
comes to creating powerful multifaceted and polymorphic expressions.
Taking the concept of type inference and abstracting up one level we
are introduced to type unification. type unificiation takes
the result of Algorithm W (the inferred type) and finds a way to create
a valid substitution of two expressions where both expressions are
of equivalent types. In simpler wording, unification allows two type
expressions to match.
When we are able to have a result with a matching pair of types we
are able to achieve pattern matching.
\begin{verbatim}
let unification_example x =
match x with
1 -> "Foo"
| 2 -> "Bar"
| 3 -> "Fizz"
| 4 -> "Buzz"
| _ -> "You entered: " ^ string_of_int x;;
(* val unification_example : int -> string = *)
unification_example 2;;
(* - : string = "Bar" *)
unification_example 4;;
(* - : string = "Buzz" *)
unification_example 9;;
(* - : string = "You entered: 9" *)
\end{verbatim}
As in C with the multiway conditional, \texttt{switch}, we are able to make
any number of possible values (\texttt{1...4}, with a wildcard \texttt{\_}) and
have a return based on the value given to \texttt{x}. However, do not be fooled,
what is happening here is not like \texttt{switch} or nested-\texttt{if} statements.
The result of this pattern matching process is permitted by the
type unification of \texttt{x} in \texttt{unification\_example}.
The power of pattern matching as a result of type unification is not
limited to just this multiway conditional scenario. You can find
pattern matching to be used in data destructuring, variable binding,
compiler tokenization, case analysis, and a more elegant solution
to exception handling\footnote{\url{https://www.cs.cornell.edu/courses/cs3110/2014fa/lectures/5/lec05.pdf}}.
\subsubsection{Note: Type Soundness \& Decidability}
\label{sec:orgcc664a6}
As type soundness is not constrained to monomorphic types as
specified in the Hindley-Milner algorithm and Standard ML formal
specification, it is possible to get unsound results where decidability
of the expression is not successful. OCaml has relaxed value
restrictions (and subtyping rules)\footnote{\url{https://caml.inria.fr/pub/old\_caml\_site/caml-list/1507.html}}\textsuperscript{,}\,\footnote{\url{https://www.math.nagoya-u.ac.jp/\~garrigue/papers/inria080613.pdf}}\textsuperscript{,}\,\footnote{\url{https://caml.inria.fr/pub/docs/oreilly-book/html/book-ora016.html}}.
\begin{verbatim}
let unsound_example = function x when x = x -> true;;
(* Characters 22-51:
let unsound_example = function x when x = x -> true;;
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
All clauses in this pattern-matching are guarded.
val unsound_example : 'a -> bool = *)
\end{verbatim}
\subsection{Higher-Ranked Types and Polymorphism}
\label{sec:orgf5f2295}
As explained above the OCaml type checking system is not as decidable
as Standard ML, and this is due to the relaxing of value/rank restriction.
This is not unique to OCaml, as it is also the case in the type systems
of Haskell (at \emph{rank-n}) and Rust. When dealing with functional programming languages
it is often desired to be able to use a term in differently-typed
contexts. This is different from the above examples of
unification/pattern matching where we are able to determine equivalent
types.
When using terms of a type in a differently-typed context we are asserting
the polymorphic quality for the type of that term. Polymorphic types
use something in mathematical logic known as universal quantification,
which may ring a bell if you have taken a course on discrete/predicate
logic. The meaning of this ``universal quantification'' is expressed with
a proposition where a type rule can be satisfied by any member of a
domain. In other words, universal quantification in functional programming
languages allow for a type may be given a different binding based on
the context they are quantifying.
You have likely been exposed to parametric polymorphism in other
languages, such as C++ with the template system or simple generic
programming in Java. An extension of the OCaml Hindley-Milner style
type system is the inclusion of subtype polymorphism. Which, like generics
allows for an object or expression of a certain type to work correctly
if passed to an object with a particular compatible subtype. We have
seen in the section on object-oriented programming in OCaml an example
where an expression is able to return a generic type.
\subsubsection{Parametric Polymorphism}
\label{sec:org9ff7c8d}
If you have experienced OCaml in the past, you will likely be aware
that function/operator overloading is not valid in the current
implementation. The reason for this is because the Hindley-Milner
inferencing type system and overloading operations can often conflict
with each other. There have been attempts in the past to workaround this
issue, namely with \emph{ad-hoc} modular implicits\footnote{\url{https://arxiv.org/pdf/1512.01895.pdf}}.
However, subtyping in OCaml is as powerful (if not more powerful and
performance-efficient) than the template system found in C++.
In Ocaml, when type inference determines that an expression is decidably
valid for any type (\emph{a la. generics}), the type system automatically
makes the expression polymorphic and parametric with type variables.
We have been introduced to type variables in the section covering
object-oriented programming in OCaml, with the notation of the
generic/arbitrary type \texttt{'a}. Expanding on that knowledge, and the
concept of multiple type variables, we can introduce parametric
polymorphism and observe value restriction.
\begin{verbatim}
let id x = x;;
(* val id : 'a -> 'a = *)
let weak_id = id id;;
(* val weak_id : '_weak1 -> '_weak1 = *)
weak_id 1;;
(* - : int = 1 *)
weak_id "OCaml";;
(* Characters 8-15:
weak_id "OCaml";;
^^^^^^^
Error: This expression has type string but an expression was expected of type int*)
\end{verbatim}
As we see above, we are given the arbitrary type \texttt{'a} in the first
statement, which when assigned to the polymorphic identifier \texttt{weak\_id}
is transformed into \texttt{'\_weak1}. The \texttt{\_} wildcard in the type expression
simply means of any unknown type, the universal quantifier. This works
when we apply the expression \texttt{weak\_id} to type \texttt{int}, but directly
afterwards we are now restricted to expressions of type \texttt{int -> int}.
The example above is only weakly polymorphic. The ability to retain
full polymorphism we use a technique known as ``Eta expansion'', and
return fully generalized types.\footnote{\url{http://ocamllabs.io/iocamljs/type\_inference.html}}
\begin{verbatim}
let map_id l = List.map id l;;
(* val map_id : 'a list -> 'a list = *)
\end{verbatim}
\subsubsection{Higher-Rank Polymorphism}
\label{sec:orgf0d56c6}
This section I graciously am parts lifting from \href{http://devmusings.legiasoft.com/blog/2008/05/23/higher-rank\_polymorphism\_in\_ocaml}{/dev/musings}, who
explained the sitution so well.
Higher-rank polymorphism in OCaml can be a sticky situation, with
many different possible implementations. At its core the OCaml
type system only allows for rank-1 polymorphism, which we saw
in the last section where \texttt{let}-binding is used to introduce polymorphic
expressions. Higher-ranked polymorphism comes with issues of decidablity
with Hindley-Milner type inference. Generally, the higher the rank
the more arbitrary categorical arrows are involved.
\begin{itemize}
\item \emph{Rank-1} (\texttt{let}-binding) polymorphism is always predicative and decidable, because all universal quantifiers do not appear as parameters to type constructions.
\item \emph{Rank-k} polymorphism is impredicative and decidable.\footnote{\url{https://wiki.haskell.org/Impredicative\_types}}
\item \emph{Rank-n} polymorphism is impredicative and not decidable.
\end{itemize}
Since OCaml is strictly \emph{prenex} (rank-1) polymorphic we have to create
rank-k solutions using type records\footnote{\url{https://dev.realworldocaml.org/records.html}}.
While explicit type annotations can exist in many places in OCaml, the
place where it is most abundant and reusable to the type system itself
is in the type record field. We can simulate a polymorphic type \texttt{r}
in a record field, as follows:
\begin{verbatim}
type r = {f : 'a . 'a -> 'a};;
(* type r = { f : 'a. 'a -> 'a; } *)
\end{verbatim}
Now, reusing our \texttt{let}-polymorphic expressions from earlier, we can
now rewrite them using the injective expression for type \texttt{r}.
\begin{verbatim}
let id x = x;;
(* val id : 'a -> 'a = *)
let map_pair r (p1, p2) = (r.f p1, r.f p2);;
(* val map_pair : r -> 'a * 'b -> 'a * 'b = *)
let sample = map_pair {f = id} (3, true);;
(* val sample : int * bool = (3, true) *)
\end{verbatim}
The particular difference between this example and higher-ranked types
in Standard ML is as mentioned earlier Standard ML works with
monomorphic types. When dealing with monomorphic types, we are
constrained in the kinds of data structures that can be created using
higher-ranked polymorphism.
\subsection{The Module System}
\label{sec:org7564382}
Structure control and modules are a common tradition nowadays in
programming languages. However, not many languages come close to the
expressive power of the module system in OCaml. The OCaml module system
is actually derived from the one started by Standard ML. Modules in
these type-inferred languages are first-class, in that a module
can come with its own set of interfaces, signatures, and submodules.
One of the only languages that approximates the power offered by OCaml
and Standard ML in its module abstraction is, yet another ML-dialect, F\#.
OCaml's module system is concerned primarily with a module and its
respective signature. Typically a module in another non-ML language will
be strictly stratified, in that you can not treat modules as values to
an expression. However, in OCaml and the ML-dialects this is corrected
by the notion of \emph{first-class modules}\footnote{\url{http://www.cs.cornell.edu/courses/cs3110/2020sp/manual-4.8/manual028.html}}.
For example:
\begin{verbatim}
let sort (type s) (module Set : Set.S with type elt = s) l =
Set.elements (List.fold_right Set.add l Set.empty);;
(* val sort : (module Set.S with type elt = 's) -> 's list -> 's list = *)
let make_set (type s) cmp =
let module S = Set.Make(struct
type t = s
let compare = cmp
end) in
(module S : Set.S with type elt = s);;
(* val make_set : ('s -> 's -> int) -> (module Set.S with type elt = 's) = *)
\end{verbatim}
With the module system, we can expand the module type signature, or
functor type which is inferred for a module much in the same way we can
infer the types of expressions. This is useful for making module types
reusable, or implementing module-selection in pattern-matching, or any
number of other possibilities.
For example, using the signature idiom (abbreviated):
\begin{verbatim}
module type MYHASH = sig
include module type of struct include Hashtbl end
val replace: ('a, 'b) t -> 'a -> 'b -> unit
end;;
(* module type MYHASH =
sig
type ('a, 'b) t = ('a, 'b) Hashtbl.t
val create : ?random:bool -> int -> ('a, 'b) t
val clear : ('a, 'b) t -> unit
val reset : ('a, 'b) t -> unit
val copy : ('a, 'b) t -> ('a, 'b) t
val add : ('a, 'b) t -> 'a -> 'b -> unit
val find : ('a, 'b) t -> 'a -> 'b
val find_opt : ('a, 'b) t -> 'a -> 'b option
val find_all : ('a, 'b) t -> 'a -> 'b list
val mem : ('a, 'b) t -> 'a -> bool
val remove : ('a, 'b) t -> 'a -> unit
val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
val filter_map_inplace : ('a -> 'b -> 'b option) -> ('a, 'b) t -> unit
val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
val length : ('a, 'b) t -> int
val randomize : unit -> unit
val is_randomized : unit -> bool
type statistics =
Hashtbl.statistics = {
num_bindings : int;
num_buckets : int;
max_bucket_length : int;
bucket_histogram : int array;
}
val stats : ('a, 'b) t -> statistics
val to_seq : ('a, 'b) t -> ('a * 'b) Seq.t
val to_seq_keys : ('a, 'b) t -> 'a Seq.t
val to_seq_values : ('a, 'b) t -> 'b Seq.t
val add_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit
val replace_seq : ('a, 'b) t -> ('a * 'b) Seq.t -> unit
val of_seq : ('a * 'b) Seq.t -> ('a, 'b) t
...*)
\end{verbatim}
The powerful properties of first-class modules allows not only for
rigorous applications to an existing code-base, but also creates and
aligns with highly expressive code. With first-class modules, the types
of abstractions can be permitted to generalize module use with functors,
or create data structures out of modules which are functional and pure.
\subsection{Generalized Algebraic Datatypes}
\label{sec:org4460708}
Type parameters can be used in a multifaceted way, allowing for additional
constratins and abstractions which may change depending on how the value
being used is constructed. In earlier sections we addressed the concept
of universal quantification, but we can also apply a similar concept to
type rules known as the existential quantifier.
Again, back to discrete/prediate logic, when we deal with existential
quantification, we are thinking of situations where in a logical system
there exists some variable which can be applied to our system from a
domain. This is different from universal quantification, where the
variable can be anything (or all members in a logical system).
OCaml uses existential quantification to create something known as an
equality-qualified type, or a generalized algebraic datatype. While this
notion is not unique to OCaml (and can similarly be found in Haskell),
GADTs can be thought of as an existential extension to pattern matching.
Additionally, you can find similar a similar concept in the
OCaml-implemented proof assistant Coq with the introduction of inductive
data types\footnote{\url{http://adam.chlipala.net/cpdt/html/InductiveTypes.html\#:\~:text=Coq\%20inductive\%20types\%20generalize\%20the,the\%20possibility\%20for\%20type\%20dependency}}.
Constraints applied to a value constructor can be applied in a similar
manner to pattern matching. However, instead of using a specified value
with a specific datatype, we can instead construct a generalized type
and us this when applying it to a function which computes similar to
pattern matching\footnote{\url{https://caml.inria.fr/pub/docs/manual-ocaml/gadts.html}}.
\begin{verbatim}
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term;;
(* type _ term =
Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term *)
let rec eval : type a. a term -> a = function
| Int n -> n
| Add -> (fun x y -> x+y)
| App(f,x) -> (eval f) (eval x);;
(* val eval : 'a term -> 'a = *)
let two = eval (App (App (Add, Int 1), Int 1));;
(* val two : int = 2 *)
\end{verbatim}
\subsection{Lisp Macros \& Syntax Extension}
\label{sec:orgecae3f9}
As OCaml, and the ML-family come from the tradition of LISP, you can
often find OCaml to have many of the niceties that come bundled with
the expressive power of LISP-dialects. If you have used LISP, you know
that the language itself is intrinsically extensible, meaning that
you can extend the language itself without recompiling (using macros).
This same power is also found in the OCaml language using the
preprocessor-pretty-printer of OCaml, \texttt{camlp5} (which has replaced
and deprecated \texttt{camlp4}\footnote{\url{https://whitequark.org/blog/2014/04/16/a-guide-to-extension-points-in-ocaml/}}).
More information about this functionality can be found \href{https://camlp5.github.io/doc/html/}{here}.
\section{Projects using OCaml}
\label{sec:org1af0324}
Here is an unorganized list of projects that I enjoy which are using
OCaml.
\begin{itemize}
\item \href{https://mirage.io/}{MirageOS - Unikernels}
\item \href{https://github.com/RedPRL/cooltt}{CoolTT - Cartestian Cubical Type Theory Proof Assistant}
\item \href{http://frama-c.com/}{Frama-C - Extensible Static Software Analyzer}
\item \href{http://compcert.inria.fr/research.html}{CompCert - Formally Verified C99 Compiler} (Note: This is \emph{non-free} software)
\item \href{https://coq.inria.fr/}{Coq - Proof Assistant}
\item \href{https://www.fstar-lang.org/}{F* - An effectful formally verified language}
\item \href{https://reasonml.github.io/}{ReasonML - ML-style/Javascript ecosystem}
\item \href{http://why3.lri.fr/}{Why3 - Deductive Program Verification}
\item \href{http://lablgtk.forge.ocamlcore.org/}{Lablgtk - Stubless GTK Bindings for OCaml}
\item \href{https://ocaml.xyz/}{OWL - OCaml for Scientific Computing}
\item \href{https://camlp5.github.io/}{Camlp5 - Preprocessor-Pretty-Printer of OCaml}
\end{itemize}
\section{Tutorials for OCaml}
\label{sec:orgd0ed4de}
Great! Perhaps you are convinced of some of the functionality of OCaml
and you are now looking for some actual tutorials that teach you how
to do things.
\begin{itemize}
\item \href{http://roscidus.com/blog/blog/2014/06/06/python-to-ocaml-retrospective/}{Python to OCaml}
\item \href{https://learnxinyminutes.com/docs/ocaml/}{Learn OCaml in Y Minutes}
\item \href{https://queue.acm.org/detail.cfm?id=2038036}{OCaml for the Masses}
\item \href{https://dev.realworldocaml.org/}{Real World OCaml}
\item \href{http://www.cs.cornell.edu/courses/cs3110/2020sp/}{CS 3110 - Data Structures and Functional Programming @ Cornell University}
\item \href{https://github.com/ocaml-community/awesome-ocaml\#algorithms-and-data-structures}{Awesome OCaml}
\end{itemize}
\noindent\rule{\textwidth}{0.5pt}
\section*{Have a response?}
\label{sec:org3946c1d}
Responses and discussion pertaining to any of the blog entries on my
website are welcome! Start a discussion on the \href{https://lists.sr.ht/\~brettgilio/blog-discussion}{mailing list} by sending
an email to \href{mailto:\~brettgilio/blog-discussion@lists.sr.ht}{\textasciitilde{}brettgilio/blog-discussion@lists.sr.ht}.
\section*{Errata:}
\label{sec:orgd35c271}
\begin{itemize}
\item \textit{<2020-09-03 Thu 18:03> } Correct some typos and ambiguous language.
\end{itemize}
\noindent\rule{\textwidth}{0.5pt}
\end{document}