e3.mana

------------------------------------------------------------------------------
--
--  Generic Expression Gadt
--
------------------------------------------------------------------------------

namespace E3

  import Core

  ------------------------------------------------------------------------------
  --  E - expressions
  ------------------------------------------------------------------------------

  type E : Type -> Type where
    EX     : a -> E a
    EApply : E (a -> b) -> E a -> E b

  ------------------------------------------------------------------------------
  --
  ------------------------------------------------------------------------------

  lift1 : (a -> b) -> E a -> E b
  lift1 f e = EApply (EX f) e

  lift2 : (a -> b -> c) -> E a -> E b -> E c
  lift2 f e d = EApply (EApply (EX f) e) d

  instance FromInteger (E Int) where fromInteger = EX . fromInteger
  instance Add         (E Int) where (+) = lift2 (+)
  instance Multiply    (E Int) where (*) = lift2 (*)

  (===) = lift2 (== : Int -> Int -> Bool)

  ------------------------------------------------------------------------------
  --
  ------------------------------------------------------------------------------

  eval : E a -> a
  eval (EX     x  ) = x
  eval (EApply f x) = eval f (eval x)

  ------------------------------------------------------------------------------
  --
  ------------------------------------------------------------------------------

  main = do
    print <| eval <| (5 + 3 : E Int)
    print <| eval <| 5 === 3
    print <| eval <| lift1 not (5 === 3)
    print <| eval <| lift2 (+) (EX "hello ") (EX "world")