{-# 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')