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