--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module : Type.Logic
--Author : Daniel Schüssler
--License : BSD3
--Copyright : Daniel Schüssler
--
--Maintainer : Daniel Schüssler
--Stability : Experimental
--Portability : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description :
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}
-- |
--
-- Propositions as types (of kind @*@), proofs as values
--
module Type.Logic where
import Data.Type.Equality
import Control.Monad.Cont
import Data.Typeable
import Data.Monoid hiding(All)
import Control.Exception
-- class Prop p where
-- proofs :: [p]
-- instance (Prop a, Prop b) => Prop (Either a b) where
-- proofs = diagonal [ fmap Left proofs, fmap Right proofs ]
-- instance (Prop a, Prop b) => Prop (a, b) where
-- proofs = liftM2 (,) proofs proofs
-- instance (Prop a, Prop b) => Prop (a -> b) where
-- proofs = case
newtype Falsity = Falsity { elimFalsity :: forall a. a }
deriving Typeable
-- instance Prop Falsity where proofs = []
-- instance Show Falsity where show _ = error "show: Proof of Falsity used"
data Truth = TruthProof
deriving (Show,Typeable)
-- instance Prop Truth where proofs = [TruthProof]
type Not a = a -> Falsity
instance Typeable a => (Show (a -> Falsity)) where
show _ = "<< proof of falsity from " ++ show (typeOf (undefined :: a)) ++ " >>"
-- | This class collects lemmas. It plays no foundational role.
class Fact a where
auto :: a
-- -- | Priority 1 facts
-- class Fact1 a where
-- auto1 :: a
-- instance Fact1 a => Fact a where
-- auto = auto1
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
-- )
-- isLeft :: Either t t1 -> Bool
-- isLeft (Left _) = True
-- isLeft (Right _) = False
-- isRight = not . isLeft
-- instance Show (a :=: b) where show Refl = "Refl"
class Decidable a where decide :: Either (Not a) a
instance (Decidable Falsity) where
decide = (Left id)
instance (Decidable Truth) where
decide = (Right TruthProof)
instance (Decidable a, Decidable b) => Decidable (a,b) where
decide = (case (decide ,decide ) of
(Right p, Right q) -> Right (p,q)
(Left p, _) -> Left (p . fst)
(_, Left q) -> Left (q . snd)
)
instance (Decidable a, Decidable b) => Decidable (Either a b) where
decide = (case (decide ,decide ) of
(Left p, Left q) -> Left (either p q)
(Right p, _) -> Right (Left p)
(_, Right q) -> Right (Right q)
)
instance (Decidable a, Decidable b) => Decidable (a -> b) where
decide = (case decide of
Right q -> Right (const q)
Left q -> case decide of
Right p -> Left (\f -> q (f p))
Left p -> Right (elimFalsity . p)
)
instance (Decidable a) => Decidable (Not a) where
decide = (case decide of
Right p -> Left ($p)
Left p -> Right p
)
-- | Existential quantification
data Ex p where
Ex :: 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))
-- | Universal quantification
newtype All p = All { allElim :: forall b. p b }
instance Fact (All p -> p b) where auto = allElim
-- | Unique existence
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"
class Decidable1 s where
decide1 :: Either (Not (s a)) (s a)
class Finite s where
enum :: [Ex s]
instance Finite s => Decidable (Ex s) where
decide = case enum of
[] -> Left (\_ -> Falsity (assert False undefined))
[x] -> Right x
-- instance Finite s => Decidable (Ex s) where
-- decide = case enum of
-- [] -> Left (\_ -> Falsity (assert False undefined))
-- [x] -> Right x