simulating GADTs with Leibniz equality

Leibniz.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Leibniz where

-- WANT this without GADTS!:

data Form res where
  FInt  :: Int -> Form Int
  FAdd  :: Form Int -> Form Int -> Form Int
  FNull :: Form Int -> Form Bool


evalF :: Form res -> res
evalF (FInt i)   = i
evalF (FAdd a b) = evalF a + evalF b
evalF (FNull f)  = evalF f == 0


exampleF :: Bool
exampleF = evalF (FNull $ FAdd (FInt 2) (FInt (-2)))

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

-- use this nice represeantation of Leibniz-equality:
newtype LEq a b  = EqProof { applyL :: forall f . f a -> f b }

-- wrapper for identity
newtype Identity a = Identity { unIdent :: a }

-- use this to use an idenity-"proof" to coerce types in a safe way:
coerce :: LEq a b -> a -> b
coerce proof = unIdent . applyL proof . Identity


coerceSym :: LEq a b -> b -> a
coerceSym proof = coerce (sym proof)


-- the non-GADT type then just has to carry proofs around
data LeibnizGadt res
  = LInt  (LEq  Int res) Int
  | LAdd  (LEq  Int res) (LeibnizGadt Int) (LeibnizGadt Int)
  | LNull (LEq Bool res) (LeibnizGadt Int)


lInt :: Int -> LeibnizGadt Int
lInt n = LInt refl n


lNull :: LeibnizGadt Int -> LeibnizGadt Bool
lNull li = LNull refl li


lAdd :: LeibnizGadt Int -> LeibnizGadt Int -> LeibnizGadt Int
lAdd la lb = LAdd refl la lb


-- because of the carried-proof eval can coerce the concrete types into res
evalL :: LeibnizGadt res -> res
evalL (LInt  proof i)     = coerce proof i
evalL (LAdd  proof la lb) = coerce proof $ evalL la + evalL lb
evalL (LNull proof li)    = coerce proof $ evalL li == 0


exampleL :: Bool
exampleL = evalL (lNull $ lAdd (lInt 2) (lInt (-2)))


-- and just as with the real thing, this won't typecheck
-- malformed = lAdd (lInt 4) (lNull $ lInt 0)
-- and you should not get a value `LInt ?? 4 :: LeibnizGadt res`
-- for anything other than `res ~ Int` without cheating!
-- you should try to find ?? for say `LInt ?? 4 :: LeibnizGadt Bool` - have fun
-- btw: this is an example of cheating ;)
ohNoes :: LeibnizGadt Bool
ohNoes = LInt undefined 4

----------------------------------------------------------------------
-- equality is a equivalence relation:

refl :: LEq a a
refl = EqProof id


newtype FlipF f a b = FlipF { unflip :: f b a }

sym :: LEq a b -> LEq b a
sym proof = unflip $ applyL proof (FlipF refl)


trans :: LEq a b -> LEq b c -> LEq a c
trans proofAB proofBC = EqProof $ applyL proofBC . applyL proofAB