{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
-- Regardless of what the above declaration says, all our instances
-- here *are* decidable. By `decidable instances' GHC means
-- instances whose termination can be _easily_ decided locally, 
-- on the per-instance basis. Sometimes we need more extensive analysis.


-- Big-Lambda HOAS
-- Even higher-order abstract syntax: are GADTs compelling?

{- 
We show the typeclass implementation of the example used to make the
case for GADTs. We demonstrate the higher-order abstract-syntax-based
embedding of a language in Haskell and implement static and dynamic
semantics of the language. The interpreter of the language is tagless
and statically assured: Only well-typed terms may be evaluated, and
the evaluation of those does not get stuck. We use no tags and *no*
run-time pattern-matching, therefore, the `eval' function has no
possibility of raising a run-time error.  Our language is
_non_-strongly normalizing and non-structurally inductive due to the
presence of Fix; yet the typechecking is decidable and our typeclass
programs always terminate.

The running example has been used as an argument for generalized
recursive data types (one of the variants of GADTs). This
message is meant to clarify the expressiveness of GADTs with respect
to typeclasses. Our implementation is also aimed at the sometimes
exuberant enthusiasm for GADTs.

In positive contribution, we demonstrate the _automatic_ promotion of
a value-level higher-order abstract syntax (HOAS) term to the
type-level. The small-lambda HOAS becomes the big-Lambda HOAS and can
be operated by the typechecker. We demonstrate the typechecking of our
term language by abstract interpretation.  The latter is performed by
the Haskell typechecker itself, following straightforward declarative
rules expressed via instance declarations.  The code works in GHC and
Hugs.

Please see the accompanying article for more.

-}

module HOASL where

-- The following helper class represents (generally, untyped) 
-- functions in the object language. The end user will NOT write
-- any instances of the class, so this class does not have to be exported.
-- This class is instrumental in automatical lifting 
-- of Haskell functions into the object language, or the `lifting' of 
-- the value-level polymorphic functions onto the type level. 
-- That makes the big-lambda explicit and permits applications to it. 

class Apply f x y | f x -> y where
    apply :: f -> x -> y

-- The identity `function'. It is introduced for illustration only.
-- The end users will use the generic instance below for all their needs.
data ID
instance Apply ID x x where
    apply _ x = x

-- `Lifting' of ordinary, value-level polymorphic functions onto 
-- the `type level', to permit their typechecking by abstract
-- interpretation. 
-- The TypeCast below signifies the application of the Big Lambda.
instance TypeCast x x1 => Apply (x1 -> y) x y where
    apply f x = f (typeCast x)

-- The syntax of our terms
-- The terms containing binders (like Lam and Fix) should have the type
-- annotation on the bound variable (just as is the case for the code
-- in the GRDT paper). That type, however, can be inferred in many cases, as 
-- the examples below show.
newtype Lit a = Lit a			-- aka, Lift in GRDT
newtype Inc a = Inc a
newtype IsZ a = IsZ a
newtype If  a b c = If (a,b,c)
newtype Fst a = Fst a
newtype Snd a = Snd a
newtype Pair a b = Pair (a,b)

	-- Higher-order terms
newtype Lam f t = Lam f			-- t is the type of the bound arg
newtype App a b = App (a,b)
newtype Fix f t = Fix f			-- ditto


-- Hypothetical reasoning: used for typechecking functions
-- (aka typechecking by abstract interpretation). 
newtype AbsValue t = AbsValue t

-- Static semantics: well-formedness rules (aka, typing rules)
--	Of a t 
-- asserts the term a has the type t
class Of a t | a -> t

instance Of (Lit t) t
instance Of a Int => Of (Inc a) Int
instance Of a Int => Of (IsZ a) Bool
instance (Of t Bool, Of b1 a, Of b2 a) => Of (If t b1 b2) a
instance (Of t1 a, Of t2 b) => Of (Pair t1 t2) (a,b)
instance Of t (a,b) => Of (Fst t) a
instance Of t (a,b) => Of (Snd t) b
instance (Of a (t1->t2), Of b t1) => Of (App a b) t2

-- The Hyp elimination rule: we get what we assumed
instance Of (AbsValue t) t

-- The Hyp introduction rule: typechecking functions.
-- The function mapping the  term `a' to the term 'b'
-- has the type t1->t2, if the function maps the term AbsValue t1 
-- to the term that has the type t2.
-- In other words, if the body of the function has the type t2
-- _assuming_ the argument has the type t1.
instance (Apply f (AbsValue t1) y, Of y t2) => Of (Lam f t1) (t1->t2)

-- Ditto for the type-checking of Fix. Using of the AbsValue makes the
-- typechecking of the HOAS Fix terminating! Although we lack
-- structural induction, we do maintain decidability.
instance (Apply f (AbsValue t) y, Of y t) => Of (Fix f t) t


teval :: Of e t => e -> t		-- static evaluator
teval = undefined			-- all computation is static


-- Dynamic semantics: big-step evaluation

class Eval a t | a->t where
    eval:: a -> t

instance Of (Lit a) a => Eval (Lit a) a where
    eval (Lit i) = i
instance Eval t Int => Eval (Inc t) Int where
    eval (Inc t) = eval t + 1
instance Eval t Int => Eval (IsZ t) Bool where
    eval (IsZ t) = eval t == 0
instance (Eval t Bool, Eval b1 a, Eval b2 a) => Eval (If t b1 b2) a where
    eval (If (t,b1,b2)) = if eval t then eval b1 else eval b2
instance (Eval t1 a, Eval t2 b) => Eval (Pair t1 t2) (a,b) where
    eval (Pair (t1,t2)) = (eval t1, eval t2)
instance Eval t (a,b) => Eval (Fst t) a where
    eval (Fst t) = fst (eval t)
instance Eval t (a,b) => Eval (Snd t) b where
    eval (Snd t) = snd (eval t)


instance (Eval a (t1->t2), Eval b t1) => Eval (App a b) t2 where
    eval (App (a,b)) = (eval a) (eval b)

instance (Apply f (Lit t1) b, Eval b t2)
    => Eval (Lam f t1) (t1->t2) where
    eval (Lam f) = \x -> eval (apply f (Lit x))

-- Here, we convert the Fix to the value-level fix
instance (Apply f (Lit t) y, Eval y t)
    => Eval (Fix f t) t where
    eval (Fix f) = fix (\x -> eval $ apply f (Lit x))

fix f = f (fix f)



-- Tests

tl1 =  teval $ Lam (undefined::ID)
t2  =   eval $ Fix (undefined::ID)

-- the test from the first-order language

t3 = If ( (IsZ (Fst (Pair (Lit (0::Int), Lit (1::Int)))))
        , (Inc (Fst (Pair (Lit (0::Int), Lit (1::Int)))))
        , (Inc (Snd (Pair (Lit (0::Int), Lit (1::Int))))) )

et3 = eval t3 -- 1


-- Make t3 higher-order

t3f p = If ( (IsZ (Fst p)), (Inc (Fst p)), (Inc (Snd p)) )

et4f1 = teval $ Lam t3f
et4f2 =  eval $ Lam t3f
et4f3 = eval $ App (Lam t3f, (Pair (Lit (0::Int), Lit (1::Int))))


t5f = Lam $ \p -> If( IsZ p, (Pair (p,Inc p)), (Pair (p,Fix id)) )

et5f1 = teval $ t5f
et5f2 =  eval $ t5f
et5f3 =  eval $ App (t5f, Lit (0::Int)) -- yields (0,1)
et5f4t= teval $ App (t5f, Lit (1::Int)) -- typechecking terminates
et5f4 =  eval $ App (t5f, Lit (1::Int)) -- evaluation diverges!


-- The final test, that using Fix in a meaningful way.
-- We implement the addition: x + y -> z
-- Because we have the increment but don't have decrement, the
-- first argument must be given with the opposite sign.

t7 self = Lam f
 where
 f p = -- p is a (Pair x y) where x is negative
   If( IsZ (Fst p), Snd p,
      App (self, Pair ((Inc (Fst p)),Inc (Snd p))))

et71 = teval (Lam t7)
et72 = teval (Fix t7)
et73 = eval $ App (Fix t7,Pair(Lit(-5),Lit(4)))



-- to make the code self-contained

class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x