{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
#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',
-- * Conversion between equalities
fromRefl,
fromLeibniz,
reflToLeibniz,
leibnizToRefl,
-- * Coercion
coerce,
coerceInner,
coerce',
withRefl,
-- * Re-exported modules
module Data.Proxy,
) where
import Data.Kind (Type)
import Data.Proxy
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) => Leibniz a b -> eq a b
fromLeibniz eq = apply eq (reflexivity Proxy)
fromRefl :: (Preorder eq) => a :=: b -> eq a b
fromRefl Refl = reflexivity'
reflToLeibniz :: a :=: b -> Leibniz a b
reflToLeibniz Refl = Leibniz id
class Preorder (eq :: k -> k -> Type) where
reflexivity :: proxy a -> eq a a
transitivity :: eq a b -> eq b c -> eq a c
class (Preorder eq) => Equality (eq :: k -> k -> Type) where
symmetry :: eq a b -> eq b a
instance Preorder (:=:) where
{-# SPECIALIZE instance Preorder (:=:) #-}
transitivity Refl Refl = Refl
{-# INLINE [1] transitivity #-}
reflexivity _ = Refl
{-# INLINE [1] reflexivity #-}
instance Equality (:=:) where
{-# SPECIALIZE instance Equality (:~:) #-}
symmetry Refl = Refl
{-# INLINE [1] symmetry #-}
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 :: proxy y -> eq x y -> Reason eq x y
reflexivity' :: (Preorder r) => r x x
reflexivity' = reflexivity Proxy
by, because :: proxy 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'
{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
(=>=) :: (Preorder r) => r y z -> Reason r x y -> r x z
eq =>= (_ `Because` eq') = transitivity eq' eq
{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
(===) :: (Equality eq) => eq x y -> Reason eq y z -> eq x z
(===) = (=<=)
{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
(=~=) :: r x y -> proxy y -> r x y
eq =~= _ = eq
start :: (Preorder eq) => proxy a -> eq a a
start = reflexivity
byDefinition :: (Preorder eq) => eq a a
byDefinition = reflexivity Proxy
admitted :: Reason eq x y
admitted = undefined
{-# WARNING admitted "There are some goals left yet unproven." #-}
cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
cong Proxy Refl = Refl
cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
cong' _ Refl = Refl
{- | Type coercion. 'coerce' is using @unsafeCoerce a@.
So, please, please do not provide the @undefined@ as the proof.
Using this function instead of pattern-matching on equality proof,
you can reduce the overhead introduced by run-time proof.
-}
coerceInner, coerce :: (a :=: b) -> f a -> f b
{-# DEPRECATED coerce "Use coerceInner instead" #-}
coerce = coerceInner
{-# INLINE coerce #-}
coerceInner _ = unsafeCoerce
{-# INLINE [1] coerceInner #-}
-- | Coercion for identity types.
coerce' :: a :=: b -> a -> b
coerce' _ = unsafeCoerce
{-# INLINE [1] coerce' #-}
{-# RULES
"coerce/unsafeCoerce" [~1] forall xs.
coerceInner xs =
unsafeCoerce
"coerce'/unsafeCoerce" [~1] forall xs.
coerce' xs =
unsafeCoerce
#-}
{- | Solves equality constraint without explicit coercion.
It has the same effect as @'Data.Type.Equality.gcastWith'@,
but some hacks is done to reduce runtime overhead.
-}
withRefl :: forall a b r. a :~: b -> ((a ~ b) => r) -> r
withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b)
class Proposition (f :: k -> Type) where
type OriginalProp (f :: k -> Type) (n :: k) :: Type
unWrap :: f n -> OriginalProp f n
wrap :: OriginalProp f n -> f n
data HVec (xs :: [Type]) where
HNil :: HVec '[]
(:-) :: x -> HVec xs -> HVec (x ': xs)
infixr 9 :-
type family (xs :: [Type]) :~> (a :: Type) :: Type where
'[] :~> a = a
(x ': xs) :~> a = x -> (xs :~> a)
infixr 1 :~>
data HVecView (xs :: [Type]) :: Type where
HNilView :: HVecView '[]
HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
deriving instance Show (HVecView xs)
class KnownTypeList (xs :: [Type]) where
viewHVec' :: HVecView xs
instance KnownTypeList '[] where
viewHVec' = HNilView
instance (KnownTypeList ts) => KnownTypeList (t ': ts) where
viewHVec' = HConsView Proxy viewHVec'
newtype Magic (xs :: [Type]) 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 :: Type) where
type Predicate c :: Bool
type Args c :: [Type]
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