#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
#endif
module Proof.Equational ( (:~:)(..), (:=:)
, sym, trans
, Equality(..), Preorder(..), reflexivity'
, (:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)
, Reason(..), because, by, (===), start, byDefinition
, admitted, Proxy(..), cong, cong'
, Proposition(..), HVec(..), FromBool (..)
, applyNAry, applyNAry', fromBool'
, fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
, coerce, coerce', withRefl
, module Data.Singletons, module Data.Proxy
) where
import Data.Proxy
import Data.Singletons
import Data.Type.Equality hiding (apply)
import Unsafe.Coerce
infix 4 :=:
type a :\/: b = Either a b
infixr 2 :\/:
type a :/\: b = (a, b)
infixr 3 :/\:
type (:=:) = (:~:)
data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
leibnizToRefl :: Leibniz a b -> a :=: b
leibnizToRefl eq = apply eq Refl
fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b
fromLeibniz eq = apply eq (reflexivity sing)
fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b
fromRefl Refl = reflexivity'
reflToLeibniz :: a :=: b -> Leibniz a b
reflToLeibniz Refl = Leibniz id
class Preorder (eq :: k -> k -> *) where
reflexivity :: Sing a -> eq a a
transitivity :: eq a b -> eq b c -> eq a c
class Preorder eq => Equality (eq :: k -> k -> *) where
symmetry :: eq a b -> eq b a
instance Preorder (:=:) where
transitivity Refl Refl = Refl
reflexivity _ = Refl
instance Equality (:=:) where
symmetry Refl = Refl
instance Preorder (->) where
reflexivity _ = id
transitivity = flip (.)
leibniz_refl :: Leibniz a a
leibniz_refl = Leibniz id
instance Preorder Leibniz where
reflexivity _ = leibniz_refl
transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb
instance Equality Leibniz where
symmetry eq = unFlip $ apply eq $ Flip leibniz_refl
newtype Flip f a b = Flip { unFlip :: f b a }
data Reason eq x y where
Because :: Sing y -> eq x y -> Reason eq x y
reflexivity' :: (SingI x, Preorder r) => r x x
reflexivity' = reflexivity sing
by, because :: Sing y -> eq x y -> Reason eq x y
because = Because
by = Because
infixl 4 ===, =<=, =~=, =>=
infix 5 `Because`
infix 5 `because`
(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
eq =<= (_ `Because` eq') = transitivity eq eq'
(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
eq =>= (_ `Because` eq') = transitivity eq' eq
(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
(===) = (=<=)
(=~=) :: r x y -> Sing y -> r x y
eq =~= _ = eq
start :: Preorder eq => Sing a -> eq a a
start = reflexivity
byDefinition :: (SingI a, Preorder eq) => eq a a
byDefinition = reflexivity sing
admitted :: Reason eq x y
admitted = undefined
cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
cong Proxy Refl = Refl
cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b
cong' _ Refl = Refl
coerce :: (a :=: b) -> f a -> f b
coerce _ a = unsafeCoerce a
coerce' :: a :=: b -> a -> b
coerce' _ a = unsafeCoerce a
withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
Refl -> r
class Proposition (f :: k -> *) where
type OriginalProp (f :: k -> *) (n :: k) :: *
unWrap :: f n -> OriginalProp f n
wrap :: OriginalProp f n -> f n
data HVec (xs :: [*]) where
HNil :: HVec '[]
(:-) :: x -> HVec xs -> HVec (x ': xs)
infixr 9 :-
type family (xs :: [*]) :~> (a :: *) :: * where
'[] :~> a = a
(x ': xs) :~> a = x -> (xs :~> a)
infixr 1 :~>
data HVecView (xs :: [*]) :: * where
HNilView :: HVecView '[]
HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
deriving instance Show (HVecView xs)
class KnownTypeList (xs :: [*]) where
viewHVec' :: HVecView xs
instance KnownTypeList '[] where
viewHVec' = HNilView
instance KnownTypeList ts => KnownTypeList (t ': ts) where
viewHVec' = HConsView Proxy viewHVec'
newtype Magic (xs :: [*]) a = Magic { _viewHVec' :: KnownTypeList xs => a }
withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' HNilView f = f HNil
apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $
apply' ts (\ts' -> f $ a :- ts')
applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
applyNAry = apply' (viewHVec' :: HVecView ts)
applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' _ _ = applyNAry
class FromBool (c :: *) where
type Predicate c :: Bool
type Args c :: [*]
fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c , Predicate c ~ 'True) => proxy c -> Args c :~> c
fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool