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