Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
-- This file is copy&pasteable into
-- That fore dependencies are inlined (and renamed), i.e. Equals, Exists and Product.
module Main where
import Prelude
import Data.Either
import Data.Tuple
import Data.Maybe
import Control.Monad.Eff
import Control.Monad.Eff.Console (log)
-- Equality
newtype Equals a b = Refl (forall c. c a -> c b)
subst :: forall a b c. Equals a b -> c a -> c b
subst (Refl f) x = f x
-- | Equality is reflexive
refl :: forall a. Equals a a
refl = Refl id
newtype Symm p a b = Symm (p b a)
-- | Equality is symmetric
symm :: forall a b. Equals a b -> Equals b a
symm p = case subst p (Symm refl) of Symm s -> s
-- | Equality is transitive
trans :: forall a b c. Equals a b -> Equals b c -> Equals a c
trans = flip subst
newtype Coerce a = Coerce a
-- | If two things are equal you can convert one to the other
coerce :: forall a b. Equals a b -> a -> b
coerce f a = case (subst f (Coerce a)) of Coerce b -> b
-- Exists
newtype Exists f = MkExists (forall r. (forall a. f a -> r) -> r)
runExists :: forall r f. Exists f -> (forall a. f a -> r) -> r
runExists (MkExists f) x = f x
mkExists :: forall f a. f a -> Exists f
mkExists x = MkExists (\f -> f x)
-- Product
newtype Product f g a = Product (Tuple (f a) (g a))
-- | Create a product.
product :: forall f g a. f a -> g a -> Product f g a
product fa ga = Product (Tuple fa ga)
data LExpr a
= LZero (Equals Int a)
| LSucc (Equals Int a) (LExpr a)
| LBool (Equals Boolean a) Boolean
| LEq (Equals Boolean a) (Exists LEqP)
type LEqP = Product LExpr LExpr
lzero :: LExpr Int
lzero = LZero refl
lsucc :: LExpr Int -> LExpr Int
lsucc = LSucc refl
lbool :: Boolean -> LExpr Boolean
lbool = LBool refl
leq :: forall a. LExpr a -> LExpr a -> LExpr Boolean
leq x y = LEq refl (mkExists (product x y))
lType :: forall a. LExpr a -> Either (Equals a Int) (Equals a Boolean)
lType (LZero proof) = Left (symm proof)
lType (LSucc proof _) = Left (symm proof)
lType (LBool proof _) = Right (symm proof)
lType (LEq proof _ ) = Right (symm proof)
succ :: Int -> Int
succ x = 1 + x
lToInt :: LExpr Int -> Int
lToInt (LZero _proof) = 0
lToInt (LSucc _proof n) = succ (lToInt n)
-- But now exhaustiveness checker complains about LBool and LEq cases?
-- Well, as we have Bool := Int "proof", we'll just use it!
lToInt (LBool proof b) = coerce proof b -- coerce :: a := b -> a -> b
lToInt l@(LEq proof _uv) = coerce proof (lToBool (subst (symm proof) l))
lToBool :: LExpr Boolean -> Boolean
lToBool e@(LZero proof) = coerce proof (lToInt (subst (symm proof) e))
lToBool e@(LSucc proof _) = coerce proof (lToInt (subst (symm proof) e))
lToBool (LBool proof b) = coerce proof b
lToBool (LEq _proof e) = runExists e (\(Product (Tuple u v)) -> case lType u of
Left proof -> lToInt (subst proof u) == lToInt (subst proof v)
Right proof -> lToBool (subst proof u) == lToBool (subst proof v))
lequals :: forall a b. LExpr a -> LExpr b -> Maybe (Equals a b)
lequals (LZero p) (LZero q) = Just (trans (symm p) q)
lequals (LSucc p n) (LSucc q m) = do
_proof <- lequals n m
pure (trans (symm p) q)
lequals (LBool p a) (LBool q b)
| a == b = Just (trans (symm p) q)
| otherwise = Nothing
lequals (LEq p xy) (LEq q uv)
| existsEquals lequals' xy uv = Just (trans (symm p) q)
| otherwise = Nothing
lequals _ _ = Nothing
lequals' :: forall a b. (Product LExpr LExpr) a -> (Product LExpr LExpr) b -> Maybe (Equals a b)
lequals' (Product (Tuple x y)) (Product (Tuple u v)) = do
proof <- lequals x u
_proof <- lequals y v -- it's irrelevant which proof we pick!
pure proof
:: forall f. (forall a b. f a -> f b -> Maybe (Equals a b))
-> Exists f -> Exists f
-> Boolean
existsEquals eq ex ey =
runExists ex (\x ->
runExists ey (\y ->
case eq x y of
Just _ -> true
Nothing -> false))
one :: LExpr Int
one = lsucc lzero
two :: LExpr Int
two = lsucc one
main = do
log (show $ lToInt two)
log (show $ lToBool $ leq two two)
log (show $ lToBool $ leq two one)
log (show $ isJust $ lequals one (lbool true))
log (show $ isJust $ lequals one two)
log (show $ isJust $ lequals (leq one one) (leq (lsucc lzero) one))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment