{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-} -- for spurious reasons
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
-- Reproducing the Scala Cake pattern
{- The pattern is well explained in
http://events.inf.ed.ac.uk/Milner2012/slides/Odersky/Odersky.pdf
(slides 12-18) as well as in Section 4 of
Scalable Component Abstractions
Martin Odersky and Matthias Zenger, EPFL Lausanne
OOPSLA 2005
http://lampwww.epfl.ch/~odersky/papers/ScalableComponent.html
The pattern has been illustrated on the example from the Scala
compiler, which has to track (term) identifiers such as variables and
constants, and their types. Scala is an OO language, so the types are
class types. Thus identifiers have types, types can be class types,
and components (members) of a class are identifiers. Hence the mutual
dependence between identifiers and types.
The common example for the Cake pattern can be described by the
following two mutually dependent interfaces, in OCaml syntax.
module type Term = sig
type t (* abstract: identifiers *)
val typeof : t -> Type.ctype (* The type of an identifier *)
val new : string -> t (* Enter a new identifier. If the
identifier was already entered, return
the old id. That is:
eq (new name) (new name) === true
If the entered identifier has not been
seen before, it is associated with a type
variable (yet undetermined type).
*)
val enter : t -> Type.ctype -> unit (* Associate a type with an identifier:
unify the given type and the already
associated type.
*)
val show : t -> string
val eq : t -> t -> bool
end
module type Type = sig
type t (* abstract: representation of a type *)
type ctype = t * t (* The first component: the class type of
a method (this-type). The second: the result type.*)
val members : t -> Term.t list (* All members of a class *)
val tvar : unit -> t (* A new type variable *)
val new : string -> t (* Enter the name of a class,
eq (new name) (new name) == true
*)
val add : t -> Term.t -> unit (* Add a new member to the class *)
val unify : t -> t -> unit (* throw an exception otherwise *)
val show : t -> string
val eq : t -> t -> bool
end
Requirements:
- support mutual dependence between Term and Type;
- maintain abstraction (encapsulation) for Term.t and Type.t
to let us swap one implementation for another, e.g., to transparently
add hash-consing. We show off the encapsulation
by swapping one implementation of Term with the extended one,
which logs all created identifiers.
- separate compilation of Term and Type implementation;
- make it possible to have several instances of
Term or Type signatures within the same
program without mixing them up: One may compare
Term.t within the same Term instance but not between
different instances. That is, each new implementation/instance
of Term should have distinct Term.t.
- avoid public or private global mutable state (static data)
(the compiler must be reentrant: needed for Eclipse plug-ins)
- instances of Term and Type must be first class
(in ML terms, we need first-class modules)
The problem is to implement this pattern in Haskell.
The paper and the slides stress the crucial role of Scala self-types.
In Haskell it corresponds to an unusual type class instance selection
mechanism. Normally instances are selected based on the concrete type.
For example:
class Term repr where
instance Term VTable
Here the instance is selected based on a concrete type of repr being
VTable. To emulate Scala's self-types, we need to select on a part of
repr. Suppose repr is a tuple. Then
instance Term (VTable,s) ...
selects based on the first component of the tuple, for any possible
second component. However, we don't want to commit to repr being
necessarily a tuple, and VTable is the first component. It could be
the second component, so long as we can unambiguously find it in
repr. So we need to abstract from the details of repr
structure. Suppose we have
class Lens part whole where
extract :: whole -> part
update :: part -> whole -> whole
establishing a lens (reader/updater) between a type whole and its `component'
part. For example, whole may be a tuple and part may be one of its components.
Then we would like to write
class Term repr
instance Lens VTable repr => Term repr
instance Lens VTableAnother repr => Term repr
where the first instance is chosen if repr has a component named VTable.
Here is another hypothetical implementation of the pattern. Suppose an
argument of a type could be a type-level record
data Repr {term_part: t1, typ_part: p2} = ...
instance Term Repr{term_part: VTable}
Here we do not care of the order of the labels in Repr's argument, only on
the existence of the label term_part of the type VTable.
We can closely emulate this record approach. Here is the outline:
type family TermPart repr :: *
type family TypPart repr :: *
newtype Proj s repr = Proj repr
the intent here is that TermPart repr returns Proj s repr
(e.g. if repr = tuple (TTable,VTable) then
TermPart (TTable,VTable) = Proj VTable (TTable,VTable)
instance (Term (TermPart repr)) => Term repr -- dispatch
instance Lens VTable repr => Term (Proj VTable repr) where -- real instance
This approach requires overlapping instances, or class duplication.
In this code we implement a slightly different, and simpler, approach, taking
advantage of the fact that we already have something like
type family TermPart repr :: *
We have a type family Vt to associate with the type of the identifiers with
the implementation of Term. In other words, we need to associate Term with
Term.t. We define
class Term repr vt where
typeof :: vt -> repr -> Ctyp repr
and write
instance Lens (VTable repr) repr => Term repr (VN repr)
selecting not on VTable (the concrete type of Term) but on the concrete
type of Term.t. The result is the same -- we select on a specific
part of repr without knowing the precise structure of repr.
In our case all operations within Term mention Term.t -- so the dispatch
works. If we had an operation in Term that doesn't mention Term.t --
for example, debug_print :: repr -> String, we should add another
vt-like key (and another parameter to the Term class).
As a matter of fact, the full instance declaration has the form
instance (SymbolCtx repr, TypCtx repr, Lens (VTable repr) repr) =>
Term repr (VN repr) where
It defines the concrete implementation of the Term interface (where
Term.t is VN repr) and *abstractly* refers to the implementation of the
Typ interface (TypCtx). It also abstractly refers to a symbol table,
used for hash-consing names. Compare with Scala code from slide 17
trait Symbols { this: Types with Symbols =>
trait Symbol { def tpe: Type }
}
(we call Symbols Term and Types Typ.)
The type of run
run :: Monad m =>
(forall t. (TermCtx t, TypCtx t) => StateT t m a) -> m a
makes sure that the computation to be run uses only the Term and
Typ interface and knows nothing at all about their concrete implementations.
-}
module ScalaCake where
import qualified Data.Map as M
import Control.Monad.State
-- import Control.Monad.Trans.State
-- In real life we will have separate modules for separate implementations
-- of Types and Terms. For the sake of illustration, we combine all
-- the modules in a single file. We do indicate module boundaries in comments.
-- ------------------------------------------------------------------------
-- Interfaces (mutually recursive)
type family Vt repr :: * -- corresponds to Term.t
type family Tt repr :: * -- corresponds to Type.t
type Name = String -- concrete name
type ErrMsg = String -- error message
-- First we define the pure implementation (and turn into a monad later)
-- Unlike the OCaml interface in the comments, here we are explicit
-- about all effects.
-- repr is some implementation of the Term table. Vt repr is
-- the type of identifiers associated with that table.
class Term repr vt where
typeof :: vt -> repr -> Ctyp repr
vnew :: Name -> repr -> (vt, repr)
venter :: vt -> Ctyp repr -> repr -> Either ErrMsg repr
vshow :: vt -> repr -> String
-- The complete interface for Term
type TermCtx repr = (Term repr (Vt repr), Eq (Vt repr), Show (Vt repr))
type Ctyp repr = (Tt repr, Tt repr)
class Typ repr tt where
tvar :: repr -> (tt, repr)
tnew :: Name -> repr -> (tt, repr)
add :: tt -> Vt repr -> repr -> repr
unify :: tt -> tt -> repr -> Either ErrMsg repr
members :: tt -> repr -> [Vt repr]
tshow :: tt -> repr -> String
-- The complete interface for Typ
type TypCtx repr = (Typ repr (Tt repr), Eq (Tt repr), Show (Tt repr))
-- Turn the pure interface into a monadic one
type MTermCtx repr m = (Monad m, MonadState repr m, TermCtx repr)
mtypeof :: MTermCtx repr m => Vt repr -> m (Ctyp repr)
mtypeof v = do
repr <- get
return $ typeof v repr
mvnew :: MTermCtx repr m => Name -> m (Vt repr)
mvnew name = do
repr <- get
let (t,repr') = vnew name repr
put repr'
return t
mventer :: MTermCtx repr m => Vt repr -> Ctyp repr -> m ()
mventer v typ = do
repr <- get
case venter v typ repr of
Left err -> fail err
Right repr -> put repr
mvshow :: MTermCtx repr m => Vt repr -> m String
mvshow t = do
repr <- get
return $ vshow t repr
type MTypCtx repr m = (Monad m, MonadState repr m, TypCtx repr)
mtnew :: MTypCtx repr m => Name -> m (Tt repr)
mtnew name = do
repr <- get
let (t,repr') = tnew name repr
put repr'
return t
-- Add a new method to the class
mnew :: (MTypCtx repr m, MTermCtx repr m) => Vt repr -> Ctyp repr -> m ()
mnew v clt@(tclass, tresult) = do
repr <- get
case venter v clt (add tclass v repr) of
Left err -> fail err
Right repr -> put repr
mtshow :: MTypCtx repr m => Tt repr -> m String
mtshow t = do
repr <- get
return $ tshow t repr
mmembers :: MTypCtx repr m => Tt repr -> m [Vt repr]
mmembers t = do
repr <- get
return $ members t repr
ap2 :: Monad m => (a -> b -> m c) -> m a -> m b -> m c
ap2 f ma mb = do
a <- ma
b <- mb
f a b
-- ------------------------------------------------------------------------
-- Example
-- Make the initial environment, with built-in identifiers and classes
prelude = do
tstr <- mtnew "String" -- the string class
tint <- mtnew "Int" -- the Int class
-- Enter method String.length : Int
ap2 mnew (mvnew "length") (return (tint,tstr))
-- Enter method Int.toString : String
ap2 mnew (mvnew "toString") (return (tstr,tint))
-- An example of using the Term and Typ tables, given the prelude
-- The examples are meant to look quite like Scala code in
-- code fragments on Odersky's slides.
ex1 = do
liftIO.putStrLn $ "Debugging printing: showing the identifiers"
liftIO.print =<< mvnew "toString"
liftIO.print =<< mvnew "length"
liftIO.print =<< mvnew "length" -- should be the same ident
liftIO.print =<< mtnew "Int"
liftIO.print =<< mtnew "String"
liftIO.print =<< mtnew "String"
liftIO.putStrLn $ "check mvnew invariant"
liftIO.print =<< (liftM2 (==) (mvnew "length") (mvnew "length"))
liftIO.putStrLn $ "check mtnew invariant"
liftIO.print =<< (liftM2 (==) (mtnew "Int") (mtnew "Int"))
-- print the type of the length method
(tclass,tresult) <- mtypeof =<< mvnew "length"
liftIO.putStrLn $ "length method"
liftIO.print $ tclass
liftIO.print $ tresult
liftIO.print =<< mtshow tclass
liftIO.print =<< mtshow tresult
liftIO.putStrLn $ "Members of Int"
liftIO.print =<< mapM mvshow =<< mmembers =<< mtnew "Int"
-- ------------------------------------------------------------------------
-- Putting it all together
-- Combining concrete implementations of Term and Typ to actually run the
-- examples
with_symbol_table :: (forall table. SymbolCtx table => table -> w) -> w
with_symbol_table body = body makeSymbMap
class Lens part whole where
extract :: whole -> part
update :: part -> whole -> whole
-- Specialized instances of Len's methods, to keep the same repr
extr :: Lens (part repr) repr => repr -> part repr
extr = extract
upd :: Lens (part repr) repr => part repr -> repr -> repr
upd = update
data Tables sym vt tt =
Tables sym -- symbol table
(vt (Tables sym vt tt)) -- Term table
(tt (Tables sym vt tt)) -- Typ table
instance (Tables sym vt tt) ~ repr => Lens (vt repr) (Tables sym vt tt) where
extract (Tables s v t) = v
update v (Tables s _ t) = Tables s v t
instance Lens (tt (Tables sym vt tt)) (Tables sym vt tt) where
extract (Tables s v t) = t
update t (Tables s v _) = Tables s v t
-- mutually recursive only at the type level
-- only here concrete types show up
makeTables :: SymbolCtx sym => sym -> Tables sym VTable TTable
makeTables sym = Tables sym makeVTable makeTTable
type instance Vt (Tables sym VTable tt) = VN (Tables sym VTable tt)
type instance Tt (Tables sym vt TTable) = TN (Tables sym vt TTable)
run :: Monad m =>
(forall t. (TermCtx t, TypCtx t) => StateT t m a) -> m a
run m = with_symbol_table (\sym -> evalStateT m (makeTables sym))
ex1run :: IO ()
ex1run = run (prelude >> ex1)
-- Show the absence of mix-up
-- Actually, we've seen that before (in SymbolTable.lhs)
-- The higher-rank type of run prevents any mix-ups.
-- ------------------------------------------------------------------------
-- Our implementation of Term and Typ relies on Symbols, interned strings.
-- Here is the abstract interface, which is the only thing available to
-- Term and Typ implementations. Therefore, we can easily swap one
-- method of interning for another.
class SymbolTable rep where
type Symbol rep :: * -- the type of the symbol
intern :: Name -> rep -> (Symbol rep, rep) -- intern a symbol
extern :: Symbol rep -> rep -> String
gensym :: String -> rep -> (Symbol rep, rep)
-- The alias for the set of constraints representing the table
-- (in other words, all interfaces the table is meant to implement)
type SymbolCtx rep = (SymbolTable rep, Show (Symbol rep),
Eq (Symbol rep), Ord (Symbol rep))
-- ------------------------------------------------------------------------
-- One implementation of the Term signature
-- It should be in a separate module
-- This concrete implementation of Term uses the abstract implementations
-- of Typ and the Symbol table. See in particular, the implementation of vnew
-- (which uses Typ.tvar) and venter (which uses unify).
-- Only the type VTable, but not the data constructor is exported
data VTable s = VTable (M.Map (Symbol s) (Ctyp s))
makeVTable :: (SymbolCtx s, TypCtx s) => VTable s -- also exported
makeVTable = VTable M.empty
-- Only the type VN, but not the data constructor is exported
newtype VN s = VN (Symbol s)
instance SymbolCtx s => Eq (VN s) where
VN s1 == VN s2 = s1 == s2
instance SymbolCtx s => Show (VN s) where -- for debugging
show (VN s) = "VN:" ++ show s
-- Compare with Self-type in Scala (shown in the comments above)
instance (SymbolCtx repr, TypCtx repr, Lens (VTable repr) repr) =>
Term repr (VN repr) where
typeof (VN key) repr =
let (VTable m) = extr repr in
M.findWithDefault (error "typeof: can't find") key m
vshow (VN key) repr =
extern key repr
vnew name repr =
let (key,r1) = intern name repr
VTable m1 = extr r1
in case M.lookup key m1 of
Just _ -> (VN key, r1) -- name already seen
Nothing ->
let (tclass,r2) = tvar r1
(tresult,r3) = tvar r2
VTable m2 = extr r3
in (VN key, upd (VTable (M.insert key (tclass,tresult) m2)) r3)
venter v (tclass,tresult) repr =
let (tclass0,tresult0) = typeof v repr in
case unify tclass tclass0 repr of
Left err -> Left err
Right repr -> case unify tresult tresult0 repr of
Left err -> Left err
Right repr -> Right repr
-- ------------------------------------------------------------------------
-- One implementation of the Typ signature
-- It should be in a separate module
-- This concrete implementation of Typ uses abstract implementation
-- of Term and the symbol table.
-- Only the type TTable, but not the data constructor is exported
data TTable s =
TTable (M.Map (Symbol s) (TDescr s)) -- list of members for a class
data TDescr s = TLink (Symbol s) -- bound type variable
| TClass [Vt s] -- list of methods
-- Unbound type variables aren't
-- in the map
makeTTable :: (SymbolCtx s, TermCtx s) => TTable s -- also exported
makeTTable = TTable M.empty
-- Only the type TN, but not the data constructor is exported
newtype TN s = TN (Symbol s)
instance SymbolCtx s => Eq (TN s) where
TN s1 == TN s2 = s1 == s2
instance SymbolCtx s => Show (TN s) where -- for debugging
show (TN s) = "TN:" ++ show s
-- Compare with Self-type in Scala
instance (SymbolCtx repr, TermCtx repr, Lens (TTable repr) repr) =>
Typ repr (TN repr) where
tvar repr =
let (key,r1) = gensym "TVAR" repr
in (TN key, r1)
tshow (TN key) repr =
case chase key repr of
Nothing -> extern key repr
Just (key,_) -> extern key repr
members (TN key) repr =
case chase key repr of
Nothing -> error "members: TVar"
Just (_,x) -> x
tnew name repr =
let (key,r1) = intern name repr
TTable m = extr r1
in case M.lookup key m of
Just _ -> (TN key, r1) -- already seen
Nothing -> (TN key, upd (TTable (M.insert key (TClass []) m)) r1)
add (TN key) v repr =
let (TTable m) = extr repr in
case chase key repr of
Nothing -> error "add: lookup"
Just (key,x) -> upd (TTable (M.insert key (TClass (v:x)) m)) repr
unify (TN key1) (TN key2) repr =
let (TTable m) = extr repr in
if key1 == key2 then Right repr
else case (chase key1 repr, chase key2 repr) of
(Nothing, _) -> Right $
upd (TTable (M.insert key1 (TLink key2) m)) repr
(_,Nothing) -> Right $
upd (TTable (M.insert key2 (TLink key1) m)) repr
(Just (key1,x1), Just (key2,x2)) ->
if key1 == key2 || x1 == x2 then Right repr
else Left "unification failed"
chase :: (Lens (TTable repr) repr, SymbolCtx repr) =>
Symbol repr -> repr -> Maybe (Symbol repr, [Vt repr])
chase key rep = case M.lookup key m of
Nothing -> Nothing
Just (TLink key) -> chase key rep
Just (TClass x) -> Just (key,x)
where TTable m = extr rep
-- ------------------------------------------------------------------------
-- One implementation of Symbol table
-- We use a naive implementation of symbol tables. One can do much better,
-- for example, using Hashes. The efficiency is not the issue here; after
-- all, the implementation is well encapsulated and can be changed
-- at any moment.
-- Only SymbMap type, but NOT the data constructor is exported
newtype SymbMap = SymbMap (M.Map String (Symbol SymbMap))
data SN = Symbol
Int -- symbol code
String -- the string itself, from the set
instance SymbolTable SymbMap where
type Symbol SymbMap = SN
intern str (SymbMap m)
| Just s <- M.lookup str m = (s,SymbMap m)
| otherwise = let i = M.size m
s = Symbol i str
in (s,SymbMap (M.insert str s m))
extern (Symbol _ str) _ = str
gensym base rep@(SymbMap m) =
let i = M.size m in
intern (base ++ show i) rep
makeSymbMap = SymbMap M.empty
instance Show SN where
show (Symbol i str) = str ++ ":" ++ show i
-- We compare symbol's codes, `pointers':
instance Eq SN where
Symbol i1 _ == Symbol i2 _ = i1 == i2
instance Ord SN where
compare (Symbol i1 _) (Symbol i2 _) = compare i1 i2
getSym :: Tables sym vt tt -> sym
getSym (Tables sym _ _) = sym
putSym :: Tables sym vt tt -> sym -> Tables sym vt tt
putSym (Tables sym v t) sym' = Tables sym' v t
instance SymbolCtx sym => SymbolTable (Tables sym vt tt) where
type Symbol (Tables sym vt tt) = Symbol sym
intern name rep =
let (x,sym') = intern name (getSym rep)
in (x,putSym rep sym')
extern x rep = extern x (getSym rep)
gensym name rep =
let (x,sym') = gensym name (getSym rep)
in (x,putSym rep sym')