Index: /sizechecking/branches/macs/Lambda.hs
===================================================================
--- /sizechecking/branches/macs/Lambda.hs	(revision 25)
+++ /sizechecking/branches/macs/Lambda.hs	(revision 26)
@@ -1,3 +1,3 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilies, GADTs #-}
 
 module Lambda where
@@ -36,5 +36,4 @@
     else showChar $ C.chr $ C.ord 'a' + x
 
--- unS :: Value supply -> Precedence -> ShowS
 newtype S a = S { unS :: S.Supply Int -> Int -> ShowS }
 
@@ -59,23 +58,16 @@
 
 
-type family Sem (m :: * -> *) a :: *
-type instance Sem m Int      = Int
-type instance Sem m (a -> b) = m (Sem m a) -> m (Sem m b)
+{-
+ - reduction
+ -}
+data IR h t where
+    Lit :: Int -> IR h Int
+    App :: IR h (a -> b) -> IR h a -> IR h b
+    Lam :: (IR h a -> IR h b) -> IR h (a -> b)
 
-newtype R m a = R { unR :: m (Sem m a) }
+instance Lambda (IR h) where
+    lam = Lam
+    app = App
+    lit = Lit
 
-share :: (MonadIO m) => m a -> m (m a)
-share f = do
-    mem <- liftIO $ newIORef (False, f)
-    return $ do
-        (evald, thunk) <- liftIO $ readIORef mem
-        if evald then thunk
-        else do
-          value <- thunk
-          liftIO $ writeIORef mem (True, return value)
-          return value
-
-instance (MonadIO m) => Lambda (R m) where 
-    app x y = R $ unR x >>= ($ (unR y))
-    lit = R . return
-    lam f   = R . return $ (\x -> share x >>= unR . f . R)
+toFinal :: (Lambda l) => IR h t
Index: /sizechecking/branches/macs/Tests/LambdaTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/LambdaTest.hs	(revision 25)
+++ /sizechecking/branches/macs/Tests/LambdaTest.hs	(revision 26)
@@ -9,4 +9,11 @@
 test1 :: (Lambda l) => l Int
 test1 = app (lam $ \_ -> lit 3) (lit 2)
+
+const2 :: (Lambda l) => l ( Int -> Int )
+const2 = lam $ \_ -> lit 2
+
+t3 :: (Lambda l) => l ( (a -> a) -> (a -> a) )
+t3 = (lam $ \f -> lam $ \v -> f `app` (f `app` (f `app` v)))
+
 
 test1ast :: IO Bool