diff --git a/Control/StateAlgebra.hs b/Control/StateAlgebra.hs new file mode 100644 --- /dev/null +++ b/Control/StateAlgebra.hs @@ -0,0 +1,137 @@ +{-# OPTIONS -fglasgow-exts #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Implementing the State Monad as a term 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) diff --git a/Data/Numerals.hs b/Data/Numerals.hs new file mode 100644 --- /dev/null +++ b/Data/Numerals.hs @@ -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 +-- +-- +-- + +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 + diff --git a/Language/CBAny.hs b/Language/CBAny.hs new file mode 100644 --- /dev/null +++ b/Language/CBAny.hs @@ -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 diff --git a/Language/CPS.hs b/Language/CPS.hs new file mode 100644 --- /dev/null +++ b/Language/CPS.hs @@ -0,0 +1,439 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE UndecidableInstances #-} + +-- |- +-- +-- +-- 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 diff --git a/Language/TDPE.hs b/Language/TDPE.hs new file mode 100644 --- /dev/null +++ b/Language/TDPE.hs @@ -0,0 +1,165 @@ +{-# LANGUAGE NoMonomorphismRestriction #-} + +-- | +-- Type-directed partial evaluation, Olivier Danvy, POPL96 +-- * +-- +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 diff --git a/Language/TTF.hs b/Language/TTF.hs new file mode 100644 --- /dev/null +++ b/Language/TTF.hs @@ -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 +-- +-- +-- +-- +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 diff --git a/Language/TTFdB.hs b/Language/TTFdB.hs new file mode 100644 --- /dev/null +++ b/Language/TTFdB.hs @@ -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 + diff --git a/Language/ToTDPE.hs b/Language/ToTDPE.hs new file mode 100644 --- /dev/null +++ b/Language/ToTDPE.hs @@ -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) diff --git a/Language/Typ.hs b/Language/Typ.hs new file mode 100644 --- /dev/null +++ b/Language/Typ.hs @@ -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 (\_ -> "") +tt0_show = show_as tint 5 +-- "5" + +tt1_show = show_as tt1 undefined +-- " 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 +-- " Int) -> Int)>" + +tdn3_show = tdn_show tdn3 +-- " (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 diff --git a/Language/TypeCheck.hs b/Language/TypeCheck.hs new file mode 100644 --- /dev/null +++ b/Language/TypeCheck.hs @@ -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 (" ((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 (" ((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 (" 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 (" 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 diff --git a/liboleg.cabal b/liboleg.cabal --- a/liboleg.cabal +++ b/liboleg.cabal @@ -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 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