{-# LANGUAGE NoMonomorphismRestriction #-}

-- |
-- * Essentially, Haskell98!
-- * Typed tagless-final interpreters for simply-typed lambda-calculus
-- * de Bruijn indices
-- based on the code accompanying the paper by
--   Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan

module Language.TTFdB where

-- * Abstracting over the final interpreter in IntroHOIF.hs

-- This class defines syntax (and its instances, semantics) 
-- of our language

-- I could've moved s and z into a separate ``class Var var_repr''
-- Symantics would then have a single form
-- v :: var_repr h a -> repr h a

class Symantics repr where
    int :: Int -> repr h Int                -- int literal
    add :: repr h Int -> repr h Int -> repr h Int

    z   :: repr (a,h) a			-- variables: z and s ... (s z)
    s   :: repr h a -> repr (any,h) a
    lam :: repr (a,h) b  -> repr h (a->b)
    app :: repr h (a->b) -> repr h a -> repr h b

-- * Like GADT-based, but in lower-case
-- * Like ExpSYM, but repr is of kind * -> * -> *
-- repr is parameterized by the environment (h) and the type
-- of the expression
-- * The types read like the rules of minimal logic
-- For example, z is the axiom stating that assuming A we can get A
-- lam is the inference rule: if assuming A we derive B,
-- then we can derive the implication A->B
-- * Type system of simply-typed lambda-calculus in Haskell98!
-- The signature of the class can be read off as the typing
-- rules for simply-typed lambda-calculus. But the code
-- is Haskell98! So, contrary to the common belief, we do not
-- need dependent types to express the type system of simply
-- typed lambda-calculus. Compare with Term.agda
-- * ``a way to write a typed fold function over a typed term.''
-- as one reviewer of our paper put it


-- * Sample terms and their inferred types
td1 = add (int 1) (int 2)
-- td1 :: (Symantics repr) => repr h Int

td2 = lam (add z z)
-- td2 :: (Symantics repr) => repr h (Int -> Int)

td2o = lam (add z (s z))
-- td2o :: (Symantics repr) => repr (Int, h) (Int -> Int)
-- the inferred type says td2o is open! Needs the env with Int

td3 = lam (add (app z (int 1)) (int 2))
-- td3 :: (Symantics repr) => repr h ((Int -> Int) -> Int)

-- Ill-typed terms are not expressible
-- * td2a = app (int 1) (int 2)
--     Couldn't match expected type `a -> b' against inferred type `Int'
--       Expected type: repr h (a -> b)
--       Inferred type: repr h Int
--     In the first argument of `app', namely `(int 1)'

-- * Embedding all and only typed terms of the object language
-- * in the typed metalanguage
-- Typed object terms are represented as typed Haskell terms


-- * //
-- * Typed and tagless evaluator
-- *  object term ==> metalanguage value

newtype R h a = R{unR :: h -> a}

instance Symantics R where
    int x     = R $ const x
    add e1 e2 = R $ \h -> (unR e1 h) + (unR e2 h)

    z     = R $ \(x,_) -> x
    s v   = R $ \(_,h) -> unR v h
    lam e = R $ \h -> \x -> unR e (x,h)
    app e1 e2 = R $ \h -> (unR e1 h) (unR e2 h)

eval e = unR e ()			-- Eval in the empty environment

-- * R is not a tag!
-- The expression with unR _looks_ like tag introduction and
-- elimination. But the function unR is *total*. There is no 
-- run-time error is possible at all -- and this fact is fully 
-- apparent to the compiler.
-- * R is a meta-circular interpreter
-- It runs each object-language operation by executing the corresponding
-- metalanguage operation.
-- * R never gets stuck: no variant types, no pattern-match failure
-- * Well-typed programs indeed don't go wrong!
-- * R is total
-- * The instance R is a constructive proof of type soundness
-- First of all, we see the type preservation (for object types)
-- for interpretations: interpretations preserve types.
-- Then we see progress: the interpreter does not get stuck.
-- So we reduced the problem of type soundness of the object language
-- (simply-typed lambda-calculus) to the type soundness of the
-- metalanguage.
-- * R _looks_ like a reader monad (but h varies)
-- R looks like a reader monad, but the type of the environment
-- varies.

-- Evaluate our test expressions
td1_eval = eval td1
-- 3

td2_eval = eval td2
-- td2_eval :: Int -> Int -- can't print
-- since td2_eval is a function taking Int, we can give it an Int
td2_eval' = eval td2 21
-- 42

-- td2o_eval = eval td2o
-- Can't evaluate the open term

td3_eval = eval td3
-- td3_eval :: (Int -> Int) -> Int

-- * //
-- Another interpreter

newtype S h a = S{unS :: [String] -> String}

instance Symantics S where
    int x     = S $ const $ show x
    add e1 e2 = S $ \h -> 
      "(" ++ unS e1 h ++ "+" ++ unS e2 h ++ ")"

    z     = S $ \(x:_) -> x
    s v   = S $ \(_:h) -> unS v h
    lam e = S $ \h -> 
       let x = "x" ++ show (length h)
       in "(\\" ++ x ++ " -> " ++ unS e (x:h) ++ ")"
    app e1 e2 = S $ \h -> 
      "(" ++ unS e1 h ++ " " ++ unS e2 h ++ ")"

-- Now this is almost the Reader monad. Why not fully?
-- The interpretation of lam is quite different from that in R
-- The environment is a regular, homogeneous list now
-- (see the rules 's' and 'z')

view :: S () a -> String -- Only closed terms can be viewed
view e = unS e []

td1_view = view td1
-- "(1+2)"

td2_view = view td2
-- "(\\x0 -> (x0+x0))"

td3_view = view td3
-- "(\\x0 -> ((x0 1)+2))"

-- We now finally see our terms in a useful form
-- Clearly, de Bruijn notation is not the most perspicuous
-- We now turn to HOAS

-- Exercise: implement the following extensions
{-

-- * //
-- Extensions of the language

-- * Multiplication
class MulSYM repr where
    mul :: repr r Int -> repr r Int -> repr r Int

-- * Booleans
class BoolSYM repr where
    bool :: Bool -> repr r Bool             -- bool literal
    if_ :: repr r Bool -> repr r a -> repr r a -> repr r a
    leq :: repr r Int -> repr r Int -> repr r Bool

-- * Fixpoint
class FixSYM repr where
    fix :: repr (a,h) a  -> repr h a

-- Logically, the signature of fix reads like nonsense
-- The extensions are independent

testpowfix () = lam {- x -} (
                  fix {- self -} (lam {- n -} (
                  let n = z; self = s z; x = s (s z)    
                  in  if_ (leq n (int 0)) (int 1)
                          (mul x (app self (add n (int (-1))))))))
testpowfix7 () = lam (app (app (testpowfix ()) z) (int 7))

rtestpw   = mkrtest testpowfix
rtestpw7  = mkrtest testpowfix7
rtestpw72 = mkrtest (\() -> app (testpowfix7 ()) (int 2)) -- 128

-- Another interpreter: it interprets each term to give its size
-- (the number of constructors)
-}

main' = do
       print td1_eval
       print td2_eval'
       print td1_view
       print td2_view
       print td3_view