{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-} -- for spurious reasons
-- 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 Terms = sig
type t (* abstract: identifiers *)
val typeof : t -> Types.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.sctype -> 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 Types = 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 -> Terms.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 -> Terms.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 Terms and Types;
- maintain abstraction (encapsulation) for Terms.t and Types.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 Terms with the extended one,
which logs all created identifiers.
- separate compilation of Terms and Types implementation;
- make it possible to have several instances of
Terms or Types signatures within the same
program without mixing them up: One may compare
Terms.t within the same Terms instance but not between
different instances. That is, each new implementation/instance
of Terms should have distinct Terms.t.
- avoid public or private global mutable state (static data)
(the compiler must be reentrant: needed for Eclipse plug-ins)
- instances of Terms and Types must be first class
(in ML terms, we need first-class modules)
The problem is to implement this pattern in Haskell. (We will call
Terms.t as TermID and Types.t as TypeID)
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 Terms repr where
instance Terms 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 Terms (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 Terms repr
instance Lens VTable repr => Terms repr
instance Lens VTableAnother repr => Terms 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 {terms_part: t1, typ_part: p2} = ...
instance Terms Repr{terms_part: VTable}
Here we do not care of the order of the labels in Repr's argument, only on
the existence of the label terms_part of the type VTable.
We can closely emulate this record approach. Here is the outline:
type family TermsPart repr :: *
type family TypesPart repr :: *
newtype Proj s repr = Proj repr
the intent here is that TermsPart repr returns Proj s repr
(e.g. if repr = tuple (TTable,VTable) then
TermsPart (TTable,VTable) = Proj VTable (TTable,VTable)
instance (Terms (TermsPart repr)) => Terms repr -- dispatch
instance Lens VTable repr => Terms (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 TermsPart repr :: *
We have a type family Vt to associate with the type of the identifiers with
the implementation of Terms. In other words, we need to associate Terms with
Terms.t (TermID) We define
class Terms repr vt where
typeof :: vt -> repr -> Ctyp repr
and write
instance Lens (VTable repr) repr => Terms repr (VN repr)
selecting not on VTable (the concrete type of Terms) but on the concrete
type of TermID. 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 Terms mention TermID -- so the dispatch
works. If we had an operation in Terms that doesn't mention TermID --
for example, debug_print :: repr -> String, we should add another
vt-like key (and another parameter to the Terms class).
As a matter of fact, the full instance declaration has the form
instance (SymbolCtx repr, TypesCtx repr, Lens (VTable repr) repr) =>
Terms repr (VN repr) where
It defines the concrete implementation of the Terms interface (where
TermID is VN repr) and *abstractly* refers to the implementation of the
Types interface (TypesCtx). 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 Terms.)
The type of run
run :: Monad m =>
(forall t. (TermsCtx t, TypesCtx t) => StateT t m a) -> m a
makes sure that the computation to be run uses only the Terms and
Types interface and knows nothing at all about their concrete implementations.
-}
module ScalaCake where
-- import interfaces
import TTCl
import SymbolCl
import Lens
import Control.Monad.State
-- import the implementations
import Terms
import Types
import qualified Symbols as S
import qualified TermsD -- the debug version
-- 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))
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
-- An example of using the Terms and Types 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"
ex1run :: IO ()
ex1run = run (prelude >> ex1)
-- Show the absence of mix-up
-- The higher-rank type of run prevents any mix-ups.
ex2 = run $ do
liftIO.putStrLn $ "Several instances of the `compiler' (Table)"
(tclass1,tresult1) <- mtypeof =<< mvnew "length"
length1 <- mvnew "length"
prelude
-- nested instantiation
run $ do
prelude
(tclass2,tresult2) <- mtypeof =<< mvnew "length"
(tclass2',tresult2') <- mtypeof =<< mvnew "toString"
return $ tclass2 == tclass2'
length2 <- mvnew "length"
length2' <- mvnew "length"
-- If we uncomment the statement below
-- we get an error that
-- Could not deduce (Tt t ~ Tt t1)
-- The types of type class identifiers are distinct
-- return $ tclass1 == tclass2'
return $ length2 == length2'
-- Likewise, if we uncomment the statement below we get an error
-- Could not deduce (Vt t1 ~ Vt t)
-- return $ length2 == length1
-- Running ex1 with a debug version of Terms (tracing on typeof)
-- The instances below show all we need to do to replace one
-- version of a Terms component with another. Essentially, we
-- update the final assembly. The Types component is unaffected,
-- although it does depend on Terms and uses the type of identifiers
-- exported by Terms (different for Terms and TermsD)
ex1runD :: IO ()
ex1runD = runD (prelude >> ex1)
where
runD :: Monad m =>
(forall t. (TermsCtx t, TypesCtx t) => StateT t m a) -> m a
runD m = S.with_symbol_table (\sym -> evalStateT m (makeTables sym))
makeTables sym = Tables sym TermsD.makeVTable makeTTable
type instance Vt (Tables sym TermsD.VTable tt) =
TermsD.VN (Tables sym TermsD.VTable tt)
instance Lens (TermsD.VTable (Tables sym TermsD.VTable tt))
(Tables sym TermsD.VTable tt) where
extract (Tables s v t) = v
update v (Tables s _ t) = Tables s v t
-- ------------------------------------------------------------------------
-- Putting it all together
-- Combining concrete implementations of Terms and Types to actually run the
-- examples
data Tables sym vt tt =
Tables sym -- symbol table
(vt (Tables sym vt tt)) -- Terms table
(tt (Tables sym vt tt)) -- Types table
instance Lens (VTable (Tables sym VTable tt)) (Tables sym VTable 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
-- boiler-plate instance, for illustration of the boilerplate
-- It can be avoided as shown in Terms and Types components.
-- Also, we could have avoided boilerplate with closed type families
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')
-- 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. (TermsCtx t, TypesCtx t) => StateT t m a) -> m a
run m = S.with_symbol_table (\sym -> evalStateT m (makeTables sym))