gadts.purs

-- This file is copy&pasteable into
-- http://try.purescript.org/
--
-- 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

existsEquals
    :: 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))