liboleg 2010.1.2 → 2010.1.5

raw patch · 11 files changed

+2225/−3 lines, 11 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Control/StateAlgebra.hs +137/−0
• Data/Numerals.hs +77/−0
• Language/CBAny.hs +293/−0
• Language/CPS.hs +439/−0
• Language/TDPE.hs +165/−0
• Language/TTF.hs +242/−0
• Language/TTFdB.hs +212/−0
• Language/ToTDPE.hs +10/−0
• Language/Typ.hs +278/−0
• Language/TypeCheck.hs +359/−0
• liboleg.cabal +13/−3

@@ -0,0 +1,137 @@+{-# OPTIONS -fglasgow-exts #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Implementing the State Monad as a term algebra+--+-- <http://okmij.org/ftp/Haskell/types.html#state-algebra>+--+module Control.StateAlgebra where++import Control.Monad+import Control.Monad.State hiding (runState)++-- | Monadic actions are terms composed from the following constructors+--+data Bind t f   = Bind t f+data Return v   = Return v+data Get        = Get+data Put v      = Put v++-- | examples of terms+term1 = (Return True) `Bind` Put+term2 = Get `Bind` (\v -> Put (not v) `Bind` (\() -> Return v))++-- | An example of an ill-formed term+term_ill1 = Get `Bind` Get+-- | An example of an ill-typed term+-- The following term is ill-typed because it attempts to store both+-- a boolean and a character in the state. Our state can have only one type.+term_ill2 = Put True `Bind` (\() -> Put 'a')+++-- | The interpreter of monadic actions+-- It takes the term 't' and the initial state of the type 's'+-- and returns the final state and the resulting value. The type+-- of the result, 'a', is uniquely determined by the term and the state+--+class RunBind t s a => RunState t s a | t s -> a where+    runst :: t -> s -> (s,a)+++instance RunState (Return a) s a where+    runst (Return a) s = (s,a)+instance RunState Get s s where+    runst _ s = (s,s)+instance RunState (Put s) s () where+    runst (Put s) _ = (s,())+instance (RunState m s a, RunState t s b)+    => RunState (Bind m (a->t)) s b where+    runst (Bind m k) s = runbind m k s++-- | Interpretation of the Bind action requires an auxiliary class+-- This is due to the polymorphism of the monadic bind, which has the +-- type  +--+-- > m a -> (a -> m b) -> m b+--+-- Note the polymorphism both in 'a' (value type of the input monadic+-- action) and 'b' (value type of the resulting action)+--+class RunBind m s a where+    runbind :: RunState t s b => m -> (a->t) -> s -> (s,b)++instance RunBind (Return a) s a where+    runbind (Return a) k s = runst (k a) s++instance RunBind (Get) s s where+    runbind Get k s = runst (k s) s++instance RunBind (Put s) s () where+    runbind (Put s) k _ = runst (k ()) s++instance (RunBind m s x, RunState y s w)+    => RunBind (Bind m (x->y)) s w where+    runbind (Bind m f) k s+        = runbind m (\x -> Bind (f x) k) s++-- | We can now run (interpret) our sample terms+--+eterm1 = runst term1 False+-- (True,())++-- | term2 denoted the action of negating the current state and returning+-- the original state+eterm2 = runst term2 False+-- (True,False)++-- eterm_ill1 = runst term_ill1 True+-- The above gives an error message saying there is no rule+-- to interpret (Bind Get Get)+-- Indeed, this term is ill-formed.++-- eterm_ill2 = runst term_ill2 True+-- The error message says there is no rule (RunState (Put Char) Bool a)+-- That is, one can't store a Char in the state of the type Bool.+-- The above term is ill-typed indeed.+++-- | Now, we show that our term representation of the state monad +-- is an instance of MonadState+data Statte s a = forall t. RunState t s a => Statte t++instance RunState (Statte s a) s a where+    runst (Statte t) s = runst t s++instance RunBind (Statte s a) s a where+    runbind (Statte m) k s = runbind m k s++instance Monad (Statte s) where+    (Statte m) >>= f = Statte (Bind m (\x -> f x))+    return = Statte . Return++instance MonadState s (Statte s) where+    get = Statte Get+    put = Statte . Put++-- | We can write computations expressed by term1 and term2 using+-- the normal monadic syntax+--+-- The following identity function is to resolve polymorphism, to tell+-- that monadic terms below should use our representation of MonadState+as_statte :: Statte s a -> Statte s a+as_statte = id++-- term1 = (Return True) `Bind` Put+mterm1 = as_statte (return True >>= put)+emterm1 = runst mterm1 False+-- (True,())+++-- term2 = Get `Bind` (\v -> Put (not v) `Bind` (\() -> Return v))+mterm2 = as_statte $+	 do+	 v <- get+	 put (not v)+	 return v+emterm2 = runst mterm2 False+-- (True,False)

@@ -0,0 +1,77 @@+{-# OPTIONS -fglasgow-exts #-}++-- | Illustration of the 2-order lambda-calculus, +-- using Church numerals as an example.+-- The example shows limited impredicativity+--+-- <http://okmij.org/ftp/Haskell/types.html#some-impredicativity>+--++module Data.Numerals where++import Prelude hiding (succ, exp)++newtype N = N (forall a . (a -> a) -> a -> a)+un (N x) = x++zero :: N+zero = N ( \f a ->  a )++succ :: N -> N+succ n = N ( \f a -> f (un n f a) )++one:: N+one = succ zero++add, mul :: N -> N -> N+add m n = N( \f a -> un m f (un n f a)  )+mul m n = N( \f a -> un m (un n f) a )++exp :: N -> N -> N+exp m n = un n (mul m) one++exp2 :: N -> N -> N+exp2 m n = N (\f a -> un n (un m) f a)++test1 = un (exp two three) (+1) 0+    where two = succ one+	  three = succ two++test2 = un (exp2 two three) (+1) 0+    where two = succ one+	  three = succ two+++-- | Simpler illustrations of impredicativity+--+f1:: (forall a. a->a) -> b -> b+f1 g x = g x++testf1 = f1 id True+-- True++foo:: forall c notimportant. (c->c) -> notimportant+foo = undefined++{- the following gives an error+testf1' = foo f1++    Inferred type is less polymorphic than expected+      Quantified type variable `a' escapes+      Expected type: (a -> a) -> a -> a+      Inferred type: (forall a1. a1 -> a1) -> b -> b+    In the first argument of `foo', namely `f1'+    In the definition of `testf1'': testf1' = foo f1+-}+++newtype W = W{unW :: forall a. a -> a}++f2:: W -> b -> b+f2 g x = unW g x++testf2 = f2 (W id) True++testf2' = foo (\x -> W(f2 x))+-- testf2'' = foo (W . f2) -- can't use the composition+

@@ -0,0 +1,293 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- |+-- * Almost Haskell98. See CB98,hs for the genuine Haskell98 version+-- Here we use a few extensions to make the code prettier+--+-- * Embedding a higher-order domain-specific language (simply-typed+-- * lambda-calculus with constants) with a selectable evaluation order:+-- * Call-by-value, call-by-name, call-by-need+++module Language.CBAny where++import Data.IORef+import Control.Monad+import Control.Monad.Trans++-- | The (higher-order abstract) syntax of our DSL+type Arr exp a b = exp a -> exp b++class EDSL exp where+     int :: Int -> exp Int              -- This part is like before+     add :: exp Int -> exp Int -> exp Int+     sub :: exp Int -> exp Int -> exp Int++     lam :: (exp a -> exp b) -> exp (Arr exp a b)+     app :: exp (Arr exp a b) -> exp a -> exp b+++-- | A convenient abbreviation (could've been called `bind')+let_ :: EDSL exp => exp a -> (exp a -> exp b) -> exp b+let_ x y = (lam y) `app` x++-- | A sample EDSL term+t :: EDSL exp => exp Int+t = (lam $ \x -> let_ (x `add` x)+                      $ \y -> y `add` y) `app` int 10++-- * Write a term once, evaluate many times (with different orders)++-- * //+-- * Embedding of the DSL into Haskell+-- An EDSL expression of the type a is interpreted as a Haskell value+-- of the type S l m a, where m is a Monad (the parameter of the interpretation)+-- and l is the label for the evaluation order (one of Name, Value, or Lazy).++newtype S l m a = S { unS :: m a } deriving (Monad, MonadIO)++-- * //+-- * Call-by-name++data Name                               -- The label++-- | We use IO to print out the evaluation trace, so to observe+-- the difference in evaluation orders+--+instance MonadIO m => EDSL (S Name m) where+  int = return+  add x y = do a <- x+               b <- y+               liftIO $ putStrLn "Adding"+               return (a + b)+  sub x y = do a <- x+               b <- y+               liftIO $ putStrLn "Subtracting"+               return (a - b)+  lam f   = return f+  app x y = x >>= ($ y)+++-- Tests+++runName :: S Name m a -> m a+runName x = unS x++-- The addition (x `add` x) is performed twice because y is bound+-- to a computation, and y is evaluated twice+t0SN = runName t >>= print+{-+Adding+Adding+Adding+40+-}++-- |A more elaborate example+t1 :: EDSL exp => exp Int+t1 = (lam $ \x -> let_ (x `add` x) +                  $ \y -> lam $ \z -> +                  z `add` (z `add` (y `add` y))) `app` (int 10 `sub` int 5) +                                                 `app` (int 20 `sub` int 10)++t1SN = runName t1 >>= print+{-+*CB> t1SN+Subtracting+Subtracting+Subtracting+Subtracting+Adding+Subtracting+Subtracting+Adding+Adding+Adding+Adding+40+-}++-- A better example+t2 :: EDSL exp => exp Int+t2 = (lam $ \z -> lam $ \x -> let_ (x `add` x)+                      $ \y -> y `add` y) `app` (int 100 `sub` int 10)+                                         `app` (int 5 `add` int 5)++-- The result of subtraction was not needed, and so it was not performed+-- OTH, (int 5 `add` int 5) was computed four times+t2SN = runName t2 >>= print+{-+*CB> t2SN+Adding+Adding+Adding+Adding+Adding+Adding+Adding+40+-}++-- * //+-- * Call-by-value+-- * The only difference is the interpretation of lam:+-- * before evaluating the body, _always_ evaluate the argument++data Value++-- We reuse most of EDSL (S Name) except for lam+vn :: S Value m x -> S Name m x+vn = S . unS+nv :: S Name m x -> S Value m x+nv = S . unS++instance MonadIO m => EDSL (S Value m) where+    int = nv . int+    add x y = nv $ add (vn x) (vn y)+    sub x y = nv $ sub (vn x) (vn y)+    -- Easier to write it rather than to change the label and then+    -- invoke S Name's app+    app x y = x >>= ($ y)++    -- This is the only difference between CBN and CBV:+    -- lam first evaluates its argument, no matter what+    -- This is the definition of CBV after all+    -- lam f   = return (\x -> (f . return) =<< x)+    -- or, in the pointless notation suggested by Jacques Carette+    lam f   = return (f . return =<<)++runValue :: S Value m a -> m a+runValue x = unS x++-- We now evaluate the previously written tests t, t1, t2+-- under the new interpretation++t0SV = runValue t >>= print+{-+*CB> t0SV+Adding+Adding+40+-}++t1SV = runValue t1 >>= print+{-+*CB> t1SV+Subtracting+Adding+Subtracting+Adding+Adding+Adding+40+-}++-- Although the result of subs-traction was not needed, it was still performed+-- OTH, (int 5 `add` int 5) was computed only once+t2SV = runValue t2 >>= print+{-+*CB> t2SV+Subtracting+Adding+Adding+Adding+40+-}++-- * //+-- * Call-by-need+-- * The only difference is the interpretation of lam:+-- * before evaluating the body, share the argument+-- * The argument is evaluated _at most_ once++share :: MonadIO m => m a -> m (m a)+share m = do+          r <- liftIO $ newIORef (False,m)+          let ac = do+                   (f,m) <- liftIO $ readIORef r+                   if f then m+                      else do+                           v <- m+                           liftIO $ writeIORef r (True,return v)+                           return v+          return ac++data Lazy++ln :: S Lazy m x -> S Name m x+ln = S . unS+nl :: S Name m x -> S Lazy m x+nl = S . unS++-- We reuse most of EDSL (S Name) except for lam+instance MonadIO m => EDSL (S Lazy m) where+    int = nl . int+    add x y = nl $ add (ln x) (ln y)+    sub x y = nl $ sub (ln x) (ln y)+    -- Easier to write it rather than change the label and then+    -- invoke S Name's app+    app x y = x >>= ($ y)++    -- This is the only difference between CBN and CBNeed+    -- lam shares its argument, no matter what+    -- This is the definition of CBNeed after all+    -- lam f           = return (\x -> f =<< share x)+    -- Or, in the pointless notation+    lam f           = return ((f =<<) . share)+++runLazy :: S Lazy m a -> m a+runLazy x = unS x++-- We now evaluate the previously written tests t, t1, t2+-- under the new interpretation++-- Here, Lazy is just as efficient as CBV+t0SL = runLazy t  >>= print+{-+*CB> t0SL+Adding+Adding+40+-}++-- Ditto+t1SL = runLazy t1 >>= print+{-+*CB> t1SL+Subtracting+Subtracting+Adding+Adding+Adding+Adding+40+-}++-- Now, Lazy is better than both CBN and CBV: subtraction was not needed,+-- and it was not performed.+-- All other expressions were needed, and evaluated once.+t2SL = runLazy t2 >>= print+{-+*CB> t2SL+Adding+Adding+Adding+40+-}++main = do+       t0SN >>= print+       t1SN >>= print+       t2SN >>= print++       t0SV >>= print+       t1SV >>= print+       t2SV >>= print++       t0SL >>= print+       t1SL >>= print+       t2SL >>= print

@@ -0,0 +1,439 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}++-- |-+-- <http://okmij.org/ftp/tagless-final/course/course.html#CPS>+--+-- We demonstrate ordinary and administrative-redex--less call-by-value+-- Continuation Passing Style (CPS) transformation that assuredly produces+-- well-typed terms and is patently total.+-- +-- Our goal here is not to evaluate, view or serialize a tagless-final term, but+-- to transform it to another one. The result is a tagless-final term, which we+-- can interpret in multiple ways: evaluate, view, or transform again. We first+-- came across transformations of tagless-final terms when we discussed pushing+-- the negation down in the simple, unityped language of addition and negation.+-- The general case is more complex. It is natural to require the result of+-- transforming a well-typed term be well-typed. In the tagless-final approach+-- that requirement is satisfied automatically: after all, only well-typed terms+-- are expressible. We require instead that a tagless-final transformation be+-- total. In particular, the fact that the transformation handles all possible+-- cases of the source terms must be patently, syntactically clear. The complete+-- coverage must be so clear that the metalanguage compiler should be able to see+-- that, without the aid of extra tools.+-- +-- Since the only thing we can do with tagless-final terms is to interpret them,+-- the CPS transformer is written in the form of an interpreter. It interprets+-- source terms yielding transformed terms, which can be interpreted in many ways.+-- In particular, the terms can be interpreted by the CPS transformer again,+-- yielding 2-CPS terms. CPS transformers are composable, as expected.+-- +-- A particular complication of the CPS transform is that the type of the result+-- is different from the type of the source term: the CPS transform translates not+-- only terms but also types.  Moreover, the CPS type transform and the arrow type+-- constructor do not commute. For that reason, we have to introduce an extended+-- Symantics class, ESymantics, which makes the meaning of function types+-- dependent on a particular interpreter. As it turns out, we do not have to+-- re-write the existing Symantics terms: we can re-interpret any old terms in the+-- extended Symantics.  Conversely, any extended Symantics term can be interpreted+-- using any old, legacy, Symantics interpreter. The CPS transform is an extended+-- Symantics interpreter proper.+-- +-- The ordinary (Fischer or Plotkin) CPS transform introduces many administrative+-- redices, which make the result too hard to read. Danvy and Filinski proposed a+-- one-pass CPS transform, which relies on the metalanguage to get rid of the+-- administrative redices. The one-pass CPS transform can be regarded as an+-- example of the normalization-by-evaluation.+-- +-- +module Language.CPS where++import qualified Language.TTF as Sym++-- * Extending Symantics:+-- * Parameterizing the arrows by the interpreter++-- *  CBAny.hs: type Arr exp a b = exp a -> exp b+-- That is different from the R interpreter we did earlier.+-- Evaluating an object term rep (Arr a b) in CBAny+-- would give us a function, but not of the type a -> b.+-- In the case of R, it would be R a -> R b.+-- It didn't matter for CBAny: We can't observe functional +-- values anyway. In contrast, the term (repr Int) was interpreted +-- in CBAny as Haskell Int, which we can observe. +-- Thus, CBAny is suitable for encoding ``the whole code'' (a typical program),+-- whose result is something we can observe (but not apply).++-- Can we be flexible and permit interpretations of+-- repr (a->b) as truly Haskell functions a->b?+-- We need to make the interpretations of arrows dependent+-- on a particular interpreter.++-- * Emulating ML modules in Haskell+-- Making arrows dependent on the interpreter looks better in OCaml: +-- we write a signature that contains the type ('a,'b) arrow.+-- Different structures implementing the signature will specify+-- the concrete type for ('a,'b) arrow.+-- To emulate this facility -- structures (modules) containing not +-- only values but also types -- we need type functions.+-- We can use multi-parameter type classes with functional dependencies.+-- It seems more elegant here to use type families.++-- * //+-- * How to interpret arrows and other types+type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *++class ESymantics repr where+    int :: Int  -> repr Int+    add :: repr Int  -> repr Int -> repr Int++    lam :: (repr a -> repr b) -> repr (Arr repr a b)+    app :: repr (Arr repr a b) -> repr a -> repr b++-- * Like Symantics in CBAny.hs+-- The class declaration looks exactly like that in CBAny.hs.+-- However, there Arr was a type synonym. Here it is a type+-- function, indexed by repr.++-- * //+-- * All old Symantics terms can be re-interpreted in the+-- * extended Symantics+-- That is, we do not have to re-write the terms written+-- using the methods of the old Symantics (e.g., the terms+-- Sym.th1, Sym.th2, etc.) We merely have to re-interpret them,++-- generalizing the arrow+type family GenArr repr a :: *+type instance GenArr repr Int    = Int+type instance GenArr repr (a->b) = +    Arr repr (GenArr repr a) (GenArr repr b)++newtype ExtSym repr a = ExtSym{unExtSym:: repr (GenArr repr a)}++-- The re-interpretation, essentially the identity+instance ESymantics repr => Sym.Symantics (ExtSym repr) where+    int       = ExtSym . int+    add e1 e2 = ExtSym $ add (unExtSym e1) (unExtSym e2)++    lam e     = ExtSym $ lam (unExtSym . e . ExtSym)+    app e1 e2 = ExtSym $ app (unExtSym e1) (unExtSym e2)+++-- Sample terms++te1 = unExtSym Sym.th1 -- re-interpreting the old Symantics term th1+-- te1 = add (int 1) (int 2)+-- te1 :: (ESymantics repr) => repr Int++te2 = unExtSym Sym.th2+-- te2 = lam (\x -> add x x)+-- te2 :: (ESymantics repr) => repr (Arr repr Int Int)++-- We don't have to re-write th3 as te3; we merely re-interpret it+te3 = unExtSym Sym.th3+-- te3 = lam (\x -> (app x (int 1)) `add` (int 2))+-- te3 :: (ESymantics repr) => repr (Arr repr (Arr repr Int Int) Int)++te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x))))+      in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0)++-- The inferred type is interesting+-- te4+--   :: (Arr repr (Arr repr Int Int) (Arr repr Int Int)+--         ~+--       Arr repr (Arr repr Int Int) (Arr repr Int b),+--       ESymantics repr) =>+--      repr b+-- Because Arr is a type family, and type families are not+-- injective++-- * //+-- * The converse: ESymantics => Symantics+-- All extended symantics terms can be interpreted using+-- any old, legacy, Symantics interpeter+-- * Inject _all_ old interpreters into the new one+newtype Lg repr a = Lg{unLg :: repr a}++type instance Arr (Lg repr) a b = a -> b++instance Sym.Symantics repr => ESymantics (Lg repr) where+    int       = Lg . Sym.int+    add e1 e2 = Lg $ Sym.add (unLg e1) (unLg e2)+    lam e     = Lg $ Sym.lam (unLg . e . Lg)+    app e1 e2 = Lg $ Sym.app (unLg e1) (unLg e2)++legacy :: Sym.Symantics repr => (repr a -> b) -> Lg repr a -> b+legacy int e = int (unLg e)++-- * //+-- * We can use all existing interpreters _as they are_++te3_eval = legacy Sym.eval te3+-- te3_eval :: Arr (Lg Sym.R) (Arr (Lg Sym.R) Int Int) Int++te3_eval' = te3_eval id+-- 3++te3_view = legacy Sym.view te3+-- "(\\x0 -> ((x0 1)+2))"++te4_eval = legacy Sym.eval te4+-- 42++te4_view = legacy Sym.view te4+-- "(((\\x0 -> (\\x1 -> (x0 (x0 (x0 x1))))) (\\x0 -> (x0+14))) 0)"++-- We haven't gained anything though. Now we will++-- * //+-- * CBV CPS transform+-- *  CPS[ value ] = \k -> k $ CPSV[ value ]+-- *  CPS[ e1 e2 ] =+-- *   \k ->+-- *     CPS[ e1 ] (\v1 ->+-- *       CPS[ e2 ] (\v2 ->+-- *         v1 v2 k))+-- * (similar for addition)+-- *+-- *  CPSV[ basec ] = basec+-- *  CPSV[ x ]     = x+-- *  CPSV[ \x.e ]  = \x -> CPS[ e ]+-- We chose left-to-right evaluation order+-- * Danvy: CPS is *the* canonical transform+-- * CPS on types is NOT the identity+-- Why? Try to work out the types first++-- * //+newtype CPS repr w a = +   CPS{cpsr :: repr (Arr repr (Arr repr a w) w)}+-- Here, w is the answer-type+-- We observe the similarity with the double negation+-- CPS is the transform: we use the arrows of the base interpreter++type instance Arr (CPS repr w) a b = +   Arr repr a (Arr repr (Arr repr b w) w)++-- Auxiliary functions+-- Using (Arr repr a b) instead of (a->b) hinders the type+-- inference since type functions are not in general injective.+-- We need the following functions to constrain the types+-- so that the inference will work.+-- I wish there were a way to declare a type family injective!+cpsk :: ESymantics repr => (repr (Arr repr a w) -> repr w) -> CPS repr w a+cpsk = CPS . lam++appk :: ESymantics repr =>+	CPS repr w a -> (repr a -> repr w) -> repr w+appk (CPS e) f = app e $ lam f++-- * CPS of a value+cpsv :: ESymantics repr => repr a -> CPS repr w a+cpsv v = cpsk $ \k -> app k v++instance ESymantics repr => ESymantics (CPS repr w) where+    int x = cpsv $ int x+    add e1 e2 = cpsk $ \k ->+ 		  appk e1 $ \v1 ->+ 		  appk e2 $ \v2 ->+ 		     app k (add v1 v2)+    lam e = cpsv $ lam (\x -> cpsr $ e (cpsv x))+    app ef ea = cpsk $ \k ->+ 		  appk ef $ \vf ->+ 		  appk ea $ \va ->+ 		     app (app vf va) k+++-- * //+-- * Applying the transform, evaluate afterwards++tec1 = cpsr te1+-- tec1 :: (ESymantics repr) => repr (Arr repr (Arr repr Int w) w)++-- We need to pass the identity continuation+tec1_eval = legacy Sym.eval tec1 id+-- 3++-- * The case of administrative redices+tec1_view = legacy Sym.view tec1+-- "(\\x0 -> ((\\x1 -> (x1 1)) +--    (\\x1 -> ((\\x2 -> (x2 2)) (\\x2 -> (x0 (x1+x2)))))))"++-- The result is a bit of a mess: lots of administrative redices++tec2 = cpsr te2+tec2_eval = legacy Sym.eval tec2++-- The interpretation of a function is not usable, because of w...+-- Here we really need the answer-type polymorphism+-- OTH, like in CBAny.hs, the transform of a generally 'effectful'+-- function can be used in a `pure' code.+-- We can get a pure function out of tec2_eval; but+-- we have to do differently (from passing an identity continuation)+tec2_eval' = \a -> tec2_eval (\k -> k a id)+-- tec2_eval' :: Int -> Int++tec2_eval'' = tec2_eval' 21+-- 42++tec2_view = legacy Sym.view tec2+-- even bigger mess++tec4 = cpsr te4+tec4_eval = legacy Sym.eval tec4 id+-- 42++tec4_view = legacy Sym.view tec4+-- view is a mess... makes a good wall-paper pattern though...++-- * //+-- * Composing interpreters: doing CPS twice+-- We have already seen how to chain tagless final interpreters.+-- We push this further: we do CPS twice++tecc1 = cpsr tec1+-- The type makes it clear we did CPS twice++-- To evaluate the doubly-CPSed term, we have to do+-- more than just apply the identity continuation+-- flip($) is \v\k -> k v, which is sort of cpsv+tecc1_eval = legacy Sym.eval tecc1+tecc1_eval' = tecc1_eval (\k -> k (flip ($)) id)+-- 3++tecc1_view = legacy Sym.view tecc1+-- very big mess+++-- * //+-- * One-pass CPS transform+-- Taking advantage of the metalanguage to get rid of the+-- administrative redices++newtype CPS1 repr w a = +   CPS1{cps1r :: (repr a -> repr w) -> repr w}++reflect :: ESymantics repr =>+	   ((repr a -> repr w) -> repr w) ->+	   repr (Arr repr (Arr repr a w) w)+reflect e = lam (\k -> e (\v -> app k v))+-- * reflect e = lam (e . app)++-- The same as in CPS+-- After all, CPS1 is an optimization of CPS+type instance Arr (CPS1 repr w) a b = +   Arr repr a (Arr repr (Arr repr b w) w)++-- * CPS1 of a value+cps1v :: ESymantics repr => repr a -> CPS1 repr w a+cps1v v = CPS1 $ \k -> k v++instance ESymantics repr => ESymantics (CPS1 repr w) where+    int x = cps1v $ int x+    add e1 e2 = CPS1 $ \k ->+ 		  cps1r e1 $ \v1 ->+ 		  cps1r e2 $ \v2 ->+ 		     k (add v1 v2)++    lam e = cps1v $ lam $ reflect . cps1r . e . cps1v++    app ef ea = CPS1 $ \k ->+ 		  cps1r ef $ \vf ->+ 		  cps1r ea $ \va ->+ 		     app (app vf va) (lam k)++cps1 = reflect . cps1r++-- * //+-- * Applying the transform, evaluate afterwards++tek1 = cps1 te1+-- tek1 :: (ESymantics repr) => repr (Arr repr (Arr repr Int w) w)++-- We need to pass the identity continuation+tek1_eval = legacy Sym.eval tek1 id+-- 3++-- * The result is indeed much nicer+-- Administrative redices are gone, serious operations+-- (like addition) remain+tek1_view = legacy Sym.view tek1+-- "(\\x0 -> (x0 (1+2)))"++tek2 = cps1 te2+tek2_eval = legacy Sym.eval tek2+tek2_eval'' = tek2_eval (\k -> k 21 id)+-- 42++-- Again, only serious redices remain+tek2_view = legacy Sym.view tek2+-- "(\\x0 -> (x0 (\\x1 -> (\\x2 -> (x2 (x1+x1))))))"+++tek4 = cps1 te4+tek4_eval = legacy Sym.eval tek4 id+-- 42++tek4_view = legacy Sym.view tek4+-- The result is large, but comprehensible...+-- "(\\x0 -> +--   (((\\x1 -> (\\x2 -> (x2 (\\x3 -> (\\x4 -> ((x1 x3) (\\x5 -> ((x1 x5) +--                         (\\x6 -> ((x1 x6) (\\x7 -> (x4 x7)))))))))))) +--     (\\x1 -> (\\x2 -> (x2 (x1+14))))) +--   (\\x1 -> ((x1 0) (\\x2 -> (x0 x2))))))"++-- * //+-- * Composing interpreters: doing CPS twice+-- We have already seen how to chain tagless final interpreters.+-- We push this further: we do CPS twice++tekk1 = cps1 tek1+-- The type makes it clear we did CPS twice++tekk1_eval = legacy Sym.eval tekk1++-- tekk1_eval ::+--   (((Int -> (w1 ->w) -> w) -> (w1->w) -> w) -> w) -> w+tekk1_eval' = tekk1_eval (\k -> k (flip ($)) id)+-- 3++tekk1_view = legacy Sym.view tekk1+-- "(\\x0 -> (x0 (\\x1 -> (\\x2 -> ((x1 (1+2)) (\\x3 -> (x2 x3)))))))"+-- Can be eta-reduced+-- "(\\x0 -> (x0 (\\x1 -> (\\x2 -> ((x1 (1+2)) x2)))))"+-- "(\\x0 -> (x0 (\\x1 -> (x1 (1+2)) )))"++-- * Lessons+-- * The output of CPS is assuredly typed+-- * The conversion is patently total+-- * Composable transformers in the tagless final style++++main = do+       print te3_eval'+       print te3_view+       print te4_eval+       print te4_view++       print tec1_eval+       print tec1_view+       print tec2_eval''+       print tec2_view+       print tec4_eval+       print tec4_view++       print tecc1_view+       print tecc1_eval'++       print tek1_eval+       print tek1_view+       print tek2_eval''+       print tek2_view+       print tek4_eval+       print tek4_view++       print tekk1_eval'+       print tekk1_view

@@ -0,0 +1,165 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++-- |+-- Type-directed partial evaluation, Olivier Danvy, POPL96+-- * <http://www.brics.dk/~danvy/tdpe-ln.pdf>+--+module Language.TDPE where++import Language.TTF hiding (main)		-- HOAS Symantics++--  ``black-box'' functions, _compiled_+import Language.ToTDPE+++-- * //+-- * Demo first+-- * bbf1 and bbf2 are imported from the _compiled_ module ToTDPE+-- We can see their types+-- TDPE> :t bbf1+-- bbf1 :: t -> t1 -> t+-- TDPE> :t bbf2+-- bbf2 :: (c -> c) -> c -> c+-- Can you tell what they are? Especially bbf2?+-- * It would be great to have a function a -> repr a++-- * //+-- * Deriving reify_t :: t -> repr t+-- We call this `magic' function reify. It is actually a family of+-- functions, indexed by types.+-- * Why the name `reify'?+-- We convert from a Haskell value of the type t to an object+-- _representing_ that value of type t.++-- * Start with reify_aa :: (a -> a) -> repr (a -> a)+-- Here, we convert from a metalanguage function (a->a) (`the thing')+-- to an object (EDSL) function repr (a->a). The latter is also a Haskell+-- value, which represents `the thing.'+-- In other words, we take an `abstract', or opaque function (a->a)+-- (which we can't print, for example) and produce an object (repr (a->a))+-- that we can view. In general, `reify' means representing an abstract+-- concept in terms of a concrete object a value.++-- We take as an input a _polymorphic_ Haskell function of the principal+-- type a->a. The input function also has the instantiated type+-- repr a -> repr a, right?+-- So, the real type of reify_aa is +--    reify_aa :: (repr a -> repr a) -> repr (a->a)+-- Have we seen a function of that type already?+-- We thus obtain reify_aa = lam++-- * //+-- * Deriving reify_aabb :: (a->a)->(b->b) -> repr ((a->a)->(b->b))+-- Let us overlook a bit silly type of the term+-- The input function can be instantiated: we substitute (repr a) for a+-- and (repr b) for b. So, we need to convert+--    (repr a -> repr a) -> (repr b ->  repr b)+-- to repr ((a->a)->(b->b)).+-- The desired term has the form repr (t1->t2). There is only one way+-- to construct a term of that type, use lam. We write+-- reify_aabb f = lam (\x -> ???)+-- where x must have the type (repr (a->a)) and ??? must have the type+-- (repr (b->b)).+-- Recall, that f, the argument to reify_aabb has the type+--   (repr a -> repr a) -> (repr b ->  repr b)+-- Here is our plan: take x and somehow convert it to a term+-- of the type (repr a -> repr a). Pass the result to the function f,+-- obtaining a term of the type (repr b -> repr b).+-- We know how to convert that to (repr (b->b)): we apply reify_bb.+-- To carry out our plan, we need the function reflect:++-- * //+-- * We need reflect_aa :: repr (a->a) -> (repr a -> repr a)+-- It too is a family of functions, indexed by type. It is in a sense+-- the `inverse' of reify. We will talk about that sense later.+-- It takes an object _representing_ the true Haskell function, and+-- produces the _represented_ thing, the true Haskell function.+-- Have we already seen the function of that type? the `inverse' of lam?++-- Our final result:+-- reflect_aa = app+-- reify_aabb f = lam (\x -> reify_bb (f (reflect_aa x)))+-- What is reflect_aabb? Anyone?++-- * //+-- * We build reify_t and reflect_t together and inductively.++data RR repr meta obj = RR{reify   :: meta -> repr obj,+			   reflect :: repr obj -> meta}++-- * The base of induction (reify/reflect for base types)+base :: RR repr (repr a) a+base = RR{reify = id, reflect = id}++-- * The inductive case+infixr 8 -->				-- arrow constructor for RR++(-->) :: Symantics repr =>+         RR repr m1 o1 -> RR repr m2 o2 -> RR repr (m1 -> m2) (o1 -> o2)+r1 --> r2 = RR{reify   = \m -> lam (reify r2 . m . reflect r1),+	       reflect = \o -> reflect r2 . app o . reify r1}++-- reflect looks like eta-expansion: \x -> app o x,+-- with intervening reify/reflect and the change of levels++-- * //+-- * Examples++-- We come back to the original question: what are bbf1 and bbf2?++tb1 = reify (base --> base --> base) bbf1+-- tb1 :: (Symantics repr) => repr (o1 -> o11 -> o1)++-- Now that we've got a Symantics term, we can view it+tb1_view = view tb1+-- "(\\x0 -> (\\x1 -> x0))"+++tb2 = reify ((base --> base) --> (base --> base)) bbf2+-- tb2 :: (Symantics repr) => repr ((o1 -> o1) -> o1 -> o1)++-- We can evaluate the reified term in many ways++tb2_eval = eval tb2 (succ) 0+-- 3++-- In the beta-eta normal form!++tb2_view = view tb2+-- "(\\x0 -> (\\x1 -> (x0 (x0 (x0 x1)))))"++-- * //+-- * Duality of reify/reflect+-- *  reflect . reify = eq_meta+-- *  reify . reflect = eq_obj+-- Where eq_meta is the equality of meta-terms and eq_obj is the equality+-- of object terms. What sort of equality? Often this question is+-- elided or hand-waved, which is a pity.++-- Let's take an example of the type a -> a, where reify_aa is lam and+-- reflect_aa is app.+-- app . lam +-- == \f -> app (lam f)+-- == \f -> \e -> app (lam (\x -> f x)) e+-- {beta at obj level}+-- == \f -> \e -> f e == id_meta++-- lam . app+-- == \f -> lam (app f) +-- == \f -> lam (\e -> app f e)+-- {eta at obj level}+-- == \f -> f == id_obj (since f has the type repr (a->a))+--+-- So, reflect/reify duality expresses beta-eta equivalence:+-- we should equate object terms modulo beta/eta.+-- This is the reason+-- * reify gives the object term representing the normal form of meta+-- * cf Normalization-by-evaluation+-- See the real form of bbf2. What we have printed is a+-- beta-eta-normal form.+++main = do+       print tb1_view+       print tb2_eval+       print tb2_view

@@ -0,0 +1,242 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++-- |+--+-- Typed tagless-final interpreters for PCF+-- Higher-order abstract syntax+-- based on the code accompanying the paper by+--   Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan+--+-- <http://okmij.org/ftp/tagless-final/course/course.html#TDPE>+--+--+module Language.TTF where++-- | The language is simply-typed lambda-calculus with fixpoint and+-- constants. It is essentially PCF.+-- The language is just expressive enough for the power function.+-- We define the language by parts, to emphasize modularity.+-- The core plus the fixpoint is the language described in the paper+--+--   /Hongwei Xi, Chiyan Chen, Gang Chen Guarded Recursive Datatype Constructors, POPL2003/+--+-- which is used to justify GADTs.+--+-- * Core language+class Symantics repr where+    int :: Int  -> repr Int              -- int literal+    add :: repr Int  -> repr Int -> repr Int++    lam :: (repr a -> repr b) -> repr (a->b)+    app :: repr (a->b) -> repr a -> repr b++-- |+-- * Like ExpSYM, but repr is of kind * -> *+-- repr is parameterized by the type of the expression+-- * The types read like the minimal logic in +-- * Gentzen-style natural deduction+-- * Type system of simply-typed lambda-calculus in Haskell98!++-- * Sample terms and their inferred types+-- They do look better now.+th1 = add (int 1) (int 2)+-- th1 :: (Symantics repr) => repr Int++th2 = lam (\x -> add x x)+-- th2 :: (Symantics repr) => repr (Int -> Int)++th3 = lam (\x -> add (app x (int 1)) (int 2))+-- th3 :: (Symantics repr) => repr ((Int -> Int) -> Int)+++-- |+-- * th2o = lam (\x -> add x y)+-- th2o is not accepted: open terms are simply not+-- expressible in HOAS+++-- * //+-- * Typed and tagless interpreter+--+newtype R a = R{unR :: a}++instance Symantics R where+    int x     = R x+    add e1 e2 = R $ unR e1 + unR e2++    lam f     = R $ unR . f . R+    app e1 e2 = R $ (unR e1) (unR e2)++-- |+-- * R is not a tag! It is a newtype+-- The expression with unR _looks_ like tag introduction and+-- elimination. But the function unR is *total*. There is no +-- run-time error is possible at all -- and this fact is fully +-- apparent to the compiler.+-- Furthermore, at run-time, (R x) is indistinguishable from x+-- * R is a meta-circular interpreter+-- This is easier to see now. So, object-level addition is+-- _truly_ the metalanguage addition. Needless to say, that is+-- efficient.+-- * R never gets stuck: no pattern-matching of any kind+-- * R is total+--+eval e = unR e++th1_eval = eval th1+-- 3++th2_eval = eval th2+-- th2_eval :: Int -> Int+-- We can't print a function, but we can apply it++th2_eval' = eval th2 21+-- 42++th3_eval = eval th3+-- th3_eval :: (Int -> Int) -> Int+++-- |+-- * //+-- Another interpreter+--+type VarCounter = Int+newtype S a = S{unS:: VarCounter -> String}++instance Symantics S where+    int x     = S $ const $ show x+    add e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ "+" ++ unS e2 h ++ ")"++    lam e = S $ \h -> +       let x = "x" ++ show h+       in "(\\" ++ x ++ " -> " ++ +            unS (e (S $ const x)) (succ h) ++ ")"+    app e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ " " ++ unS e2 h ++ ")"++-- The major difference from TTFdb is the interpretation+-- of lam++view e = unS e 0++th1_view = view th1+-- "(1+2)"++th2_view = view th2+-- "(\\x0 -> (x0+x0))"++th3_view = view th3+-- "(\\x0 -> ((x0 1)+2))"++-- |+-- * The crucial role of repr being a type constructor+-- rather than just a type. It lets some information about+-- object-term representation through (the type) while+-- keeping the representation itself hidden.+--+-- * //+-- * Extensions of the language+--+-- * Multiplication+class MulSYM repr where+    mul :: repr Int -> repr Int -> repr Int++-- * Booleans+class BoolSYM repr where+    bool :: Bool -> repr Bool             -- bool literal+    leq :: repr Int -> repr Int -> repr Bool+    if_ :: repr Bool -> repr a -> repr a -> repr a++-- * Fixpoint+class FixSYM repr where+    fix :: (repr a -> repr a)  -> repr a++-- | Logically, the signature of fix reads like nonsense+--+-- * http://xkcd.com/704/++-- * Extensions are independent of each other++-- The main power+-- Looks like Scheme, doesn't it?+-- We can define suitable infix operators however.+--+-- The inferred type of pow shows all the extensions in action+tpow  = lam (\x -> fix (\self -> lam (\n ->+                        if_ (leq n (int 0)) (int 1)+                            (mul x (app self (add n (int (-1))))))))+-- tpow :: (Symantics repr, BoolSYM repr, MulSYM repr, FixSYM repr) =>+--         repr (Int -> Int -> Int)++tpow7 = lam (\x -> app (app tpow x) (int 7))+tpow72 = app tpow7 (int 2)+-- tpow72 :: (Symantics repr, BoolSYM repr, MulSYM repr, FixSYM repr) => +-- repr Int++-- * //+-- * Extending the R interpreter++instance MulSYM R where+    mul e1 e2 = R $ unR e1 * unR e2++instance BoolSYM R where+    bool b    = R b+    leq e1 e2 = R $ unR e1 <= unR e2+    if_ be et ee = R $ if unR be then unR et else unR ee ++instance FixSYM R where+    fix f = R $ fx (unR . f . R) where fx f = f (fx f)++-- Again, the extensions are independent++tpow_eval = eval tpow+-- tpow_eval :: Int -> Int -> Int++tpow72_eval = eval tpow72+-- 128++-- * //+-- * Extending the S interpreter++-- Only the case of fix is interesting (and perhaps, of if_)++instance MulSYM S where+    mul e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ "*" ++ unS e2 h ++ ")"++instance BoolSYM S where+    bool x     = S $ const $ show x+    leq e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ "<=" ++ unS e2 h ++ ")"+    if_ be et ee = S $ \h ->+       unwords["(if", unS be h, "then", unS et h, "else", unS ee h,")"]++instance FixSYM S where+    fix e = S $ \h -> +       let self = "self" ++ show h+       in "(fix " ++ self ++ "." ++ +            unS (e (S $ const self)) (succ h) ++ ")"++tpow_view = view tpow+-- "(\\x0 -> (fix self1.(\\x2 -> (if (x2<=0) then 1 else (x0*(self1 (x2+-1))) ))))"++-- Other interpreters are possible: C (staging), L and P (partial evaluation)+-- Refer to the slide with the contributions of the paper++{-+-- Another interpreter: it interprets each term to give its size+-- (the number of constructors)+-}++main = do+       print th1_eval+       print th2_eval'++       print th1_view+       print th2_view+       print th3_view++       print tpow72_eval+       print tpow_view

@@ -0,0 +1,212 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++-- |+-- * Essentially, Haskell98!+-- * Typed tagless-final interpreters for simply-typed lambda-calculus+-- * de Bruijn indices+-- based on the code accompanying the paper by+--   Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan++module Language.TTFdB where++-- * Abstracting over the final interpreter in IntroHOIF.hs++-- This class defines syntax (and its instances, semantics) +-- of our language++-- I could've moved s and z into a separate ``class Var var_repr''+-- Symantics would then have a single form+-- v :: var_repr h a -> repr h a++class Symantics repr where+    int :: Int -> repr h Int                -- int literal+    add :: repr h Int -> repr h Int -> repr h Int++    z   :: repr (a,h) a			-- variables: z and s ... (s z)+    s   :: repr h a -> repr (any,h) a+    lam :: repr (a,h) b  -> repr h (a->b)+    app :: repr h (a->b) -> repr h a -> repr h b++-- * Like GADT-based, but in lower-case+-- * Like ExpSYM, but repr is of kind * -> * -> *+-- repr is parameterized by the environment (h) and the type+-- of the expression+-- * The types read like the rules of minimal logic+-- For example, z is the axiom stating that assuming A we can get A+-- lam is the inference rule: if assuming A we derive B,+-- then we can derive the implication A->B+-- * Type system of simply-typed lambda-calculus in Haskell98!+-- The signature of the class can be read off as the typing+-- rules for simply-typed lambda-calculus. But the code+-- is Haskell98! So, contrary to the common belief, we do not+-- need dependent types to express the type system of simply+-- typed lambda-calculus. Compare with Term.agda+-- * ``a way to write a typed fold function over a typed term.''+-- as one reviewer of our paper put it+++-- * Sample terms and their inferred types+td1 = add (int 1) (int 2)+-- td1 :: (Symantics repr) => repr h Int++td2 = lam (add z z)+-- td2 :: (Symantics repr) => repr h (Int -> Int)++td2o = lam (add z (s z))+-- td2o :: (Symantics repr) => repr (Int, h) (Int -> Int)+-- the inferred type says td2o is open! Needs the env with Int++td3 = lam (add (app z (int 1)) (int 2))+-- td3 :: (Symantics repr) => repr h ((Int -> Int) -> Int)++-- Ill-typed terms are not expressible+-- * td2a = app (int 1) (int 2)+--     Couldn't match expected type `a -> b' against inferred type `Int'+--       Expected type: repr h (a -> b)+--       Inferred type: repr h Int+--     In the first argument of `app', namely `(int 1)'++-- * Embedding all and only typed terms of the object language+-- * in the typed metalanguage+-- Typed object terms are represented as typed Haskell terms+++-- * //+-- * Typed and tagless evaluator+-- *  object term ==> metalanguage value++newtype R h a = R{unR :: h -> a}++instance Symantics R where+    int x     = R $ const x+    add e1 e2 = R $ \h -> (unR e1 h) + (unR e2 h)++    z     = R $ \(x,_) -> x+    s v   = R $ \(_,h) -> unR v h+    lam e = R $ \h -> \x -> unR e (x,h)+    app e1 e2 = R $ \h -> (unR e1 h) (unR e2 h)++eval e = unR e ()			-- Eval in the empty environment++-- * R is not a tag!+-- The expression with unR _looks_ like tag introduction and+-- elimination. But the function unR is *total*. There is no +-- run-time error is possible at all -- and this fact is fully +-- apparent to the compiler.+-- * R is a meta-circular interpreter+-- It runs each object-language operation by executing the corresponding+-- metalanguage operation.+-- * R never gets stuck: no variant types, no pattern-match failure+-- * Well-typed programs indeed don't go wrong!+-- * R is total+-- * The instance R is a constructive proof of type soundness+-- First of all, we see the type preservation (for object types)+-- for interpretations: interpretations preserve types.+-- Then we see progress: the interpreter does not get stuck.+-- So we reduced the problem of type soundness of the object language+-- (simply-typed lambda-calculus) to the type soundness of the+-- metalanguage.+-- * R _looks_ like a reader monad (but h varies)+-- R looks like a reader monad, but the type of the environment+-- varies.++-- Evaluate our test expressions+td1_eval = eval td1+-- 3++td2_eval = eval td2+-- td2_eval :: Int -> Int -- can't print+-- since td2_eval is a function taking Int, we can give it an Int+td2_eval' = eval td2 21+-- 42++-- td2o_eval = eval td2o+-- Can't evaluate the open term++td3_eval = eval td3+-- td3_eval :: (Int -> Int) -> Int++-- * //+-- Another interpreter++newtype S h a = S{unS :: [String] -> String}++instance Symantics S where+    int x     = S $ const $ show x+    add e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ "+" ++ unS e2 h ++ ")"++    z     = S $ \(x:_) -> x+    s v   = S $ \(_:h) -> unS v h+    lam e = S $ \h -> +       let x = "x" ++ show (length h)+       in "(\\" ++ x ++ " -> " ++ unS e (x:h) ++ ")"+    app e1 e2 = S $ \h -> +      "(" ++ unS e1 h ++ " " ++ unS e2 h ++ ")"++-- Now this is almost the Reader monad. Why not fully?+-- The interpretation of lam is quite different from that in R+-- The environment is a regular, homogeneous list now+-- (see the rules 's' and 'z')++view :: S () a -> String -- Only closed terms can be viewed+view e = unS e []++td1_view = view td1+-- "(1+2)"++td2_view = view td2+-- "(\\x0 -> (x0+x0))"++td3_view = view td3+-- "(\\x0 -> ((x0 1)+2))"++-- We now finally see our terms in a useful form+-- Clearly, de Bruijn notation is not the most perspicuous+-- We now turn to HOAS++-- Exercise: implement the following extensions+{-++-- * //+-- Extensions of the language++-- * Multiplication+class MulSYM repr where+    mul :: repr r Int -> repr r Int -> repr r Int++-- * Booleans+class BoolSYM repr where+    bool :: Bool -> repr r Bool             -- bool literal+    if_ :: repr r Bool -> repr r a -> repr r a -> repr r a+    leq :: repr r Int -> repr r Int -> repr r Bool++-- * Fixpoint+class FixSYM repr where+    fix :: repr (a,h) a  -> repr h a++-- Logically, the signature of fix reads like nonsense+-- The extensions are independent++testpowfix () = lam {- x -} (+                  fix {- self -} (lam {- n -} (+                  let n = z; self = s z; x = s (s z)    +                  in  if_ (leq n (int 0)) (int 1)+                          (mul x (app self (add n (int (-1))))))))+testpowfix7 () = lam (app (app (testpowfix ()) z) (int 7))++rtestpw   = mkrtest testpowfix+rtestpw7  = mkrtest testpowfix7+rtestpw72 = mkrtest (\() -> app (testpowfix7 ()) (int 2)) -- 128++-- Another interpreter: it interprets each term to give its size+-- (the number of constructors)+-}++main' = do+       print td1_eval+       print td2_eval'+       print td1_view+       print td2_view+       print td3_view+

@@ -0,0 +1,10 @@+-- Sample functions to use for type-directed partial evaluation (TDPE)+-- Compiling this module makes for a nicer example++module Language.ToTDPE where++-- ``black-box'' functions++bbf1 x y = x++bbf2 f = f . f . (id f)

@@ -0,0 +1,278 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Rank2Types, ExistentialQuantification #-}++-- |+-- * Type representation, equality and the safe typecast:+-- * the above-the-board version of Data.Typeable+--+module Language.Typ where++import Control.Monad+import Control.Monad.Error+++-- |+-- * The language of type representations: first-order and typed+-- It is quite like the language of int/neg/add we have seen before,+-- but it is now typed.+-- It is first order: the language of simple types is first order++class TSYM trepr where+    tint :: trepr Int+    tarr :: trepr a -> trepr b -> trepr (a->b)++-- |+-- * The view interpreter+-- The first interpreter is to view the types+--+newtype ShowT a = ShowT String++instance TSYM ShowT where+    tint = ShowT $ "Int"+    tarr (ShowT a) (ShowT b) = ShowT $ "(" ++ a ++ " -> " ++ b ++ ")"++view_t :: ShowT a -> String+view_t (ShowT s) = s++-- * //+-- * Quantifying over the TSYM interpreter+-- This closes the type universe++newtype TQ t = TQ{unTQ :: forall trepr. TSYM trepr => trepr t}++-- | TQ is itself an interpreter, the trivial one+instance TSYM TQ where+    tint = TQ tint+    tarr (TQ a) (TQ b) = TQ (tarr a b)++-- | Sample type expressions+-- +tt1 = (tint `tarr` tint) `tarr` tint+-- tt1 :: (TSYM trepr) => trepr ((Int -> Int) -> Int)++tt2 = tint `tarr` (tint `tarr` tint)+-- tt2 :: (TSYM trepr) => trepr (Int -> Int -> Int)++tt1_view = view_t (unTQ tt1)+-- "((Int -> Int) -> Int)"++tt2_view = view_t (unTQ tt2)+-- "(Int -> (Int -> Int))"++-- * //+-- * Show Typ-able expressions+-- * No Show type class constraint!++-- The signature is quite like gshow in a generic programming+-- library such as EMGM or LIGD+show_as :: TQ a -> a -> String+show_as tr a = +    case unTQ tr of ShowAs _ f -> f a++-- | The implementation of the interpreter ShowAs shows off+-- the technique of accumulating new TQ as we traverse the old+-- one. We shall see more examples later.+-- One is again reminded of attribute grammars.+--+data ShowAs a = ShowAs (TQ a) (a -> String)++instance TSYM ShowAs where+    tint = ShowAs tint show  -- as Int+    tarr (ShowAs t1 _) (ShowAs t2 _) =+        let t = tarr t1 t2 in+	ShowAs t (\_ ->  "<function of the type " ++ +	                 view_t (unTQ t) ++ ">")+tt0_show = show_as tint 5+-- "5"++tt1_show = show_as tt1 undefined+-- "<function of the type ((Int -> Int) -> Int)>"++-- We can't show functional values, but at least we should be+-- able to show their types++-- * //+-- * Type representation+-- * Compare with Dyta.Typeable.TypeRep+-- It is not a data structure!+data Typ = forall t. Typ (TQ t)+++-- * //+-- * Alternative to quantification: copying+-- Before instantiating one interpreter, we fork it.+-- One copy can be instantiated, but the other remains polymorphic+-- Compare with Prolog's copy_term+-- This approach keeps the type universe extensible+-- Again the same pattern: traverse one TQ and build another+-- (another two actually)++data TCOPY trep1 trep2 a = TCOPY (trep1 a) (trep2 a)++instance (TSYM trep1, TSYM trep2) +    => TSYM (TCOPY trep1 trep2)+  where+    tint = TCOPY tint tint+    tarr (TCOPY a1 a2) (TCOPY b1 b2) = +	TCOPY (tarr a1 b1) (tarr a2 b2)++-- * //+-- * Equality and safe type cast++-- * c is NOT necessarily a functor or injective!+-- For example, repr is not always a functor+-- I wonder if we can generalize to an arbitrary type function+-- represented by its label lab:+-- newtype EQU a b = EQU (forall lab. (Apply lab a -> Apply lab b)+-- That would let us _easily_ show, for example, that+-- EQU (a,b) (c,d) implies EQU a c, for all types a, b, c, d.++newtype EQU a b = EQU{equ_cast:: forall c. c a -> c b}++-- * Leibniz equality is reflexive, symmetric and transitive+-- Here is the constructive proof++refl :: EQU a a+refl = EQU id++-- * An Unusual `functor'+tran :: EQU a u -> EQU u b -> EQU a b+tran au ub = equ_cast ub au+-- Why it works? We consider (EQU a u) as (EQU a) u,+-- and so instantiate c to be EQU a++newtype FS b a = FS{unFS:: EQU a b}++symm :: EQU a b -> EQU b a+symm equ = unFS . equ_cast equ . FS $ refl++-- Useful type-level lambdas, so to speak+newtype F1 t b a = F1{unF1:: EQU t (a->b)}++newtype F2 t a b = F2{unF2:: EQU t (a->b)}++eq_arr :: EQU a1 a2 -> EQU b1 b2 -> EQU (a1->b1) (a2->b2)+eq_arr a1a2 b1b2 = +    unF2 . equ_cast b1b2 . F2 . unF1 . equ_cast a1a2 . F1 $ refl++-- How does this work? what is the type of refl above?++-- * //+-- * Decide if (trepr a) represents a type that is equal to some type b+-- Informally, we compare a value that _represents_ a type b+-- against the _type_ b++-- We do that by interpreting trepr a in a particular way++-- * A constructive `deconstructor'+data AsInt a = AsInt (Maybe (EQU a Int))++instance TSYM AsInt where+    tint     = AsInt $ Just refl+    tarr _ _ = AsInt $ Nothing++-- This function proves useful later+as_int :: AsInt a -> c a -> Maybe (c Int)+as_int (AsInt (Just equ)) r = Just $ equ_cast equ r+as_int _ _ = Nothing++-- * Another constructive `deconstructor'++data AsArrow a = +    forall b1 b2. AsArrow (TQ a) (Maybe (TQ b1, TQ b2, EQU a (b1->b2)))++instance TSYM AsArrow where+    tint       = AsArrow tint Nothing+    tarr (AsArrow t1 _) (AsArrow t2 _) = +	         AsArrow (tarr t1 t2) $ Just (t1,t2,refl)++as_arrow :: AsArrow a -> AsArrow a+as_arrow = id++-- More cases could be added later on...++newtype SafeCast a = SafeCast (forall b. TQ b -> Maybe (EQU a b))++instance TSYM SafeCast where+    tint = SafeCast $ \tb -> +	     case unTQ tb of AsInt eq -> fmap symm eq+    tarr (SafeCast t1) (SafeCast t2) = +	 SafeCast $ \tb -> do+	     AsArrow _ (Just (b1,b2,equ_bb1b2)) <- +		 return $ as_arrow (unTQ tb)+	     equ_t1b1 <- t1 b1+	     equ_t2b2 <- t2 b2+	     return $ tran (eq_arr equ_t1b1 equ_t2b2) (symm equ_bb1b2)+++-- * Cf. Data.Typeable.gcast+-- Data.Typeable.gcast :: (Data.Typeable.Typeable b, Data.Typeable.Typeable a) =>+--                         c a -> Maybe (c b)+-- We use our own `Typeable', implemented without+-- invoking GHC internals++safe_gcast :: TQ a -> c a -> TQ b -> Maybe (c b)+safe_gcast (TQ ta) ca tb = cast ta+ where cast (SafeCast f) = +	 maybe Nothing (\equ -> Just (equ_cast equ ca)) $ f tb++-- There is a tantalizing opportunity of making SafeCast extensible++-- * //+-- * Our own version of Data.Dynamic+-- We replace Data.Typeable with TQ a++data Dynamic = forall t. Dynamic (TQ t) t++tdn1 = Dynamic tint 5++tdn2 = Dynamic tt1 ($ 1)++tdn3 = Dynamic (tint `tarr` (tint `tarr` tint)) (*)++tdn_show (Dynamic tr a) = show_as tr a++newtype Id a = Id a+tdn_eval1 (Dynamic tr d) x = do+  Id f <- safe_gcast tr (Id d) tt1+  return . show $ f x++tdn_eval2 (Dynamic tr d) x y = do+  Id f <- safe_gcast tr (Id d) tt2 +  return . show $ f x y++tdn1_show = tdn_show tdn1+-- "5"++tdn2_show = tdn_show tdn2+-- "<function of the type ((Int -> Int) -> Int)>"++tdn3_show = tdn_show tdn3+-- "<function of the type (Int -> (Int -> Int))>"++tdn1_eval = tdn_eval1 tdn1 (+4)+-- Nothing++tdn2_eval = tdn_eval1 tdn2 (+4)+-- Just "5"++tdn2_eval' = tdn_eval2 tdn2 3 14+-- Nothing++tdn3_eval = tdn_eval2 tdn3 3 14+-- Just "42"+++main = do+       print tt1_view+       print tt2_view+       print tt0_show+       print tt1_show+       print tdn1_show+       print tdn2_show+       print tdn3_show+       print tdn1_eval+       print tdn2_eval+       print tdn2_eval'+       print tdn3_eval

@@ -0,0 +1,359 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE Rank2Types, ExistentialQuantification #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies, UndecidableInstances #-}++-- |+-- Why all these extensions?+-- I could've cheated a bit and gotten by without the last four:+-- the function typecheck below is partial anyway.+-- If we permit one sort of errors (when the deserialized term is+-- ill-typed), we may as well permit another sort of errors+-- (a closed-looking term turns out open), even if the+-- latter sort of  error can't arise if our typecheck function is correct.+-- due to the desire to let GHC check some correctness properties+-- I wanted to avoid unnecessary errors and let GHC see the+-- correctness of my code to a larger extent+--+module Language.TypeCheck where++-- No Data.Typeable, no gcast. Everything is above the board+-- No import Data.Typeable++import Language.Typ hiding (main)   +-- Our version of Typeable+import Control.Monad+import Control.Monad.Error++import Language.TTFdB hiding (main')		+-- we use de Bruijn indices++++-- * Data type of trees representing our expressions `on the wire'+-- * Serialized expressions are _untyped_+-- All content is in the form of character string+-- Imagine the following to be XML, only more compact+data Tree = Leaf String			-- CDATA+	  | Node String [Tree]		-- element with its children+	    deriving (Eq, Read, Show)+++-- * Expression format (extensible)+-- *  Node "Int" [Leaf number]    -- int literal+-- *  Node "Add" [e1,e2]          -- addition+-- *  Node "App" [e1,e2]          -- application+-- *  Node "Var" [Leaf name]+-- *  Node "Lam" [Leaf name,e1,e2] -- e2 is body, e1 is type of var+-- *  ...+-- *+-- * Format of types+-- *  Node "TInt" []		-- Int+-- *  Node "TArr" [e1,e2]       -- e1 -> e2+-- *  ...++-- * Serialized expressions are in the Church-style+-- so that we won't need inference, only type checking+-- Inference is not hard here; It is orthogonal and obscures our goal+-- here of deserialization into a typed term++-- * //+-- * Desiderata+-- * Type check once, interpret many times+-- *   detect type-checking error _before_ evaluation+-- so that the evaluators can't possibly fail because+-- the serialized expression was ill-typed. That error should be+-- detected and handled earlier.+-- Desired function:+-- typecheck :: Tree -> ???+-- We will use de-Bruijn indices (why?)+-- typecheck :: Symantics repr => Tree -> repr h ???+-- We can use something like read:+--   read :: Read a => String -> a+-- but that defeats the purpose since we must know a.+-- We may want to deserialize the term and print it out. If our+-- typecheck is like read, we get the read-show problem.+-- * Avoiding read-show problem+-- We have to abstract over a: need Dynamics, or existentials++-- * Typing dynamic typing+-- * Type-safe cast++-- * //+-- Old approach (see IncopeTypecheck.hs)+-- The Show constraint is for debugging, so to see the result+-- DynTerm repr h should be the result of typecheck+-- * data DynTerm repr h = forall a. (Show a, Typeable a) => DynTerm (repr h a)++data DynTerm repr h = forall a. DynTerm (TQ a) (repr h a)++-- A sample `dynamic' object term+tdyn1 = DynTerm tint (lam z `app` (int 1))++-- Interpret many times+tdyn1_eval = case tdyn1 of DynTerm tr t -> show_as tr $ eval t+-- "1"++-- This test particularly shows that we don't even need to know+-- the type of term; eventually we get the string+tdyn1_view = case tdyn1 of DynTerm _ t -> view t+-- "((\\x0 -> x0) 1)"+++-- * //+-- * De-serialize type expressions+-- The serialized terms contain type annotations on bound variables.+-- We need to read the annotations and convert them to Haskell types.+-- But Haskell types are not terms! So, we have to produce a term+-- with the desired Haskell type: Typ.Typ++-- * Error monad, to report deserialization errors++-- The function read_t below is necessarily partial:+-- the type annotation in the Tree form can be wrong, for example,+-- (Node "Tarr" []).+-- To report the error meaningfully, we use the Error monad++-- We should have written read_t in the open recursion style,+-- so that it would be extensible.+-- But we omit the type extensibility here for the sake of clarity++read_t :: Tree -> Either String Typ+read_t (Node "TInt" [])  = return $ Typ tint+read_t (Node "TArr" [e1,e2]) = do+  Typ t1 <- read_t e1+  Typ t2 <- read_t e2+  return . Typ $ tarr t1 t2+read_t tree = fail $ "Bad type expression: " ++ show tree++-- * A few explanations are in order+-- The TArr clause operates on `some' types t1 and t2+++-- * //+-- * Type checking environment+-- Our deserializer `typecheck' is too necessarily partial.+-- Again we will use the error monad to report errors.+-- Thus the tentative type for typecheck is+-- * typecheck :: Symantics repr => +-- *	     Tree -> Either String (DynTerm h repr)+--+-- * Open terms may legitimately occur+-- First of all, when processing the body of abstractions.+-- Second, we may use `global constants' (standard Prelude, of sorts).+-- We therefore type-check in the type environment Gamma,+-- which is a map from variable names to their types. Hence+-- type-check should have this signature:+-- * typecheck :: Symantics repr => +-- *	     Tree -> Gamma -> Either String (DynTerm h repr)+-- But Gamma and h are related! We should make it explicit that+-- Gamma (type checking environment) determines h (the run-time environment+-- of a term).+-- *   Gamma is a compile-time environment: contains variable names+-- *   h is a run-time environment: contains values+-- Both environments are indexed by types of their elements; +-- since h is a nested tuple, so should be Gamma++type VarName = String+data VarDesc t = -- Component of Gamma+    VarDesc (TQ t) VarName ++-- * Relating Gamma and h+class Var gamma h | gamma -> h where+    findvar :: Symantics repr =>+	       VarName -> gamma -> Either String (DynTerm repr h)++-- Like asTypeOf, used to specialize polymorphic term repr h t+-- to a specific type t+asTypeRepr :: t -> repr h t -> repr h t+asTypeRepr _ = id++instance Var () () where+    findvar name _ = fail $ "Unbound variable: " ++ name++instance Var gamma h => Var (VarDesc t,gamma) (t,h) where+    findvar name (VarDesc tr name',_) | name == name' =+	 return $ DynTerm tr z++    findvar name (_,gamma) = do+         DynTerm tr v <- findvar name gamma+	 return $ DynTerm tr (s v)+++-- * //+typecheck :: (Symantics repr, Var gamma h) =>+	     Tree -> gamma -> Either String (DynTerm repr h)++typecheck (Node "Int" [Leaf str]) gamma =+    case reads str of+      [(n,[])] -> return $ DynTerm tint (int n)+      _        -> fail $ "Bad Int literal: " ++ str++typecheck (Node "Add" [e1, e2]) gamma = do+  DynTerm (TQ t1) d1 <- typecheck e1 gamma+  DynTerm (TQ t2) d2 <- typecheck e2 gamma+  case (as_int t1 d1, as_int t2 d2) of+    (Just t1', Just t2') -> return . DynTerm tint $ add t1' t2'+    (Nothing,_) -> fail $ "Bad type of a summand: " ++ view_t t1+    (_,Nothing) -> fail $ "Bad type of a summand: " ++ view_t t2+++typecheck (Node "Var" [Leaf name]) gamma = findvar name gamma++typecheck (Node "Lam" [Leaf name,etyp,ebody]) gamma = do+  Typ ta <- read_t etyp+  DynTerm tbody body  <- typecheck ebody (VarDesc ta name, gamma)+  return $ DynTerm (tarr ta tbody) (lam body)++typecheck (Node "App" [e1, e2]) gamma = do+  DynTerm (TQ t1) d1 <- typecheck e1 gamma+  DynTerm (TQ t2) d2 <- typecheck e2 gamma+  AsArrow _ arr_cast <- return $ as_arrow t1+  let errarr = fail $ "operator type is not an arrow: " ++ view_t t1+  (ta,tb,equ_t1ab) <- maybe errarr return arr_cast+  let df = equ_cast equ_t1ab d1+  case safe_gcast (TQ t2) d2 ta of +    Just da -> return . DynTerm tb $ app df da+    _ -> fail $ unwords ["Bad types of the application:", + 			 view_t t1, "and", view_t t2]++typecheck e gamma = fail $ "Invalid Tree: " ++ show e++-- Why the app case is complex, more complex than Add+-- The type of the argument is, well, existential++-- * //+-- * Simple tests++tx1 = typecheck +       (Node "Var" [Leaf "x"]) ()++tx2 = typecheck +       (Node "Lam" [Leaf "x",Node "TInt" [],+		    Node "Var" [Leaf "x"]]) ()+tx3 = typecheck +       (Node "Lam" [Leaf "x",Node "TInt" [],+	  Node "Lam" [Leaf "y",Node "TInt" [],+		    Node "Var" [Leaf "x"]]]) ()++tx4 = typecheck +       (Node "Lam" [Leaf "x",Node "TInt" [],+	  Node "Lam" [Leaf "y",Node "TInt" [],+	    Node "Add" [Node "Int" [Leaf "10"],+			Node "Var" [Leaf "x"]]]]) ()+++tx_view t = case t of+		 Right (DynTerm _ t) -> view t+		 Left err -> error err++tx1_view = tx_view tx1++tx4_view = tx_view tx4+-- "(\\x0 -> (\\x1 -> (10+x0)))"++-- * //+-- * Closed interpreter+-- to convert a monomorphic binding to polymorphic in tc_evalview+-- below.++newtype CL h a = CL{unCL :: forall repr. Symantics repr => repr h a}++instance Symantics CL where+    int x     = CL $ int x+    add e1 e2 = CL $ add (unCL e1) (unCL e2)+    z         = CL z+    s v       = CL $ s (unCL v)+    lam e     = CL $ lam (unCL e)+    app e1 e2 = CL $ app (unCL e1) (unCL e2)++-- * //+-- * Main tests+-- * Type-check once, evaluate many times+-- One may worry that each time we evaluate a deserialized term,+-- we are type checking it from scratch.+-- The following shows that it is not the case:+-- if Tree represents an ill-typed term, we determine an error+-- before we started evaluating it (many times).++tc_evalview exp = do+ DynTerm tr d <- typecheck exp ()+ let d' = unCL d				-- Make d polymorphic again+ return $ (show_as tr $ eval d',+	   view d')+ +-- * A few combinators to help build trees+-- XML, or even its abstractions, are too verbose+tr_int x = Node "Int" [Leaf $ show x]+tr_add e1 e2 = Node "Add" [e1, e2]+tr_app e1 e2 = Node "App" [e1, e2]+tr_lam v t e = Node "Lam" [Leaf v, t, e]+tr_var v = Node "Var" [Leaf v]++tr_tint = Node "TInt" []+tr_tarr t1 t2 = Node "TArr" [t1,t2]+++-- dt1:: Symantics repr => DynTerm repr ()+dt1 = tc_evalview (tr_add (tr_int 1) (tr_int 2))+-- Right ("3","(1+2)")++dt2 = tc_evalview (tr_app (tr_int 1) (tr_int 2))+-- Left "operator type is not an arrow: Int"++dt4 = tc_evalview +       (tr_lam "x" tr_tint (tr_lam "y" (tr_tint `tr_tarr` tr_tint) +	    (tr_lam "z" tr_tint (tr_var "y"))))+-- Right ("<function of the type (Int -> ((Int -> Int) -> (Int -> (Int -> Int))))>",+--        "(\\x0 -> (\\x1 -> (\\x2 -> x1)))")++dt41 = tc_evalview +         (tr_lam "x" tr_tint (tr_lam "y" (tr_tint `tr_tarr` tr_tint) +	    (tr_lam "z" tr_tint (tr_var "x"))))+-- Right ("<function of the type (Int -> ((Int -> Int) -> (Int -> Int)))>",+--        "(\\x0 -> (\\x1 -> (\\x2 -> x0)))")+++dt5 = tc_evalview (tr_lam "x" tr_tint (tr_add (tr_var "x") (tr_int 1)))+-- Right ("<function of the type (Int -> Int)>",+--        "(\\x0 -> (x0+1))")++-- Making a deliberate mistake...+dt6 = tc_evalview (tr_lam "x" (tr_tint `tr_tarr` tr_tint)+	            (tr_add (tr_var "x") (tr_int 1)))+-- Left "Bad type of a summand: (Int -> Int)"++-- Untyped Church Numeral 2+exp_n2 = (tr_lam "f" (tr_tint `tr_tarr` tr_tint)+          (tr_lam "x" tr_tint+	      (tr_app (tr_var "f") (tr_app (tr_var "f") (tr_var "x")))))++dt7 = tc_evalview exp_n2+-- Right ("<function of the type ((Int -> Int) -> (Int -> Int))>",+--        "(\\x0 -> (\\x1 -> (x0 (x0 x1))))")++dt8 = tc_evalview +        (tr_app (tr_app exp_n2 +           (tr_lam "x" tr_tint (tr_add (tr_var "x") (tr_var "x"))))+           (tr_int 11))+-- Right ("44",+--        "(((\\x0 -> (\\x1 -> (x0 (x0 x1)))) (\\x0 -> (x0+x0))) 11)")+++-- Exercise: add open recursion to typecheck, so to make+-- it extensible. Add the Mul alternative, or booleans++main' = do+       print tdyn1_eval+       print tdyn1_view+       print tx4_view++       print dt1+       print dt2+       print dt4+       print dt41+       print dt5+       print dt6+       print dt7+       print dt8

@@ -1,13 +1,13 @@ name:           liboleg-version:        2010.1.2+version:        2010.1.5 license:        BSD3 license-file:   LICENSE author:         Oleg Kiselyov maintainer:     Don Stewart <dons@galois.com> homepage:       http://okmij.org/ftp/ category:       Text-synopsis:       A collection of Oleg Kiselyov's Haskell modules (2008-2010)-description:    A collection of Oleg Kiselyov's Haskell modules (2008-2010) (released with his permission)+synopsis:       An evolving collection of Oleg Kiselyov's Haskell modules+description:    An evolving collection of Oleg Kiselyov's Haskell modules (released with his permission) build-type:     Simple stability:      experimental cabal-version:  >= 1.2@@ -24,12 +24,14 @@             Data.FDList             Data.Class1             Data.Class2+            Data.Numerals              Control.CaughtMonadIO             Control.ShiftResetGenuine             Control.VarStateM             Control.ExtensibleDS             Control.Poly2+            Control.StateAlgebra              Codec.Image.Tiff @@ -47,7 +49,15 @@             Language.TEval.TInfTEnv             Language.TEval.TInfTM             Language.CB+            Language.CBAny+            Language.CPS             Language.CB98+            Language.TTF+            Language.TTFdB+            Language.TDPE+            Language.ToTDPE+            Language.Typ+            Language.TypeCheck              Text.PrintScan             Text.PrintScanF