Skip to content

Instantly share code, notes, and snippets.

@CarstenKoenig
Created March 20, 2018 12:22
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save CarstenKoenig/3e0db4ecaa813e6006e1d657f694efde to your computer and use it in GitHub Desktop.
simulating GADTs with Leibniz equality
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment