{-# LANGUAGE NoMonomorphismRestriction #-}

-- |
-- Type-directed partial evaluation, Olivier Danvy, POPL96
-- * <http://www.brics.dk/~danvy/tdpe-ln.pdf>
--
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