src/Logic/Kernel.hs

   1 -- For `proven`
   2 {-# LANGUAGE BangPatterns #-}
   3 -- For `Exists`
   4 {-# LANGUAGE ExistentialQuantification #-}
   5 -- For `Exists` instances
   6 {-# LANGUAGE QuantifiedConstraints #-}
   7 -- For `(=:)`
   8 {-# LANGUAGE RankNTypes #-}
   9 {-# LANGUAGE Safe #-}
  10 -- For `UnNamed` and `Exists` instances
  11 {-# LANGUAGE UndecidableInstances #-}
  12 -- For `letSymbol`
  13 -- {-# LANGUAGE AllowAmbiguousTypes #-}
  14 -- For pattern `Named`
  15 {-# LANGUAGE ViewPatterns #-}
  16
  17 module Logic.Kernel (
  18   type (:::) (),
  19   pattern Named,
  20   (...),
  21   unitName,
  22   type UnNamed,
  23   type UnName,
  24   unName,
  25   letName,
  26   letName2,
  27   letName3,
  28   letName4,
  29   liftName,
  30   liftName2,
  31   liftName3,
  32   liftName4,
  33   -- letSymbol,
  34   namedAs,
  35   (=:),
  36   type Proof (),
  37   proven,
  38   implies,
  39   unImplies,
  40   type Provable (..),
  41   type Axiom (..),
  42   type Lemma (..),
  43   type SuchThat (),
  44   type (/),
  45   (/),
  46   suchThatProof,
  47   type That (..),
  48   type (<->),
  49   (-->),
  50   (<--),
  51   type Exists (..),
  52   type EqUnNamed,
  53   type Commutative,
  54   type Associative,
  55   type RefHoTTBook,
  56 ) where
  57
  58 import Control.Applicative (Applicative (..))
  59 import Control.Monad (Monad (..))
  60 import Data.Eq (Eq (..))
  61 import Data.Function ((.))
  62 import Data.Functor (Functor (..))
  63 import Data.Ord (Ord (..))
  64 import Data.Tuple (fst, snd)
  65 import Text.Show (Show (..), showParen, showString)
  66 import Type.Reflection (Typeable, typeRep)
  67
  68 -- | A value of type @(a `:::` name)@ has the same runtime
  69 -- representation as a value of type @a@, with a nominal "name" attached.
  70 --
  71 -- The newtype constructor of `(:::)` is not exported
  72 -- as it would break the "smart constructor" confidence.
  73 newtype (:::) name a = NameAxiom a
  74   deriving (Eq, Ord)
  75
  76 instance Show a => Show (name ::: a) where
  77   showsPrec p (NameAxiom a) = showsPrec p a
  78
  79 type role (:::) nominal representational
  80 infixr 9 :::
  81
  82 -- | A safe pattern matcher to unwrap a name attached with `(:::)`.
  83 pattern Named :: UnName a => UnNamed a -> a
  84 pattern Named x <- (unName -> x)
  85
  86 {-# COMPLETE Named #-}
  87
  88 -- | Attach a name to a value of type @(a)@.
  89 -- This name must be inhabited,
  90 -- it means that if it's a data or newtype constructor,
  91 -- attaching such a name can be restricted to a module's boundary
  92 -- by not exporting that constructor out of that module.
  93 (...) :: name -> a -> name ::: a
  94 (...) _ = NameAxiom
  95
  96 infix 0 ...
  97
  98 {-# INLINE (...) #-}
  99
 100 unitName :: a -> () ::: a
 101 unitName = NameAxiom
 102 {-# INLINE unitName #-}
 103
 104 -- | Unwrap `(:::)` at the type-level.
 105 --
 106 -- This is not recursive like `coerce` would.
 107 type family UnNamed a where
 108   UnNamed (n ::: a) = a
 109   UnNamed (SuchThat a p) = UnNamed a
 110   UnNamed (That a pred x) = UnNamed (() ::: a `SuchThat` pred ())
 111   UnNamed a = a
 112
 113 -- | Unwrap `(:::)` at the value-level.
 114 --
 115 -- Note: this is not recursive like `Data.Coerce.coerce`.
 116 class UnName a where
 117   unName :: a -> UnNamed a
 118
 119 instance {-# OVERLAPS #-} UnName (n ::: a) where
 120   unName (NameAxiom a) = a
 121   {-# INLINE unName #-}
 122 instance {-# OVERLAPS #-} UnName a => UnName (SuchThat a p) where
 123   unName (SuchThat a) = unName a
 124   {-# INLINE unName #-}
 125 instance {-# OVERLAPS #-} UnName a => UnName (That a pred x) where
 126   unName (That a) = unName a
 127   {-# INLINE unName #-}
 128 instance UnNamed a ~ a => UnName a where
 129   unName a = a
 130   {-# INLINE unName #-}
 131
 132 -- | Introduce a name for the argument,
 133 -- and pass the named argument into the given function.
 134 letName :: a -> (forall x. x ::: a -> res) -> res
 135 letName x k = k (NameAxiom x)
 136 {-# INLINE letName #-}
 137
 138 infixr 0 `letName`
 139
 140 -- | Introduce names for two arguments,
 141 -- and pass the named arguments into the given function.
 142 letName2 :: a -> b -> (forall x y. x ::: a -> y ::: b -> res) -> res
 143 letName2 x y k = k (NameAxiom x) (NameAxiom y)
 144 {-# INLINE letName2 #-}
 145
 146 infixr 0 `letName2`
 147
 148 -- | Introduce names for three arguments,
 149 -- and pass the named arguments into the given function.
 150 letName3 :: a -> b -> c -> (forall x y z. x ::: a -> y ::: b -> z ::: c -> res) -> res
 151 letName3 x y z k = k (NameAxiom x) (NameAxiom y) (NameAxiom z)
 152 {-# INLINE letName3 #-}
 153
 154 infixr 0 `letName3`
 155
 156 -- | Introduce names for four arguments,
 157 -- and pass the named arguments into the given function.
 158 letName4 :: a -> b -> c -> d -> (forall x y z w. x ::: a -> y ::: b -> z ::: c -> w ::: d -> res) -> res
 159 letName4 x y z w k = k (NameAxiom x) (NameAxiom y) (NameAxiom z) (NameAxiom w)
 160 {-# INLINE letName4 #-}
 161
 162 infixr 0 `letName4`
 163
 164 -- \| Injects a `Symbol` into a `Type` for `letSymbol`.
 165 -- data Name (s :: Symbol)
 166
 167 -- \| Like `letName` but with a `Symbol` hint and a `Typeable` constraint
 168 -- enabling to `show` @(name)@.
 169 -- letSymbol :: forall (s :: Symbol) a res. KnownSymbol s => a -> (forall name. Typeable name => name ::: a -> res) -> res
 170 -- letSymbol a k =
 171 --  let n = hashUnique (unsafePerformIO newUnique)
 172 --  in case someSymbolVal (symbolVal (Proxy @s) <> show n) of
 173 --      SomeSymbol (Proxy :: Proxy n) ->
 174 --        k @(Name n) (NameAxiom a)
 175
 176 -- | Infix alias to `letName`.
 177 namedAs :: a -> (forall name. name ::: a -> res) -> res
 178 namedAs a k = k (NameAxiom a)
 179 {-# INLINE namedAs #-}
 180
 181 infixr 0 `namedAs`
 182
 183 -- | Introduce a name for the argument,
 184 -- and pass the named argument into the given function.
 185 liftName :: (forall x. x ::: a -> res) -> a -> res
 186 liftName k x = k (NameAxiom x)
 187 {-# INLINE liftName #-}
 188
 189 infixr 0 `liftName`
 190
 191 -- | Introduce names for two arguments,
 192 -- and pass the named arguments into the given function.
 193 liftName2 :: (forall x y. x ::: a -> y ::: b -> res) -> a -> b -> res
 194 liftName2 k x y = k (NameAxiom x) (NameAxiom y)
 195 {-# INLINE liftName2 #-}
 196
 197 infixr 0 `liftName2`
 198
 199 -- | Introduce names for three arguments,
 200 -- and pass the named arguments into the given function.
 201 liftName3 :: (forall x y z. x ::: a -> y ::: b -> z ::: c -> res) -> a -> b -> c -> res
 202 liftName3 k x y z = k (NameAxiom x) (NameAxiom y) (NameAxiom z)
 203 {-# INLINE liftName3 #-}
 204
 205 infixr 0 `liftName3`
 206
 207 -- | Introduce names for four arguments,
 208 -- and pass the named arguments into the given function.
 209 liftName4 :: (forall x y z w. x ::: a -> y ::: b -> z ::: c -> w ::: d -> res) -> a -> b -> c -> d -> res
 210 liftName4 k x y z w = k (NameAxiom x) (NameAxiom y) (NameAxiom z) (NameAxiom w)
 211 {-# INLINE liftName4 #-}
 212
 213 infixr 0 `liftName4`
 214
 215 -- | Operator version of `letName`.
 216 (=:) :: a -> (forall name. name ::: a -> res) -> res
 217 (=:) a k = k (NameAxiom a)
 218 {-# INLINE (=:) #-}
 219
 220 infixr 0 =:
 221
 222 -- | Here, a proposition in the logic side,
 223 -- is a type in the programming side.
 224 -- And a proven proposition is an inhabited type.
 225 --
 226 -- * `Logic.Name.RefHoTTBook`
 227 -- * https://groups.seas.harvard.edu/courses/cs152/2016sp/lectures/lec16-curryhoward.pdf
 228 -- * https://en.wikipedia.org/wiki/Type_inhabitation_problem
 229 -- * https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
 230 -- * https://ncatlab.org/nlab/show/propositions+as+types
 231 data Proof proposition = ProofAxiom
 232
 233 instance Typeable p => Show (Proof p) where
 234   showsPrec p _ =
 235     showParen
 236       (prec < p)
 237       ( showString "Proof "
 238           . showsPrec prec (typeRep @p)
 239       )
 240     where
 241       prec = 10
 242
 243 proven :: a -> Proof a
 244 proven !_ = ProofAxiom
 245 {-# INLINE proven #-}
 246
 247 type role Proof nominal
 248
 249 instance Functor Proof where
 250   fmap _f !_ = ProofAxiom
 251
 252 instance Applicative Proof where
 253   -- Observing an instance of 'a'
 254   -- Therefore, an instance of 'a' exists.
 255   pure !_ = ProofAxiom
 256   (<*>) !_ !_ = ProofAxiom
 257
 258 instance Monad Proof where
 259   -- There exist a proof that proves the existence of a proof of 'a'
 260   -- Therefore, a proof of 'a' exists.
 261   !_ >>= !_ = ProofAxiom
 262
 263 -- | The implication in the logic side,
 264 -- is the function type of the programming side.
 265 implies :: (Proof p -> Proof q) -> Proof (p -> q)
 266 implies !_ = ProofAxiom
 267 {-# INLINE implies #-}
 268
 269 -- | modus ponens
 270 unImplies :: Proof (p -> q) -> (Proof p -> Proof q)
 271 unImplies = (<*>)
 272 {-# INLINE unImplies #-}
 273
 274 -- | Reify a `Proof` or `(:::)` to inspect it.
 275 class Provable a where
 276   type ProofOf a
 277   prove :: a -> ProofOf a
 278
 279 -- nameProof :: ProofOf n a -> n ::: a
 280
 281 class Axiom p where
 282   -- | CorrectnessWarning: the default definition declares an axiom.
 283   -- This is the only way to declare an axiom out of this module
 284   -- (except through `undefined` or `TemplateHaskell` if LANGUAGE Safe is not used).
 285   --
 286   -- Beware that `Axiom` instances can be hidden from the documentation
 287   -- when not exporting a type involved in defining them,
 288   -- however their do appear in:
 289   --
 290   -- @
 291   -- ghci> :info! Axiom
 292   -- @
 293   axiom :: Proof p
 294   axiom = ProofAxiom
 295 {-# WARNING axiom "x-logic-axiom" #-}
 296
 297 class Lemma p where
 298   lemma :: Proof p
 299
 300 type (<->) p q = ((p -> q), (q -> p))
 301 infix 0 <->
 302
 303 (-->) :: (<->) p q -> p -> q
 304 (-->) = fst
 305 infix 9 -->
 306 {-# INLINE (-->) #-}
 307
 308 (<--) :: (<->) p q -> q -> p
 309 (<--) = snd
 310 infix 9 <--
 311 {-# INLINE (<--) #-}
 312
 313 type Commutative op x y = op x y <-> op y x
 314 type Associative op x y z = op (op x y) z <-> op x (op y z)
 315
 316 -- | Existential quantification.
 317 data Exists p = forall x. Exists (p x)
 318
 319 instance (forall x. Show (p x)) => Show (Exists p) where
 320   showsPrec p (Exists px) = showsPrec p px
 321
 322 -- | Class alias working around the impossibility
 323 -- to refer to the type family `UnNamed`
 324 -- in the quantified constraint of the @(`Eq` (`Exists` p))@ instance.
 325 --
 326 -- IssueRef: https://gitlab.haskell.org/ghc/ghc/-/issues/14860#note_495352
 327 class (Eq (UnNamed (p x)), UnName (p x), UnNamed (p x) ~ UnNamed (p y)) => EqUnNamed p x y
 328
 329 instance (Eq (UnNamed (p x)), UnName (p x), UnNamed (p x) ~ UnNamed (p y)) => EqUnNamed p x y
 330
 331 instance (forall x y. EqUnNamed p x y) => Eq (Exists p) where
 332   (==) (Exists (Named px)) (Exists (Named py)) = (==) px py
 333
 334 newtype SuchThat a p = SuchThat a
 335   deriving (Eq, Ord)
 336 type role SuchThat representational nominal
 337 infixr 0 `SuchThat`
 338 instance Show a => Show (SuchThat a p) where
 339   showsPrec p (SuchThat a) = showsPrec p a
 340
 341 -- | Convenient alias to `SuchThat`.
 342 type (/) = SuchThat
 343
 344 infixr 0 /
 345
 346 (/) :: a -> Proof p -> a `SuchThat` p
 347 (/) a ProofAxiom = SuchThat a
 348 {-# INLINE (/) #-}
 349
 350 suchThatProof :: a `SuchThat` p -> Proof p
 351 suchThatProof SuchThat{} = ProofAxiom
 352 {-# INLINE suchThatProof #-}
 353
 354 newtype That a p x = That (x ::: a `SuchThat` p x)
 355   deriving (Eq, Ord)
 356 type role That representational nominal nominal
 357 instance Show a => Show (That a p x) where
 358   showsPrec p (That a) = showsPrec p a
 359
 360 data RefHoTTBook
 361 -- ^ Reference to [Homotopy Type Theory: Univalent Foundations of Mathematics](https://homotopytypetheory.org/book)
 362 --
 363 -- > [
 364 -- >   {
 365 -- >     "author": [
 366 -- >       {
 367 -- >         "family": "Univalent Foundations Program",
 368 -- >         "given": "The"
 369 -- >       }
 370 -- >     ],
 371 -- >     "id": "hottbook",
 372 -- >     "issued": {
 373 -- >       "date-parts": [
 374 -- >         [
 375 -- >           2013
 376 -- >         ]
 377 -- >       ]
 378 -- >     },
 379 -- >     "publisher": "https://homotopytypetheory.org/book",
 380 -- >     "publisher-place": "Institute for Advanced Study",
 381 -- >     "title": "Homotopy Type Theory: Univalent Foundations of Mathematics",
 382 -- >     "title-short": "Homotopy Type Theory",
 383 -- >     "type": "book"
 384 -- >   }
 385 -- > ]