(* Tagless-final and Universal Algebra *)
(* Recall SYM *)
module type SYM = sig
type repr
val lit : bool -> repr
val neg : repr -> repr
val (&&) : repr -> repr -> repr
val (||) : repr -> repr -> repr
end
(* This is an algebraic signature. What is Algebra? What is an algebraic
signature?
http://okmij.org/ftp/tagless-final/Algebra.html
*)
(*
In our case, lit true and lit false are two 0-arity operations (constants),
neg is arity 1 and (&&) and (||), written in infix, are of arity 2.
The SYM signature introduces the set of operations (which I just named)
and their arities.
*)
module R = struct
type repr = bool
let lit x = x
let neg = not
let (&&) = Stdlib.(&&)
let (||) = Stdlib.(||)
end
(* It is one of the algebras of the SYM signature. The carrier set is
OCaml boolean values, and lit true, lit false, neg. etc. are the
operations, *total functions* on these values.
*)
module S0 = struct
type repr = string
let paren : string -> string = fun x -> "(" ^ x ^ ")"
let lit x = if x then "tt" else "ff"
let neg x = "~" ^ x
let (&&) x y = paren @@ x ^ " && " ^ y
let (||) x y = paren @@ x ^ " || " ^ y
end
(* This is another SYM algebra -- this time with an infinite carrier set:
set of all OCaml strings
*)
(* A SYM term like |neg (lit false)| means OCaml true value according to the
R semantics, and the string "~ff" according to the S0 semantics.
But what |neg (lit false)| means *by itself*?
*)
(* A term embedded in the tagless-final style means whatever
its interpretation makes it to mean.
Technically, an embedded term may be regarded as a function that takes
an interpretation of its syntactic forms (i.e., an implementation of
its signature) and returns the |repr| value produced by that
implementation. To say it in OCaml:
*)
type sym = {e: 'a. (module SYM with type repr = 'a) -> 'a}
(*
Different implementations of |SYM| generally choose different
concrete types for |repr|~-- therefore the type |sym| stands for a
polymorphic function: there is a implicit |forall| before |'a.|,
quantifying that type variable. Moreover, |sym| is the first-class
polymorphic function: we do want to pass terms as arguments to other
functions. In OCaml, first-class polymorphic values have to be
embedded in a record (in our case, the record with the field |e|).
Since we chose modules for tagless-final signatures and
implementations, |sym|'s argument is a value of the
module type: OCaml has first-class modules. We could just as well
have used OCaml records or objects.
*)
(* Although |sym| is the glib technical answer to the question about
the inherent meaning of embedded terms, it could be taken
seriously. In fact, we may define a denotational semantics in which
our gate terms indeed mean |sym|.
It is the most banal~-- one may say, `syntactic'~-- implementation
of |SYM|. We show only the representative part; the reader may want to finish as
an exercise.
*)
module SYMSelf = struct
type repr = sym
let lit : bool -> repr = fun x ->
{e = fun (type a) (module I : SYM with type repr=a) -> I.lit x}
let neg : repr -> repr = fun {e=e} ->
{e = fun (type a) ((module I : SYM with type repr=a) as i) -> I.neg (e i)}
let (&&) : repr -> repr -> repr = fun {e=e1} {e=e2}->
{e = fun (type a) ((module I : SYM with type repr=a) as i) ->
I.((e1 i) && (e2 i))}
let (||) : repr -> repr -> repr = fun {e=e1} {e=e2}->
{e = fun (type a) ((module I : SYM with type repr=a) as i) ->
I.((e1 i) || (e2 i))}
end
(* Sample term *)
open SYMSelf
let ex0 = neg (lit false)
(* One can now say what |neg (lit false)| means `by itself': it tells how to
interpret itself, using whatever interpreter the user may provide.
That is, |neg (lit false)| takes an interpreter as an argument and directs it to
find the meanings of |lit false| and use the interpretation of |neg|
to build the complete denotation.
The `intrinsic' meaning of an embedded term is, hence, the guiding
of its interpretation according to its structure.
This is what *syntax* means, doesn't it?
*)
(*
One may say above more `mathematically': we have already mentioned
that |SYM| is an algebraic signature. Its implementations~--
|R|, |S0|, |SYMSelf| and many more to follow~-- are
hence |SYM|-algebras. Each algebra has its own set of |repr| values (the
carrier set), which supports |neg|, etc. operations.
*)
(* Of all |SYM|-algebras, |SYMSelf| is special: it is so-called
`word' algebra, which is an initial algebra. For any
|SYM|-algebra |A|, there is a unique total function
|SYMSelf.repr -> A.repr| that `respects' the operations: the unique
homomorphism.
*)
(* Indeed, here it is *)
let h : type arep. (module SYM with type repr = arep) -> SYMSelf.repr -> arep =
fun moduleA self -> self.e moduleA
(* Let us verify that operations are `respected',
using S0 algebra as an example.
*)
(*
h (SYMSelf.lit false) = S0.lit false
For all SYMSelf term e,
h (SYMSelf.neg e) = S0.neg (h e)
*)
(* Notice, any
implementation of a |SYM|-signature is exactly the definition of
that homomorphism. For example, passing the |S0| interpreter, as the
first-class--module argument, to a
|SYMSelf| term obtains the |S0|'s interpretation of the term
*)
let _ = h (module S0) ex0
let _ = ex0.e (module S0)
(*
Banal as it may be, |SYMSelf| is insightful, and also practically
useful. First of all, it lets us easily write terms and have them
interpreted.
*)
(* Earlier:
* let ex1 = type a. a symmod -> a = function (module I) -> let open I in
* lit true && (neg (lit false))
*)
let ex1 = lit true && (neg (lit false)) (* earlier example *)
let view : sym -> string = fun {e} -> e (module S0)
let _ = view ex1
(* Conclusion: in the tagless-final style, an interpreter is an algebra
defined by its homomorphism from the initial, word algebra
*)
(* Incidentally, the relationship between SYMSelf and the algebraic
datatype representing the SYM language is an instance of the
Yoneda Lemma
*)
(* SYM is rather boring, with only two constants lit false and lit true.
We need more zero-arity symbols, whose interpretation is not so
firmly baked-in. We need `propositional letters', which could be
interpreted *freely*.
*)
(* Earlier we introduced the propositional letters like wire_x by
extending the signature, to remind:
*)
module type SYMW = sig
include SYM
val wire_x : repr
val wire_y : repr
val wire_z : repr
end
(* As before, we can build the SYMW-word algebra (SYMW-initial algebra)
Can we introduce `variables' without changing the signature?
Just remaining to be a SYM algebra?
*)
(* Let's consider a few motivating examples *)
type 'a symmod = (module SYM with type repr = 'a)
let exx1 : type a. a symmod -> a -> a = function (module I) -> fun x ->
let open I in
lit true && (neg x)
let exx2 : type a. a symmod -> a*a -> a = function (module I) -> fun (x,y) ->
let open I in
(x || y) && (neg (x && y))
let _ = exx2 (module S0)
let _ = exx2 (module S0) ("x","y")
(* To generalize *)
(* Problem: how to generalize a, a*a, a*a*a, etc?
Ohad Kammar suggested that SYMW, with some pre-defined names, is all
that needed
*)
module type Wires = sig
type repr
val x : repr
val y : repr
val z : repr
val u : repr
val v : repr
end
type 'a wires = (module Wires with type repr = 'a)
let exx3 : type a. a symmod -> a wires -> a = fun (module I) (module W) ->
let open I in let open W in
(x || y) && (neg (x && y))
(* Moreover *)
module SYMFree = struct
type repr = {e: 'a. (module SYM with type repr = 'a) -> 'a wires -> 'a}
let up : SYMSelf.repr -> repr = fun {e} ->
{e = fun (type a) (module I : SYM with type repr=a) _ -> e (module I)}
let lit : bool -> repr = fun x ->
{e = fun (type a) (module I : SYM with type repr=a) _ -> I.lit x}
let neg : repr -> repr = fun {e=e} ->
{e = fun (type a) ((module I : SYM with type repr=a) as i) env ->
I.neg (e i env)}
let (&&) : repr -> repr -> repr = fun {e=e1} {e=e2}->
{e = fun (type a) ((module I : SYM with type repr=a) as i) env ->
I.((e1 i env) && (e2 i env))}
let (||) : repr -> repr -> repr = fun {e=e1} {e=e2}->
{e = fun (type a) ((module I : SYM with type repr=a) as i) env ->
I.((e1 i env) || (e2 i env))}
end
(* SYMFRee is a SYM algebra *)
(* If A is a SYM algebra with carrier A.repr and if
h : Env -> A.repr is any function mapping `variables' into A.repr,
then there exists a unique homomorphism
h': SYMFree.repr(Env) -> A.repr extending h,
that is, h'(SYMFree.x) = h(x) for any x in env
*)
(* Indeed, our h is an instance of Wires with type repr = a *)
let h' : type a.
a symmod -> (* target algebra A *)
a wires -> (* the function h: wire assignment *)
SYMFree.repr -> (* free algebra term *)
a
= fun i wires {e} -> e i wires
let exx4 : SYMFree.repr =
let open SYMFree in
let x = {e = fun (type a) _ (module W: Wires with type repr = a) -> W.x} in
let y = {e = fun (type a) _ (module W: Wires with type repr = a) -> W.y} in
(x || y) && (neg (x && y))
let _ = h' (module S0)
(module struct type repr = string
let (x,y,z,u,v) = ("x","y","z","u","v") end)
exx4
(* Such SYMFree is called a `freely generated algebra' (or, free algebra,
for short). Now you know what is free in free algebra. The set of
`variables' (our module Wires) is called `generators'.
Incidentally, free algebra is a fundamental notion, defined already
in Birkhoff's 1935 paper.
OTH, initial algebra as a term is more recent. Initial algebra
is a free algebra with the empty set of generators.
*)
(* Although exx4 is theoretically pleasing, exx3 is quite easier to write *)