module Type.Logic where
import Data.Type.Equality
import Control.Monad.Cont
import Data.Typeable
import Data.Monoid hiding(All)
import Control.Exception
newtype Falsity = Falsity { elimFalsity :: forall a. a }
deriving Typeable
data Truth = TruthProof
deriving (Show,Typeable)
instance Show Falsity where show _ = error "show: Proof of Falsity used"
type Not a = a -> Falsity
instance Typeable a => (Show (a -> Falsity)) where
show _ = "<< proof of falsity from " ++ show (typeOf (undefined :: a)) ++ " >>"
class Fact a where
auto :: a
instance Fact Truth where
auto = TruthProof
instance Fact (Falsity -> a) where
auto = elimFalsity
instance Fact ((a,b) -> a) where
auto = fst
instance Fact ((a,b) -> b) where
auto = snd
instance (Fact a, Fact b) => Fact (a,b) where
auto = (auto, auto)
instance Fact (a -> Either a b) where
auto = Left
instance Fact (b -> Either a b) where
auto = Right
instance (Fact (a -> c), Fact (b -> c)) => Fact (Either a b -> c) where
auto = either auto auto
instance Fact (a -> Not (Not a)) where
auto p q = q p
data Decidable a = Decidable { decide :: Either (Not a) a }
deriving (Show,Typeable)
instance Fact (Decidable Falsity) where
auto = Decidable (Left id)
instance Fact (Decidable Truth) where
auto = Decidable (Right TruthProof)
instance Fact (Decidable a -> Decidable b -> Decidable (a,b)) where
auto p1 p2 = Decidable (case (decide p1,decide p2) of
(Right p, Right q) -> Right (p,q)
(Left p, _) -> Left (p . fst)
(_, Left q) -> Left (q . snd)
)
instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where
auto p1 p2 = Decidable (case (decide p1,decide p2) of
(Left p, Left q) -> Left (either p q)
(Right p, _) -> Right (Left p)
(_, Right q) -> Right (Right q)
)
instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where
auto p1 p2 = Decidable (case decide p2 of
Right q -> Right (const q)
Left q -> case decide p1 of
Right p -> Left (\f -> q (f p))
Left p -> Right (elimFalsity . p)
)
instance Fact (Decidable a -> Decidable (Not a)) where
auto p1 = Decidable (case decide p1 of
Right p -> Left ($p)
Left p -> Right p
)
data Ex p where
Ex :: forall b. p b -> Ex p
exElim :: forall p r. (forall b. p b -> r) -> Ex p -> r
exElim k (Ex prf) = k prf
instance (Fact (p a)) => Fact (Ex p) where auto = Ex (auto :: (p a))
newtype All p = All { allElim :: forall b. p b }
instance Fact (All p -> p b) where auto = allElim
data ExUniq p where
ExUniq :: p b -> (forall b'. p b' -> b :=: b') -> ExUniq p
instance Fact (ExUniq p -> Ex p) where
auto (ExUniq p _) = Ex p
instance Fact (ExUniq p -> p b -> p b' -> b :=: b') where
auto (ExUniq _ uniq) pb pb' =
case (uniq pb, uniq pb') of
(Refl,Refl) -> Refl
type COr r a b = Cont r (Either a b)
lem :: COr r (a -> r) a
lem = Cont (\k -> k (Left (\a -> k (Right a))))
elimCor :: COr r a b -> (a -> r) -> (b -> r) -> r
elimCor (Cont x) k1 k2 = x (either k1 k2)
deriving instance Typeable2 (:=:)
instance Show (a :=: b) where show Refl = "Refl"