Foundations for proving stuff in PureScript

Leibniz.purs

{-
A bunch of useful primitives when using PureScript to prove *things*.

Idea of using Leibniz equality comes from http://code.slipthrough.net/2016/08/10/approximating-gadts-in-purescript/
-}

module Leibniz where

import Prelude ((<<<), ($))
import Unsafe.Coerce (unsafeCoerce)

--

data Id a = Id a

unId :: forall a. Id a -> a
unId (Id x) = x

--

newtype Flip f a b = Flip (f b a)

unFlip :: forall f a b. Flip f a b -> f b a
unFlip (Flip f) = f

--

newtype Comp f g a = Comp (f (g a))

unComp :: forall f g a. Comp f g a -> f (g a)
unComp (Comp fga) = fga

--

newtype Leibniz a b = Leibniz (forall p. p a -> p b)
infix 4 type Leibniz as ~

coe :: forall f a b. (a ~ b) -> f a -> f b
coe (Leibniz f) = f

cast :: forall a b. (a ~ b) -> a -> b
cast (Leibniz proof) a = unId $ proof (Id a)

refl :: forall a. a ~ a
refl = Leibniz (\x -> x)

trans :: forall a b c. (a ~ b) -> (b ~ c) -> (a ~ c)
trans (Leibniz a_eq_b) (Leibniz b_eq_c) = Leibniz (b_eq_c <<< a_eq_b)

symm :: forall a b. a ~ b -> b ~ a
symm l = unFlip $ coe l (Flip refl)

cong :: forall a b f. a ~ b -> f a ~ f b
cong p = Leibniz (unComp <<< coe p <<< Comp)

-- type constructors in purescript are injective. this is true, as there
-- is no computation done at the type level when applying a type constructor
-- (different from haskell's type families), but we can't actually prove it...
inj :: forall a b f. f a ~ f b -> a ~ b
inj = unsafeCoerce