{-# LANGUAGE RankNTypes #-}
-- Tagless-final and Universal Algebra
module Algebra where
import Prelude hiding (and,or)
{- 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
-}
class SYM repr where
lit :: Bool -> repr
neg :: repr -> repr
and :: repr -> repr -> repr
or :: repr -> repr -> repr
-- This is an algebraic signature. What is Algebra? What is an algebraic
-- signature?
-- http://okmij.org/ftp/tagless-final/Algebra.html
-- Sample term
exO :: SYM repr => repr
exO = neg (lit False)
{-
In our case, lit True and lit False are two 0-arity operations (constants),
neg is arity 1 and `and` and `or`, often written in infix, are of arity 2.
The SYM signature introduces the set of operations (which I just named)
and their arities.
-}
newtype R = R Bool deriving Show
instance SYM R where
lit x = R x
neg (R x) = R $ not x
and (R x) (R y) = R (x && y)
or (R x) (R y) = R (x || y)
{- It is one of the algebras of the SYM signature. The carrier set is
Haskell boolean values (tagged with R),
and lit True, lit False, neg. etc. are the
operations, *total functions* on these values.
-}
newtype S0 = S0 String deriving Show
instance SYM S0 where
lit x = S0 $ if x then "tt" else "ff"
neg (S0 x) = S0 $ "~" ++ x
and (S0 x) (S0 y) = S0 $ paren $ x ++ " && " ++ y
or (S0 x) (S0 y) = S0 $ paren $ x ++ " || " ++ y
paren :: String -> String
paren x = "(" ++ x ++ ")"
{- This is another SYM algebra -- this time with an infinite carrier set:
set of all Haskell strings (tagged with S0)
-}
{-
exO :: R
R True
exO :: S0
S0 "~ff"
A SYM term exO, like |neg (lit False)| means (R True) value
according to the
R semantics, and the string S0 "~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 Haskell:
-}
data Sym = Sym (forall repr. SYM repr => repr)
{-
Different implementations of |SYM| generally choose different
concrete types for |repr|~-- therefore the type |Sym| stands for a
polymorphic function. Moreover, |Sym| is the first-class
polymorphic function: we do want to pass terms as arguments to other
functions.
-}
{- 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 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.
-}
type SymSelf = Sym
instance SYM Sym where
lit x = Sym (lit x)
neg (Sym e) = Sym (neg e)
and (Sym e1) (Sym e2) = Sym (and e1 e2)
or (Sym e1) (Sym e2) = Sym (or e1 e2)
-- Sample term, again
-- compare with exO! The term is the same, but the signature differs!
ex0 :: SymSelf
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
h :: SYM repr => SymSelf -> repr
h (Sym e) = e
{- Let us verify that operations are `respected',
using S0 algebra as an example.
-}
{-
h (SYMSelf.lit False) = (lit False)::S0
For all SYMSelf term e,
h (SYMSelf.neg e) = (neg (h e))::S0
-}
{- 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
-}
t0 = h ex0 :: S0
-- S0 "~ff"
{-
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.
-}
ex1 :: SymSelf
ex1 = lit True `and` (neg (lit False)) -- earlier example, in Ocaml code
view :: SymSelf -> String
view (Sym e) = let S0 x = e in x
t1 = view ex1
-- "(tt && ~ff)"
{- 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*.
-}
{- Can we introduce `variables' without changing the signature?
Just remaining to be a SYM algebra?
-}
-- Let's consider a few motivating examples
exx1 :: SYM repr => repr -> repr
exx1 x = lit True `and` (neg x)
exx2 :: SYM repr => (repr,repr) -> repr
exx2 (x,y) = (x `or` y) `and` (neg (x `and` y))
t2 = exx2 (S0 "x",S0 "y") :: S0
-- S0 "((x || y) && ~(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
-}
-- In OCaml code algebra.ml,
-- we could get away with giving the simple names like 'x', 'y', 'z'
-- for the wires. OCaml has a proper module system that lets us restrict
-- the scope of such popular names and prevent name conflicts.
-- No such luck in Haskell
data Wires repr = Wires {wire_x, wire_y, wire_z :: repr}
exx3 :: SYM repr => Wires repr -> repr
exx3 w = (wire_x w `or` wire_y w) `and` (neg (wire_x w `and` wire_y w))
-- Moreover
data SYMFree names = SF (forall repr. SYM repr => names repr -> repr)
instance SYM (SYMFree names) where
lit x = SF (\_ -> lit x)
neg (SF e) = SF (\env -> neg (e env))
and (SF e1) (SF e2) = SF (\env -> and (e1 env) (e2 env))
or (SF e1) (SF e2) = SF (\env -> or (e1 env) (e2 env))
-- The above shows that 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
-}
h' :: SYM repr => -- target algebra A
names repr -> -- the function h: wire assignment
SYMFree names -> -- free algebra term
repr
h' env (SF e) = e env
exx4 :: SYMFree Wires
exx4 =
let x = SF wire_x
y = SF wire_y
in
(x `or` y) `and` (neg (x `or` y))
t4 = h' (Wires (S0 "x") (S0 "y") (S0 "z")) exx4
-- S0 "((x || y) && ~(x || y))"
{- 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.
-}
-- In Haskell, exx4 and exx3 are actually quite similar