diff --git a/Control/Poly2.hs b/Control/Poly2.hs
new file mode 100644
--- /dev/null
+++ b/Control/Poly2.hs
@@ -0,0 +1,269 @@
+{-# OPTIONS -fglasgow-exts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE OverlappingInstances #-}
+
+-- | Type-class overloaded functions: second-order typeclass programming
+-- with backtracking
+--
+-- <http://okmij.org/ftp/Haskell/types.html#poly2>
+--
+module Control.Poly2 where
+
+-- | The classes of types used in the examples below
+--
+type Fractionals = Float :*: Double :*: HNil
+type Nums = Int :*: Integer :*: AllOf Fractionals :*: HNil
+type Ords = Bool :*: Char :*: AllOf Nums :*: HNil
+type Eqs  = AllOf (TypeCl OpenEqs) :*: AllOfBut Ords Fractionals :*: HNil
+
+
+-- | The Fractionals, Nums and Ords above are closed. But Eqs is open
+-- (i.e., extensible), due to the following:
+data OpenEqs
+instance TypeCls OpenEqs () HTrue -- others can be added in the future
+
+-- | Why we call Nums etc. a type class rather than a type set?
+-- The following does not work: type synonyms can't be recursive.
+--
+-- > type Russel = AllOfBut () Russel :*: HNil
+--
+-- But the more elaborate version does, with the expected result:
+--
+data RusselC
+instance Apply (Member Russel) x r => TypeCls RusselC x r
+type Russel = AllOfBut () (TypeCl RusselC) :*: HNil
+
+-- The following leads to predictable context stack overflow
+-- testr = apply (undefined::Member Russel) True
+
+-- Type class membership testing
+--
+data AllOf x
+data AllOfBut x y
+data TypeCl x
+
+-- | Classifies if the type x belongs to the open class labeled l
+-- The result r is either HTrue or HFalse
+class TypeCls l x r | l x -> r
+
+-- | the default instance: x does not belong
+instance TypeCast r HFalse => TypeCls l x r
+
+-- | Deciding the membership in a closed class, specified
+-- by enumeration, union and difference
+--
+data Member tl
+instance Apply (Member HNil) x HFalse
+
+instance TypeCls l x r => Apply (Member (TypeCl l)) x r
+
+instance (TypeEq h x bf, MemApp bf t x r) 
+    => Apply (Member (h :*: t)) x r
+
+instance (Apply (Member h) x bf, MemApp bf t x r)
+    => Apply (Member ((AllOf h) :*: t)) x r
+
+instance (Apply (Member exc) x bf, Apply (MemCase2 h t x) bf r)
+    => Apply (Member ((AllOfBut h exc) :*: t)) x r
+
+class MemApp bf t x r | bf t x -> r
+instance MemApp HTrue t x HTrue
+instance Apply (Member t) x r => MemApp HFalse t x r
+
+-- | we avoid defining a new class like MemApp above.
+-- I guess, after Apply, we don't need a single class ever?
+data MemCase2 h t x
+instance Apply (Member t) x r => Apply (MemCase2 h t x) HTrue r
+instance Apply (Member ((AllOf h) :*: t)) x r 
+    => Apply (MemCase2 h t x) HFalse r
+
+testm1 = apply (undefined::Member Fractionals) (1::Float)
+testm2 = apply (undefined::Member Fractionals) (1::Int)
+testm3 = apply (undefined::Member Fractionals) ()
+
+
+-- The implementation of the second-order polymorphic functions
+
+-- | A type class for instance guards and back-tracking
+-- Here, pred and f are labels and n is of a kind numeral.
+--
+class GFN n f a pred | n f a -> pred
+
+-- | The guard that always succeeds (cf. `otherwise' in Haskell)
+data Otherwise
+instance Apply Otherwise a HTrue
+
+newtype GFn f    = GFn f
+newtype GFnA n f = GFnA f
+
+newtype GFnTest n f flag = GFnTest f
+
+instance (GFN Z f a pred, Apply pred a flag,
+	  Apply (GFnTest Z f flag) a b)
+    => Apply (GFn f) a b where
+    apply (GFn f) a = apply ((GFnTest f)::GFnTest Z f flag) a
+
+instance Apply (GFnA n f) a b		-- guard succeeded
+    => Apply (GFnTest n f HTrue) a b where
+    apply (GFnTest f) a = apply ((GFnA f) :: GFnA n f) a
+
+instance (GFN (S n) f a pred, Apply pred a flag, -- else chose the next inst
+	  Apply (GFnTest (S n) f flag) a b)
+    => Apply (GFnTest n f HFalse) a b where
+    apply (GFnTest f) a = apply ((GFnTest f)::GFnTest (S n) f flag) a
+
+
+
+-- It's time for tests
+-- | A generic function that tests if its argument is a member of Eqs
+--
+data IsAnEq = IsAnEq			-- define the label for our function
+
+-- | Each case of a 2-poly function is defined by two instances,
+-- of GFN and or Apply classes.
+instance GFN Z IsAnEq a (Member Eqs)
+instance Apply (GFnA Z IsAnEq) a Bool where
+    apply _ _ = True
+
+-- | the default instance
+instance TypeCast pred Otherwise => GFN n IsAnEq a pred
+instance Apply (GFnA n IsAnEq) a Bool where
+    apply _ _ = False
+
+test1 = [apply (GFn IsAnEq) (), apply (GFn IsAnEq) (1.0::Double),
+	 apply (GFn IsAnEq) 'a']
+-- [True,False,True]
+
+-- | Augment the above function, to test for pairs of Eqs
+-- We could have added an instance to TypeCls OpenEqs above. But we wish
+-- to show off the recursive invocation of a second-order polymorphic 
+-- function
+--
+instance GFN (S Z) IsAnEq (x,y) Otherwise
+
+instance (Apply (GFn IsAnEq) x Bool,
+	  Apply (GFn IsAnEq) y Bool)
+    => Apply (GFnA (S Z) IsAnEq) (x,y) Bool where
+    apply (GFnA f) (x,y) = apply (GFn f) x && apply (GFn f) y
+
+
+test2 = [apply (GFn IsAnEq) (True,'a'),
+	 apply (GFn IsAnEq) (1.0::Double,True)]
+-- [True, False]
+
+
+-- | The main test: approximate equality. See the article for
+-- the description.
+--
+data PairOf t
+instance Apply t x r => Apply (PairOf t) (x,x) r
+instance TypeCast r HFalse => Apply (PairOf t) x r
+
+testmp1 = apply (undefined::PairOf (Member Fractionals)) 
+	  ((1::Float),(1::Float))
+testmp2 = apply (undefined::PairOf (Member Fractionals)) 
+	  ((1::Integer),(1::Integer))
+testmp3 = apply (undefined::PairOf (Member Nums)) 
+	  ((1::Integer),(1::Integer))
+
+
+data ApproxEq = ApproxEq		-- define the label
+
+-- GFN instance has no constraints!
+instance GFN Z ApproxEq (x,x) (PairOf (Member Fractionals))
+instance (Fractional x, Ord x) =>
+    Apply (GFnA Z ApproxEq) (x,x) Bool where
+    apply _ (x,y) = abs (x - y) < 0.5
+
+instance GFN (S Z) ApproxEq (x,x) (PairOf (Member Nums))
+instance (Num x, Ord x) =>
+    Apply (GFnA (S Z) ApproxEq) (x,x) Bool where
+    apply _ (x,y) = abs (x - y) < 2
+
+instance GFN (S (S Z)) ApproxEq (x,x) (PairOf (Member Eqs))
+instance (Eq x) =>
+    Apply (GFnA (S (S Z)) ApproxEq) (x,x) Bool where
+    apply _ (x,y) = x == y
+
+-- Show off the recursive invocation
+instance GFN (S (S (S Z))) ApproxEq ((x,x),(x,x))
+             (PairOf (PairOf (Member Nums)))
+instance (Apply (GFn ApproxEq) (x,x) Bool, Eq x) =>
+    Apply (GFnA (S (S (S Z))) ApproxEq) ((x,x),(x,x)) Bool where
+    apply _ ((x1,x2),(y1,y2)) = apply (GFn ApproxEq) (x1,y1) &&
+				x2 == y2
+
+-- The default instance
+instance TypeCast pred Otherwise => GFN n ApproxEq a pred
+instance Apply (GFnA n ApproxEq) a Bool where
+    apply _ _ = False
+
+-- A convenient abbreviation
+approx_eq x y = apply (GFn ApproxEq) (x,y)
+
+test3 = [approx_eq (1.0::Double) (1.5::Double),
+	 approx_eq (1.0::Float) (1.1::Float),
+	 approx_eq (1::Integer) (2::Integer),
+	 approx_eq (1::Int) True,
+	 approx_eq (Just ()) [],
+	 approx_eq ((2::Integer),(2::Integer)) ((1::Integer),(2::Integer)),
+	 approx_eq ((1::Integer),(2::Integer)) ((1::Integer),(2::Integer)) ]
+-- [False,True,True,False,False,True,True]
+
+
+-- The order matters	 
+data ApproxEq' = ApproxEq'		-- define the label
+
+instance GFN (S Z) ApproxEq' (x,x) (PairOf (Member Fractionals))
+instance (Fractional x, Ord x) =>
+    Apply (GFnA (S Z) ApproxEq') (x,x) Bool where
+    apply _ (x,y) = abs (x - y) < 0.5
+
+instance GFN Z ApproxEq' (x,x) (PairOf (Member Nums))
+instance (Num x, Ord x) =>
+    Apply (GFnA Z ApproxEq') (x,x) Bool where
+    apply _ (x,y) = abs (x - y) < 2
+
+-- The default instance
+instance TypeCast pred Otherwise => GFN n ApproxEq' a pred
+instance Apply (GFnA n ApproxEq') a Bool where
+    apply _ _ = False
+
+test4 = apply (GFn ApproxEq') ((1.0::Double),(1.5::Double))
+-- True
+
+
+-- The standard HList stuff, extracted from HList library
+
+
+data HNil = HNil
+data a :*: b = a :*: b
+infixr 5 :*:
+data HTrue
+data HFalse
+
+data Z = Z
+newtype S n = S n
+
+
+class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
+class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
+class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
+instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
+instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
+instance TypeCast'' () a a where typeCast'' _ x  = x
+
+class  TypeEq x y b | x y -> b
+instance TypeEq x x HTrue
+instance TypeCast HFalse b => TypeEq x y b
+
+
+-- A heterogeneous apply operator
+
+class Apply f a r | f a -> r where
+  apply :: f -> a -> r
+  apply = undefined
+
+-- Normal function application
+instance Apply (x -> y) x y where
+  apply f x = f x
diff --git a/Language/CB.hs b/Language/CB.hs
new file mode 100644
--- /dev/null
+++ b/Language/CB.hs
@@ -0,0 +1,276 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- | 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 in the same Final Tagless framework
+--
+-- <http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any>
+--
+
+module Language.CB where
+
+import Data.IORef
+import Control.Monad
+import Control.Monad.Trans
+
+-- | Our EDSL is typed. EDSL types are built from the following two
+-- type constructors:
+data IntT
+data a :-> b
+infixr 5 :->
+
+-- | We could have used Haskell's type Int and the arrow -> constructor.
+-- We would like to emphasize however that EDSL types need not be identical
+-- to the host language types. To give the type system to EDSL, we merely
+-- need `labels' -- which is what IntT and :-> are
+--
+-- The (higher-order abstract) syntax of our DSL
+class EDSL exp where
+     lam :: (exp a -> exp b) -> exp (a :-> b)
+     app :: exp (a :-> b) -> exp a -> exp b
+
+     int :: Int -> exp IntT		-- Integer literal
+     add :: exp IntT -> exp IntT -> exp IntT
+     sub :: exp IntT -> exp IntT -> exp IntT
+
+-- | A convenient abbreviation
+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 IntT
+t = (lam $ \x -> let_ (x `add` x)
+                      $ \y -> y `add` y) `app` int 10
+
+
+-- | Interpretation of EDSL types as host language types
+-- The type interpretation function Sem is parameterized by 'm',
+-- which is assumed to be a Monad.
+type family Sem (m :: * -> *) a :: *
+type instance Sem m IntT      = Int
+type instance Sem m (a :-> b) = m (Sem m a) -> m (Sem m b)
+
+-- | Interpretation of EDSL expressions as values of the host language (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).
+-- (S l m) is not quite a monad -- only up to the Sem interpretation
+newtype S l m a = S { unS :: m (Sem m a) }
+
+
+
+
+-- | Call-by-name
+--
+data Name
+instance MonadIO m => EDSL (S Name m) where
+  int = S . return
+  add x y = S $ do a <- unS x
+                   b <- unS y
+                   liftIO $ putStrLn "Adding"
+                   return (a + b)
+  sub x y = S $ do a <- unS x
+                   b <- unS y
+                   liftIO $ putStrLn "Subtracting"
+                   return (a - b)
+  lam f   = S . return $ (unS . f . S)
+  app x y = S $ unS x >>= ($ (unS y))
+
+
+-- Tests
+runName :: S Name m a -> m (Sem m a)
+runName x = unS x
+
+-- | Evaluating:
+--
+-- > t = (lam $ \x -> let_ (x `add` x)
+-- >                      $ \y -> y `add` y) `app` int 10
+--
+-- 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 IntT
+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 IntT
+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
+
+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)
+    app x y = nv $ app (vn x) (vn 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   = S . return $ (\x -> x >>= unS . f . S . return)
+
+runValue :: S Value m a -> m (Sem 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
+
+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
+
+-- | We reuse most of EDSL (S Name) except for lam
+ln :: S Lazy m x -> S Name m x
+ln = S . unS
+nl :: S Name m x -> S Lazy m x
+nl = S . unS
+
+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)
+    app x y = nl $ app (ln x) (ln 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           = S . return $ (\x -> share x >>= unS . f . S)
+
+
+runLazy :: S Lazy m a -> m (Sem 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
+-}
diff --git a/Language/CB98.hs b/Language/CB98.hs
new file mode 100644
--- /dev/null
+++ b/Language/CB98.hs
@@ -0,0 +1,282 @@
+-- Haskell98!
+
+-- | 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 in the same Final Tagless framework
+-- This is the Haskell98 version of the code CB.hs located in the
+-- same directory as this file
+--
+-- <http://okmij.org/ftp/tagless-final/tagless-typed.html#call-by-any>
+--
+
+module Language.CB98 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
+     lam :: (exp a -> exp b) -> exp (Arr exp a b)
+     app :: exp (Arr exp a b) -> exp a -> exp b
+
+     int :: Int -> exp Int              -- Integer literal
+     add :: exp Int -> exp Int -> exp Int
+     sub :: exp Int -> exp Int -> exp Int
+
+-- | A convenient abbreviation
+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
+
+-- | Interpretation of EDSL expressions as values of the host language (Haskell)
+-- An EDSL expression of type a is interpreted as a Haskell value
+-- of the type SName m a, SValue m a or SLazy m a, where
+-- m is a Monad (the parameter of the interpretation).
+
+newtype SName m a = SN { unSN :: m a }
+
+-- | Could be automatically derived by GHC. But we stick to Haskell98
+instance Monad m => Monad (SName m) where
+    return = SN . return
+    m >>= f = SN $ unSN m >>= unSN . f
+instance MonadIO m => MonadIO (SName m) where
+    liftIO = SN . liftIO
+
+
+-- | Call-by-name
+--
+instance MonadIO m => EDSL (SName 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 :: SName m a -> m a
+runName x = unSN 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
+--
+newtype SValue m a = SV { unSV :: m a }
+
+-- | Could be automatically derived by GHC. 
+instance Monad m => Monad (SValue m) where
+    return = SV . return
+    m >>= f = SV $ unSV m >>= unSV . f
+instance MonadIO m => MonadIO (SValue m) where
+    liftIO = SV . liftIO
+
+-- | We reuse most of EDSL (SName) except for lam
+vn :: SValue m x -> SName m x
+vn = SN . unSV
+nv :: SName m x -> SValue m x
+nv = SV . unSN
+
+instance MonadIO m => EDSL (SValue 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 SName'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 :: SValue m a -> m a
+runValue x = unSV 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
+--
+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
+
+newtype SLazy m a = SL { unSL :: m a }
+
+-- | Could be automatically derived by GHC. 
+instance Monad m => Monad (SLazy m) where
+    return = SL . return
+    m >>= f = SL $ unSL m >>= unSL . f
+instance MonadIO m => MonadIO (SLazy m) where
+    liftIO = SL . liftIO
+
+ln :: SLazy m x -> SName m x
+ln = SN . unSL
+nl :: SName m x -> SLazy m x
+nl = SL . unSN
+-- We reuse most of EDSL (SName) except for lam
+instance MonadIO m => EDSL (SLazy 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 SName'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 :: SLazy m a -> m a
+runLazy x = unSL 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
+-}
diff --git a/liboleg.cabal b/liboleg.cabal
--- a/liboleg.cabal
+++ b/liboleg.cabal
@@ -1,13 +1,13 @@
 name:           liboleg
-version:        2010.1.1
+version:        2010.1.2
 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 (2009-2008)
-description:    A collection of Oleg Kiselyov's Haskell modules (2009-2008) (released with his permission)
+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)
 build-type:     Simple
 stability:      experimental
 cabal-version:  >= 1.2
@@ -29,6 +29,7 @@
             Control.ShiftResetGenuine
             Control.VarStateM
             Control.ExtensibleDS
+            Control.Poly2
 
             Codec.Image.Tiff
 
@@ -45,6 +46,8 @@
             Language.TEval.TInfT
             Language.TEval.TInfTEnv
             Language.TEval.TInfTM
+            Language.CB
+            Language.CB98
 
             Text.PrintScan
             Text.PrintScanF