{-# LANGUAGE TypeSynonymInstances, PostfixOperators, ExistentialQuantification, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, FlexibleContexts , UndecidableInstances, KindSignatures, IncoherentInstances, ScopedTypeVariables, EmptyDataDecls, TypeFamilies, GADTs, RankNTypes, NoMonomorphismRestriction #-}

-- Simply typed lambda-calculus with named variables.

-- Names are of the form (S (S ... (S Z)...))
-- Contexts are lists (A1,(A2,...(An,())...))
-- where Ai refers to the variable with name i.
-- The type Ai is Unused if the variable is not used yet
-- or (Used A) if it is used and of type Ai.


data Z = Z
data S a = S a

data Used a = Used a
data Free a = Free a

data Dummy = Dummy

class IsEqAux a b | a -> b where
   iseqaux :: a -> b

instance IsEqAux a a where
   iseqaux x = x


class (IsEqAux a b, IsEqAux b a) => IsEq a b where
   iseqid :: a -> b

instance IsEq a a where
   iseqid x = iseqaux x



class AddVar x a c2 c1 | x a c1 -> c2 where
   add :: x -> a -> c2 -> c1

instance AddVar n a () () where
   add n a () = ()

instance IsEq a1 a2 => AddVar Z a1 (Free b,c) (Free a2,c) where
   add Z a (Free b,c) = (Free (iseqid a), c)

instance IsEq a1 a2 => AddVar Z a1 (Free b,c) (Used a2,c) where
   add Z a (Free b,c) = (Used (iseqid a), c)

instance (AddVar n a c d) => AddVar (S n) a (b,c) (b,d) where
   add (S n) a (b,c) = (b,add n a c)



class GetVar x a c | x a -> c where
  get_var :: c -> x -> a

instance GetVar Z a (Used a,()) where
  get_var (Used a,c) Z = a

instance GetVar n a c => GetVar (S n) a (Free u,c) where
  get_var (u,c) (S n) = get_var c n



class Zip c1 c2 c3 | c1 c2 -> c3 where
   split :: c3 -> (c1,c2)
instance Zip () c c where
   split c = ((),c)
instance Zip c () c where
   split c = (c,())
instance Zip () () () where
   split () = ((),())

instance (Zip c1 c2 c3, IsEq c a, IsEq c b) => Zip (Free a, c1) (Free b, c2) (Free c, c3) where
   split (Free c,c3) = let (c1,c2) = split c3 in ((Free (iseqid c),c1),(Free (iseqid c),c2))

instance (Zip c1 c2 c3, IsEq c a, IsEq c b) => Zip (Free a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Free (iseqid c),c1),(Used (iseqid c),c2))

instance (Zip c1 c2 c3, IsEq c a, IsEq c b) => Zip (Used a, c1) (Free b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used (iseqid c),c1),(Free (iseqid c),c2))

{- For linearity constraints, need to add an IsEq (Used a) (Free a) as constraints. -}
instance (Zip c1 c2 c3, IsEq c a, IsEq c b) => Zip (Used a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used (iseqid c),c1),(Used (iseqid c),c2))



data J c a = J (c -> a)

lamb :: (AddVar x a c2 c1) => x -> J c1 b -> J c2 (a -> b) 
lamb x (J f) = J (\c a -> f (add x a c))
appl :: Zip c1 c2 c3 => J c1 (a -> b) -> J c2 a -> J c3 b
appl (J f) (J g) = J (\x -> let (x1,x2) = split x in f x1 (g x2))
var :: (GetVar x a c) => x -> J c a
var x = J (\z -> get_var z x)



class Eval c a where
   eval :: (J c a) -> a

instance Eval () a where
   eval (J f) = f ()

instance (Eval c a, IsEq (Free Dummy) b) => Eval (b,c) a where
   eval (J f) = eval (J (\c -> f (iseqid (Free Dummy), c)))


{- Note that this does not work because we need to allow any b if we
   want the constraint to be satified.

instance (Eval c a) => Eval (Dummy,c) a where
   eval (J f) = eval (J (\c -> f (Dummy, c)))
-}


-- A few basic tests.

-- :t eval (lamb (S (S (S Z))) (var (S (S (S Z)))))
-- ==> :: a -> a

-- :t eval (lamb (S (S Z)) (lamb Z (var (S (S Z)))))
-- ==> :: a -> a1 -> a

-- :t eval (lamb (S (S Z)) (lamb Z (var Z)))
-- ==> :: a -> a1 -> a1

-- :t eval (lamb Z (lamb Z (var Z)))
-- ==> :: a -> a1 -> a1

-- :t eval (lamb Z (appl (var Z) (var Z)))
-- ==> Occurs check: cannot construct the infinite type:
--     a0 = a0 -> b0


-- the eval function takes a closed term.

-- :t eval (lamb (S (S (S Z))) (var Z))
-- ==> Couldn't match type `Unused' with `Used b0'
--     When using functional dependencies to combine
--     IsEqAux a a


-- We can combine open terms with Haskell's let construction to close
-- them later on.

-- :t eval (let x = (lamb (S (S Z)) (var Z)) in (lamb Z x))
-- ==> :: a1 -> a -> a1

-- :t eval (let x = (lamb (S (S Z)) (var Z)) in (lamb Z (appl x x)))
-- ==> :: a -> a

-- so this is consistent with the type system.