packages feed

gdp (empty) → 0.0.0.1

raw patch · 15 files changed

+1679/−0 lines, 15 filesdep +basedep +gdpdep +lawfulsetup-changed

Dependencies added: base, gdp, lawful

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Author name here (c) 2018++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,4 @@+# gdp: Ghosts of Departed Proofs+++
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs         #-}++module Main where++import GDP++import Data.Ord+import qualified Data.List as L++-- An unsafe merge. This relies on the user remembering to+-- sort both of the inputs using the same comparator passed+-- as the first argument to `unsafeMergeBy`. Otherwise, it+-- will produce nonsense.+unsafeMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]+unsafeMergeBy comp xs ys = go xs ys+  where+    go [] ys' = ys'+    go xs' [] = xs'+    go (x:xs') (y:ys') = case comp x y of+      GT -> y : go (x:xs') ys'+      _  -> x : go xs' (y:ys')+++-- Introduce a predicate `SortedBy comp`, indicating that+-- the value has been sorted by the comparator named `comp`.+newtype SortedBy comp name = SortedBy Defn++-- Sort a value using the comparator named `comp`. The+-- resulting value will satisfy `SortedBy comp`.+sortBy :: ((a -> a -> Ordering) ~~ comp)+       -> [a]+       -> ([a] ?SortedBy comp)+sortBy (The comp) xs = assert (L.sortBy comp xs)++-- Merge the two lists using the comparator named `comp`. The lists must+-- have already been sorted using `comp`, and the result will also be+-- sorted with respect to `comp`.+mergeBy :: ((a -> a -> Ordering) ~~ comp)+        -> ([a] ?SortedBy comp)+        -> ([a] ?SortedBy comp)+        -> ([a] ?SortedBy comp)+mergeBy (The comp) (The xs) (The ys) = assert (unsafeMergeBy comp xs ys)++newtype Opposite comp = Opposite Defn++-- A named version of the opposite ordering.+opposite :: ((a -> a -> Ordering) ~~ comp)+         -> ((a -> a -> Ordering) ~~ Opposite comp)+opposite (The comp) = defn $ \x y -> case comp x y of+  GT -> LT+  EQ -> EQ+  LT -> GT++newtype Reverse xs = Reverse Defn++-- A named version of Prelude's 'reverse'.+rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)+rev (The xs) = defn (reverse xs)++-- A lemma about reversing sorted lists.+rev_ord_lemma :: SortedBy comp xs -> Proof (SortedBy (Opposite comp) (Reverse xs))+rev_ord_lemma _ = axiom++-- Usage example.+main :: IO ()+main = do+  name compare $ \up -> do++    -- Read two lists and sort them in ascending order, then+    -- merge them and print the result.+    xs <- sortBy up <$> (readLn :: IO [Int])+    ys <- sortBy up <$> readLn+    let ans1 = mergeBy up xs ys+    print (the ans1)++    -- Now reverse the two lists and merge them using the+    -- descending comparator. This requires a proof that+    -- the reversed lists are sorted by the opposite of `up`,+    -- which we provide using (...?).+    let down = opposite up+        ans2 = mergeBy down (rev' xs) (rev' ys)+        rev' = rev ...? rev_ord_lemma+    print (the ans2)
+ gdp.cabal view
@@ -0,0 +1,51 @@+name:                gdp+version:             0.0.0.1+synopsis:            Reason about invariants and preconditions with ghosts of departed proofs.+description:         Reason about invariants and preconditions with ghosts of departed proofs.+                     The GDP library implements building blocks for creating and working with+                     APIs that may carry intricate preconditions for proper use. As a library+                     author, you can use `gdp` to encode your API's preconditions and invariants,+                     so that they will be statically checked at compile-time.+                     As a library user, you can use the `gdp` deduction rules to codify your+                     proofs that you are using the library correctly.+homepage:            https://github.com/githubuser/gdp#readme+license:             BSD3+license-file:        LICENSE+author:              Matt Noonan+maintainer:          matt.noonan@gmail.com+copyright:           (c) 2018 Matt Noonan+category:            Safe+build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     GDP+                     , Data.Arguments+                     , Data.Refined+                     , Data.The+                     , Logic.Classes+                     , Logic.NegClasses+                     , Logic.Propositional+                     , Logic.Proof+                     , Theory.Equality+                     , Theory.Named+                     +  build-depends:       base >= 4.7 && < 5+                     , lawful+                     +  default-language:    Haskell2010++executable gdp+  hs-source-dirs:      app+  main-is:             Main.hs+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  build-depends:       base+                     , gdp+                     +  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/matt-noonan/gdp
+ src/Data/Arguments.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}++{-|+  Module      :  Data.Arguments+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Data.Arguments+  ( Argument(..)+  , LHS, RHS+  , Arg(..)+  , arg+  ) where++-- | Get or modify a type within a larger type.+--   This is entirely a type-level operation, there+--   is nothing corresponding to a value access or update.+class Argument (f :: k1) (n :: k2) where+  type GetArg f n   :: k1+  type SetArg f n x :: k1++-- | Position: the left-hand side of a type.+data LHS++-- | Position: the right-hand side of a type.+data RHS++instance Argument (Either a b) LHS where+  type GetArg (Either a b) LHS    = a+  type SetArg (Either a b) LHS a' = Either a' b++instance Argument (Either a b) RHS where+  type GetArg (Either a b) RHS    = b+  type SetArg (Either a b) RHS b' = Either a b'++-- | A specialized proxy for arguments.+data Arg n = Arg++-- | Inhabitant of the argument proxy.+arg :: Arg n+arg = Arg+
+ src/Data/Refined.hs view
@@ -0,0 +1,177 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE FlexibleContexts      #-}++{-|+  Module      :  Data.Refined+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Data.Refined+  (  -- * Refinement types+    -- ** Attaching arbitrary propositions to values+    (:::)+  , (...)+  , (...>)+  , ($:)+  , exorcise+  , conjure++  -- ** Refinement types+  , Satisfies+  , type (?)+  , assert++  -- *** Forgetting and re-introducing names+  , unname+  , rename+  , (...?)++  -- *** Traversals over collections of refined types+  , traverseP, traverseP_+  , forP, forP_+  ) where++import Data.The+import Logic.Proof (Proof, axiom)+import Theory.Named++import Data.Coerce+import Data.Foldable (traverse_)++{--------------------------------------------------+  Attaching proofs to values+--------------------------------------------------}++{-| Given a type @a@ and a proposition @p@, the+    type @(a ::: p)@ represents a value of type @a@,+    with an attached "ghost proof" of @p@.++    Values of the type @(a ::: p)@ have+    the same run-time representation as values of+    the normal type @a@; the proposition @p@ does+    not carry a run-time space or time cost.+-}+newtype a ::: p = SuchThat a+infixr 1 :::++instance The a' a => The (a' ::: p) a where+  the (SuchThat x) = the x++-- | Given a value and a proof, attach the proof as a+--   ghost proof on the value.+(...) :: a -> Proof p -> (a ::: p)+x ...proof = coerce x++-- | Given a value and a proof, apply a function to the value+--   but leave the proof unchanged.+($:) :: (a -> b) -> (a ::: p) -> (b ::: p)+f $: x = coerce (f (exorcise x))++-- | Apply an implication to the ghost proof attached to a value,+--   leaving the value unchanged.+(...>) :: (a ::: p) -> (p -> Proof q) -> (a ::: q)+x ...> _ = coerce x++-- | Forget the ghost proof attached to a value.+exorcise :: (a ::: p) -> a+exorcise = coerce++-- | Extract the ghost proof from a value.+conjure :: (a ::: p) -> Proof p+conjure _ = axiom++{--------------------------------------------------+  Refinement types+--------------------------------------------------}++{-| Given a type @a@ and a predicate @p@, the type+    @a ?p@ represents a /refinement type/ for @a@.+    Values of type @a ?p@ should be values of type @a@+    that satisfy the predicate @p@.++    Values of type @a ?p@ have the same run-time representation+    as values of type @a@; the proposition @p@ does not carry a+    run-time space or time cost.+-}+newtype Satisfies (p :: * -> *) a = Satisfies a+instance The (Satisfies p a) a++-- | An infix alias for 'Satisfies'.+type a ?p = Satisfies p a+infixr 1 ?++-- | For library authors: assert that a property holds.+assert :: Defining (p n) => a -> (a ?p)+assert x = name x (\x -> unname (x ...axiom))++-- | Existential introduction for names: given a named value of+--   type @a@ that satisfies a predicate @p@, coerce to a value+--   of type @a ?p@.+unname :: (a ~~ name ::: p name) -> (a ?p)+unname = coerce . the++-- | Existential elimination for names: given a value of type+--   @a ?p@, re-introduce a new name to produce a value of type+--   @a ~~ name ::: p name@.+rename :: (a ?p) -> (forall name. (a ~~ name ::: p name) -> t) -> t+rename x k = name (the x) (\x -> k (x ...axiom))++{-| Take a simple function with one named argument and a named return,+    plus an implication relating a precondition to a postcondition of the+    function, and produce a function between refined input and output types.++@+newtype NonEmpty xs = NonEmpty Defn+newtype Reverse  xs = Reverse  Defn++rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)+rev xs = defn (reverse (the xs))++rev_nonempty_lemma :: NonEmpty xs -> Proof (NonEmpty (Reverse xs))++rev' :: ([a] ?NonEmpty) -> ([a] ?NonEmpty)+rev' = rev ...? rev_nonempty_lemma+@+-}++(...?) :: (forall name. (a ~~ name) -> (b ~~ f name))+      -> (forall name. p name -> Proof (q (f name)))+      -> (a ?p) -> (b ?q)+(...?) f _ x = rename x (\x -> unname (f (exorcise x) ...axiom))++-- | Traverse a collection of refined values, re-introducing names+--   in the body of the action.+traverseP :: (Traversable t, Applicative f)+          => (forall name. (a ~~ name ::: p name) -> f b)+          -> t (a ?p)+          -> f (t b)+traverseP f = traverse (\x -> rename x f)++-- | Same as 'traverseP', but ignores the action's return value.+traverseP_ :: (Foldable t, Applicative f)+          => (forall name. (a ~~ name ::: p name) -> f b)+          -> t (a ?p)+          -> f ()+traverseP_ f = traverse_ (\x -> rename x f)++-- | Same as 'traverse', with the argument order flipped.+forP :: (Traversable t, Applicative f)+      => t (a ?p)+      -> (forall name. (a ~~ name ::: p name) -> f b)+      -> f (t b)+forP x f = traverseP f x++-- | Same as 'traverse_', with the argument order flipped.+forP_ :: (Foldable t, Applicative f)+      => t (a ?p)+      -> (forall name. (a ~~ name ::: p name) -> f b)+      -> f ()+forP_ x f = traverseP_ f x
+ src/Data/The.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE DefaultSignatures      #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PatternSynonyms        #-}+{-# LANGUAGE ViewPatterns           #-}++{-|+  Module      :  Data.The+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Data.The+  ( The(..)+  , pattern The+  ) where++import Data.Coerce++{-| A class for extracing "the" underlying value.+    'the' should ideally be a coercion from some+    @newtype@ wrap of @a@ back to @a@.+ +    For this common use case, in the module where+    @newtype New a = New a@ is defined, an instance+    of @The@ can be created with an empty definition:++@+newtype New a = New a+instance The (New a) a+@+-}+class The d a | d -> a where+  the :: d -> a+  default the :: Coercible d a => d -> a+  the = coerce++{-| A view pattern for discarding the wrapper around+    a value.++@+f (The x) = expression x+@++    is equivalent to++@+f x = let x' = the x in expression x'+@+-}+pattern The :: The d a => a -> d+pattern The x <- (the -> x)
+ src/GDP.hs view
@@ -0,0 +1,29 @@+{-|+  Module      :  GDP+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module GDP+  ( module Data.Arguments+  , module Data.Refined+  , module Data.The+  , module Logic.Classes+  , module Logic.NegClasses+  , module Logic.Proof+  , module Logic.Propositional+  , module Theory.Equality+  , module Theory.Named+  ) where++import Data.Arguments+import Data.Refined+import Data.The+import Logic.Classes+import Logic.NegClasses+import Logic.Proof+import Logic.Propositional+import Theory.Equality+import Theory.Named
+ src/Logic/Classes.hs view
@@ -0,0 +1,229 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts      #-}++{-|+  Module      :  Logic.Classes+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Logic.Classes+  ( -- * Algebraic properties+    Reflexive(..)+  , Symmetric(..)+  , Transitive(..)+  , transitive'++  , Idempotent(..)+  , Commutative(..)+  , Associative(..)+  , DistributiveL(..)+  , DistributiveR(..)++  , Injective(..)++  ) where++import Logic.Proof+import Theory.Equality+import Theory.Named++{--------------------------------------------------------+  Special properties of predicates and functions+--------------------------------------------------------}++{-| A binary relation R is /reflexive/ if, for all x,+    R(x, x) is true. The @Reflexive r@ typeclass provides+    a single method, @refl :: Proof (r x x)@,+    proving R(x, x) for an arbitrary x.++    Within the module where the relation @R@ is defined, you can+    declare @R@ to be reflexive with an empty instance:++@+-- Define a reflexive binary relation+newtype SameColor p q = SameColor Defn+instance Reflexive SameColor+@+-}   +class Reflexive r where+  refl :: Proof (r x x)+  default refl :: (Defining (r x x)) => Proof (r x x)+  refl = axiom++{-| A binary relation R is /symmetric/ if, for all x and y,+    R(x, y) is true if and only if R(y, x) is true. The+    @Symmetric@ typeclass provides+    a single method, @symmetric :: r x y -> Proof (r y x)@,+    proving the implication "R(x, y) implies R(y, x)".++    Within the module where @R@ is defined, you can+    declare @R@ to be symmetric with an empty instance:++@+-- Define a symmetric binary relation+newtype NextTo p q = NextTo Defn+instance Symmetric NextTo+@+-}   +class Symmetric c where+  symmetric :: c p q -> Proof (c q p)+  default symmetric :: (Defining (c p q)) => c p q -> Proof (c q p)+  symmetric _ = axiom++{-| A binary relation R is /transitive/ if, for all x, y, z,+    if R(x, y) is true and R(y, z) is true, then  R(x, z) is true.+    The @Transitive r@ typeclass provides+    a single method, @transitive :: r x y -> r y z -> Proof (r x z)@,+    proving R(x, z) from R(x, y) and R(y, z).++    Within the module where @R@ is defined, you can+    declare @R@ to be transitive with an empty instance:++@+-- Define a transitive binary relation+newtype CanReach p q = CanReach Defn+instance Transitive CanReach+@+-}   +class Transitive c where+  transitive :: c p q -> c q r -> Proof (c p r)+  default transitive :: Defining (c p q) => c p q -> c q r -> Proof (c p r)+  transitive _ _ = axiom++-- | @transitive@, with the arguments flipped.+transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)+transitive' = flip transitive++{-| A binary operation @#@ is idempotent if @x # x == x@ for all @x@.+    The @Idempotent c@ typeclass provides a single method,+    @idempotent :: Proof (c p p == p)@.++    Within the module where @F@ is defined, you can declare @F@ to be+    idempotent with an empty instance:++@+-- Define an idempotent binary operation+newtype Union x y = Union Defn+instance Idempotent Union+@+-}+class Idempotent c where+  idempotent :: Proof (c p p == p)+  default idempotent :: Defining (c p p) => Proof (c p p == p)+  idempotent = axiom+  +{-| A binary operation @#@ is commutative if @x # y == y # x@ for all @x@ and @y@.+    The @Commutative c@ typeclass provides a single method,+    @commutative :: Proof (c x y == c y x)@.++    Within the module where @F@ is defined, you can declare @F@ to be+    commutative with an empty instance:++@+-- Define a commutative binary operation+newtype Union x y = Union Defn+instance Commutative Union+@+-}+class Commutative c where+  commutative :: Proof (c p q == c q p)+  default commutative :: Defining (c p q) => Proof (c p q == c q p)+  commutative = axiom++{-| A binary operation @#@ is associative if @x # (y # z) == (x # y) # z@ for+    all @x@, @y@, and @z@.+    The @Associative c@ typeclass provides a single method,+    @associative :: Proof (c x (c y z) == c (c x y) z)@.++    Within the module where @F@ is defined, you can declare @F@ to be+    associative with an empty instance:++@+-- Define an associative binary operation+newtype Union x y = Union Defn+instance Associative Union+@+-}+class Associative c where+  associative :: Proof (c p (c q r) == c (c p q) r)+  default associative :: Defining (c p q) => Proof (c p (c q r) == c (c p q) r)+  associative = axiom++{-| A binary operation @#@ distributes over @%@ on the left if+    @x # (y % z) == (x # y) % (x # z)@ for+    all @x@, @y@, and @z@.+    The @DistributiveL c c'@ typeclass provides a single method,+    @distributiveL :: Proof (c x (c' y z) == c' (c x y) (c x z))@.++    Within the module where @F@ and @G@ are defined, you can declare @F@ to+    distribute over @G@ on the left with an empty instance:++@+-- x `Union` (y `Intersect` z) == (x `Union` y) `Intersect` (x `Union` z)+newtype Union     x y = Union     Defn+newtype Intersect x y = Intersect Defn+instance DistributiveL Union Intersect+@+-}+class DistributiveL c c' where+  distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))+  default distributiveL :: (Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))+  distributiveL = axiom++{-| A binary operation @#@ distributes over @%@ on the right if+    @(x % y) # z == (x # z) % (y # z)@ for+    all @x@, @y@, and @z@.+    The @DistributiveR c c'@ typeclass provides a single method,+    @distributiveR :: Proof (c (c' x y) z == c' (c x z) (c y z))@.++    Within the module where @F@ and @G@ are defined, you can declare @F@ to+    distribute over @G@ on the left with an empty instance:++@+-- (x `Intersect` y) `Union` z == (x `Union` z) `Intersect` (y `Union` z)+newtype Union     x y = Union     Defn+newtype Intersect x y = Intersect Defn+instance DistributiveR Union Intersect+@+-}+class DistributiveR c c' where+  distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))+  default distributiveR :: (Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))+  distributiveR = axiom++{-| A function @f@ is /injective/ if @f x == f y@ implies @x == y@.+    The @Injective f@ typeclass provides a single method,+    @elim_inj :: (f x == f y) -> Proof (x == y)@.++    Within the module where @F@ is defined, you can declare @F@ to be+    injective with an empty instance:++@+-- {x} == {y} implies x == y.+newtype Singleton x = Singleton Defn+instance Injective Singleton+@+-}+class Injective f where+  elim_inj :: (f x == f y) -> Proof (x == y)+  default elim_inj :: (Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)+  elim_inj _ = axiom+++{--------------------------------------------------------+  Properites of equality+--------------------------------------------------------}++instance Reflexive Equals where+  refl = axiom++instance Symmetric Equals where+  symmetric _ = axiom++instance Transitive Equals where+  transitive _ _ = axiom
+ src/Logic/NegClasses.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts      #-}++{-|+  Module      :  Logic.NegClasses+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Logic.NegClasses+  ( -- * Algebraic properties+    Irreflexive(..)+  , Antisymmetric(..)+  ) where++import Logic.Proof+import Logic.Propositional (Not)+import Theory.Equality+import Theory.Named++{--------------------------------------------------------+  Special properties of predicates and functions+--------------------------------------------------------}++{-| A binary relation R is /irreflexive/ if, for all x,+    R(x, x) is false. The @Irreflexive r@ typeclass provides+    a single method, @irrefl :: Proof (Not (r x x))@,+    proving the negation of R(x, x) for an arbitrary x.++    Within the module where the relation @R@ is defined, you can+    declare @R@ to be irreflexive with an empty instance:++@+-- Define an irreflexive binary relation+newtype DifferentColor p q = DifferentColor Defn+instance Irreflexive DifferentColor+@+-}+class Irreflexive r where+  irrefl :: Proof (Not (r x x))+  default irrefl :: (Defining (r x x)) => Proof (Not (r x x))+  irrefl = axiom+++{-| A binary relation R is /antisymmetric/ if, for all x and y,+    when R(x, y) is true, then R(y, x) is false. The+    @Antisymmetric@ typeclass provides+    a single method, @antisymmetric :: r x y -> Proof (Not (r y x))@,+    proving the implication "R(x, y) implies the negation of R(y, x)".++    Within the module where @R@ is defined, you can+    declare @R@ to be antisymmetric with an empty instance:++@+-- Define an antisymmetric binary relation+newtype AncestorOf p q = AncestorOf Defn+instance Antisymmetric AncestorOf+@+-}   +class Antisymmetric c where+  antisymmetric :: c p q -> Proof (Not (c q p))+  default antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))+  antisymmetric _ = axiom
+ src/Logic/Proof.hs view
@@ -0,0 +1,203 @@+{-# LANGUAGE KindSignatures #-}++{-|+  Module      :  Logic.Proof+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Logic.Proof+  ( -- * The `Proof` monad+    Proof+  , (|.), (|$), (|/), (|\), ($$)+  , given+  , axiom, sorry+  ) where++import Data.Coerce+import Control.Monad ((>=>))++{--------------------------------------------------+  The `Proof` monad+--------------------------------------------------}++{-| The @Proof@ monad is used as a domain-specific+    language for constructing proofs. A value of type+    @Proof p@ represents a proof of the proposition @p@.++    For example, this function constructions a proof of+    "P or Q" from the assumption "P and Q":++> and2or :: (p && q) -> Proof (p || q)+>+> and2or pq = do+>    p <- and_elimL pq    -- or: "p <- fst <$> and_elim pq"+>    or_introL p++    If the body of the proof does not match the proposition+    you claim to be proving, the compiler will raise a type+    error. Here, we accidentally try to use @or_introR@+    instead of @or_introL@:++> and2or :: (p && q) -> Proof (p || q)+>+> and2or pq = do+>    p <- and_elimL pq+>    or_introR p++resulting in the error++@+    • Couldn't match type ‘p’ with ‘q’+      ‘p’ is a rigid type variable bound by+        the type signature for:+          and2or :: forall p q. (p && q) -> Proof (p || q)++      ‘q’ is a rigid type variable bound by+        the type signature for:+          and2or :: forall p q. (p && q) -> Proof (p || q)++      Expected type: Proof (p || q)+        Actual type: Proof (p || p)+@+-}+data Proof (pf :: *) = QED++instance Functor Proof where+  fmap _ = const QED -- modus ponens (external?)++instance Applicative Proof where+  pure = const QED -- axiom+  pf1 <*> pf2 = QED -- modus ponens (internal?)++instance Monad Proof where+  pf >>= f = QED++{-| This operator is just a specialization of @(>>=)@, but+    can be used to create nicely delineated chains of+    derivations within a larger proof. The first statement+    in the chain should produce a formula; @(|$)@ then+    pipes this formula into the following derivation rule.++> and2or :: (p && q) -> Proof (p || q)+>+> and2or pq =  and_elimL pq+>           |$ or_introL+-}++(|$) :: Proof p -> (p -> Proof q) -> Proof q+(|$) = (>>=)++infixr 7 |$++--(|-) :: ((p -> Proof r) -> Proof r) -> (p -> Proof r) -> Proof r++{-| This operator is used to create nicely delineated chains of+    derivations within a larger proof. If X and Y are two+    deduction rules, each with a single premise and a single+    conclusion, and the premise of Y matches the conclusion of X,+    then @X |. Y@ represents the composition of the two+    deduction rules.++> and2or :: (p && q) -> Proof (p || q)+>+> and2or =  and_elimL+>        |. or_introL+-}++(|.) :: (p -> Proof q) -> (q -> Proof r) -> p -> Proof r+(|.) = (>=>)++infixr 9 |.++{-| The @(|/)@ operator is used to feed the remainder of the proof in+    as a premise of the first argument.++    A common use-case is with the @Or@-elimination rules @or_elimL@ and+    @or_elimR@, when one case is trivial. For example, suppose we wanted+    to prove that @R && (P or (Q and (Q implies P)))@ implies @P@:++@+my_proof :: r && (p || (q && (q --> p))) -> Proof p++my_proof =+  do  and_elimR          -- Forget the irrelevant r.+   |. or_elimL given     -- The first case of the || is immediate;+   |/ and_elim           -- The rest of the proof handles the second case,+   |. uncurry impl_elim  --   by unpacking the && and feeding the q into+                         --   the implication (q --> p).+@++    The rising @/@ is meant to suggest the bottom half of the proof getting+    plugged in to the Or-elimination line.+-}+(|/) :: (p -> (q -> Proof r) -> Proof r) -> (q -> Proof r) -> p -> Proof r+(|/) = flip+infixr 9 |/++{-| The @(|\\)@ operator is used to take the subproof so far and feed it+    into a rule that is expecting a subproof as a premise.++    A common use-case is with the @Not@-introduction rule @not_intro@,+    which has a type that fits the second argument of @(|\\)@. By way+    of example, here is a proof that "P implies Q" along with "Not Q"+    implies "Not P".++@+my_proof :: (p --> q) -> (Not p --> r) -> Not q -> Proof r++my_proof impl1 impl2 q' =+  do  modus_ponens impl1   -- This line, composed with the next,+   |. contradicts' q'      --   form a proof of FALSE from p.+   |\\ not_intro            -- Closing the subproof above, conclude not-p.+   |. modus_ponens impl2   -- Now apply the second implication to conclude r.+@++    The falling @\\@ is meant to suggest the upper half of the proof+    being closed off by the Not-introduction line.+-}+(|\) :: (p -> Proof q) -> ((p -> Proof q) -> Proof r) -> Proof r+(|\) = flip ($)+infixl 8 |\++-- | Take a proof of @p@ and feed it in as the first premise of+--   an argument that expects a @p@ and a @q@.+($$) :: (p -> q -> Proof r) -> Proof p -> (q -> Proof r)+(f $$ pp) q = do { p <- pp; f p q }++-- | @given@ creates a proof of P, given P as+--   an assumption.+--+--   @given@ is just a specialization of @pure@ / @return@.+given :: p -> Proof p+given _ = QED++-- | @sorry@ can be used to provide a "proof" of+--   any proposition, by simply assering it as+--   true. This is useful for stubbing out portions+--   of a proof as you work on it, but subverts+--   the entire proof system.+--+-- _Completed proofs should never use @sorry@!_+sorry :: Proof p+sorry = QED++{-| @axiom@, like @sorry@, provides a "proof" of any+    proposition. Unlike @sorry@, which is used to indicate+    that a proof is still in progress, @axiom@ is meant to+    be used by library authors to assert axioms about how+    their library works. For example:++@+data Reverse xs = Reverse Defn+data Length  xs = Length  Defn++rev_length_lemma :: Proof (Length (Reverse xs) == Length xs)+rev_length_lemma = axiom+@+-}+axiom :: Proof p+axiom = QED+
+ src/Logic/Propositional.hs view
@@ -0,0 +1,478 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE TypeFamilies #-}++{-|+  Module      :  Logic.Propositional+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Logic.Propositional+  ( -- * First-order Logic++  -- ** Logical symbols+    TRUE, FALSE+  +  , And,     type (&&), type (∧), type (/\)+  , Or,      type (||), type (∨), type (\/)+  , Implies, type (-->)+  , Not+  , ForAll+  , Exists++  -- ** Natural deduction++  -- *** Tautologies+  , true+  , noncontra++  -- *** Introduction rules++  -- | Introduction rules give the elementary building blocks+  --   for creating a formula from simpler ones.+  , and_intro+  , or_introL+  , or_introR+  , impl_intro+  , not_intro+  , contrapositive+  , contradicts+  , contradicts'+  , univ_intro+  , ex_intro++  -- *** Elimination rules++  -- | Elimination rules give the elementary building blocks for+  --   decomposing a complex formula into simpler ones.+  , and_elimL+  , and_elimR+  , and_elim+  , or_elim+  , or_elimL+  , or_elimR+  , impl_elim+  , modus_ponens+  , modus_tollens+  , absurd+  , univ_elim+  , ex_elim++  -- *** Classical logic and the Law of the Excluded Middle+  , Classical+  , classically+  , lem+  , contradiction+  , not_not_elim++   -- *** Mapping over conjunctions and disjunctions+  , and_mapL+  , and_mapR+  , and_map++  , or_mapL+  , or_mapR+  , or_map++  , impl_mapL+  , impl_mapR+  , impl_map++  , not_map++  ) where++import Data.Arguments+import Data.Refined+import Data.The+import Logic.Classes+import Logic.Proof+import Theory.Named++{--------------------------------------------------+  Logical constants+--------------------------------------------------}++-- | The constant "true".+newtype TRUE  = TRUE Defn++-- | The constant "false".+newtype FALSE = FALSE Defn++-- | The conjunction of @p@ and @q@.+newtype And p q = And Defn++-- | The disjunction of @p@ and @q@.+newtype Or p q  = Or  Defn++-- | The negation of @p@.+newtype Not p   = Not Defn++-- | The implication "@p@ implies @q@".+newtype Implies p q = Implies Defn++-- | Existential quantifiation.+newtype Exists x p = Exists Defn++-- | Universal quantification.+newtype ForAll x p = ForAll Defn++-- | An infix alias for @Or@.+type p || q   = p `Or` q++-- | An infix alias for @Or@.+type p ∨ q   = p `Or` q++-- | An infix alias for @Or@.+type p \/ q  = p `Or` q++-- | An infix alias for @And@.+type p && q  = p `And` q++-- | An infix alias for @And@.+type p ∧ q   = p `And` q++-- | An infix alias for @And@.+type p /\ q  = p `And` q++-- | An infix alias for @Implies@.+type p --> q = p `Implies` q++infixl 2 `Or`+infixl 2 ||+infixl 2 ∨+infixl 2 \/++infixl 3 `And`+infixl 3 &&+infixl 3 ∧+infixl 3 /\++infixr 1 `Implies`+infixr 1 -->++{--------------------------------------------------+  Mapping over conjunctions and disjunctions+--------------------------------------------------}++-- | Apply a derivation to the left side of a conjunction.+and_mapL :: (p -> Proof p') -> (p && q) -> Proof (p' && q)+and_mapL impl conj = do+  (lhs, rhs) <- and_elim conj+  lhs' <- impl lhs+  and_intro lhs' rhs++-- | Apply a derivation to the right side of a conjunction.+and_mapR :: (q -> Proof q') -> (p && q) -> Proof (p && q')+and_mapR impl conj = do+  (lhs, rhs) <- and_elim conj+  rhs' <- impl rhs+  and_intro lhs rhs'++-- | Apply derivations to the left and right sides of a conjunction.+and_map :: (p -> Proof p') -> (q -> Proof q') -> (p && q) -> Proof (p' && q')+and_map implP implQ conj = do+  (lhs, rhs) <- and_elim conj+  lhs' <- implP lhs+  rhs' <- implQ rhs+  and_intro lhs' rhs'++-- | Apply a derivation to the left side of a disjunction.+or_mapL :: (p -> Proof p') -> (p || q) -> Proof (p' || q)+or_mapL impl = or_elim (impl |. or_introL) or_introR++-- | Apply a derivation to the right side of a disjunction.+or_mapR :: (q -> Proof q') -> (p || q) -> Proof (p || q')+or_mapR impl = or_elim or_introL (impl |. or_introR)++-- | Apply derivations to the left and right sides of a disjunction.+or_map :: (p -> Proof p') -> (q -> Proof q') -> (p || q) -> Proof (p' || q')+or_map implP implQ = or_elim (implP |. or_introL) (implQ |. or_introR)++-- | Apply a derivation to the left side of an implication.+impl_mapL :: (p' -> Proof p) -> (p --> q) -> Proof (p' --> q)+impl_mapL derv impl = impl_intro (derv |. modus_ponens impl)++-- | Apply a derivation to the right side of an implication.+impl_mapR :: (q -> Proof q') -> (p --> q) -> Proof (p --> q')+impl_mapR derv impl = impl_intro (modus_ponens impl |. derv)++-- | Apply derivations to the left and right sides of an implication.+impl_map :: (p' -> Proof p) -> (q -> Proof q') -> (p --> q) -> Proof (p' --> q')+impl_map dervL dervR impl = impl_intro (dervL |. modus_ponens impl |. dervR)++-- | Apply a derivation inside of a negation.+not_map :: (p' -> Proof p) -> Not p -> Proof (Not p')+not_map impl notP = not_intro (impl |. contradicts' notP |. absurd)++{--------------------------------------------------+  Tautologies+--------------------------------------------------}++-- | @TRUE@ is always true, and can be introduced into a proof at any time.+true :: Proof TRUE+true = axiom++-- | The Law of Noncontradiction: for any proposition P, "P and not-P" is false.+noncontra :: Proof (Not (p && Not p))+noncontra = axiom++{--------------------------------------------------+  Introduction rules+--------------------------------------------------}++-- | Prove "P and Q" from P and Q.+and_intro :: p -> q -> Proof (p && q)+and_intro _ _ = axiom++-- | Prove "P and Q" from Q and P.+and_intro' :: q -> p -> Proof (p && q)+and_intro' _ _ = axiom++-- | Prove "P or Q" from  P.+or_introL :: p -> Proof (p || q)+or_introL _ = axiom++-- | Prove "P or Q" from Q.+or_introR :: q -> Proof (p || q)+or_introR _ = axiom++-- | Prove "P implies Q" by demonstrating that,+--   from the assumption P, you can prove Q.+impl_intro :: (p -> Proof q) -> Proof (p --> q)+impl_intro _ = axiom++-- | Prove "not P" by demonstrating that,+--   from the assumption P, you can derive a false conclusion.+not_intro :: (p -> Proof FALSE) -> Proof (Not p)+not_intro _ = axiom++-- | `contrapositive` is an alias for `not_intro`, with+--   a somewhat more suggestive name. Not-introduction+--   corresponds to the proof technique "proof by contrapositive".+contrapositive :: (p -> Proof FALSE) -> Proof (Not p)+contrapositive = not_intro++-- | Prove a contradiction from "P" and "not P".+contradicts :: p -> Not p -> Proof FALSE+contradicts _ _ = axiom++-- | `contradicts'` is `contradicts` with the arguments+--   flipped. It is useful when you want to partially+--   apply `contradicts` to a negation.+contradicts' :: Not p -> p -> Proof FALSE+contradicts' = flip contradicts++-- | Prove "For all x, P(x)" from a proof of P(*c*) with+--   *c* indeterminate.+univ_intro :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))+univ_intro _ = axiom++-- | Prove "There exists an x such that P(x)" from a specific+--   instance of P(c).+ex_intro :: p c -> Proof (Exists x (p x))+ex_intro _ = axiom++{--------------------------------------------------+  Elimination rules+--------------------------------------------------}++-- | From the assumption "P and Q", produce a proof of P.+and_elimL :: p && q -> Proof p+and_elimL _ = axiom++-- | From the assumption "P and Q", produce a proof of Q.+and_elimR :: p && q -> Proof q+and_elimR _ = axiom++-- | From the assumption "P and Q", produce both a proof+--   of P, and a proof of Q.+and_elim :: p && q -> Proof (p, q)+and_elim c = (,) <$> and_elimL c <*> and_elimR c+  +{-| If you have a proof of R from P, and a proof of+     R from Q, then convert "P or Q" into a proof of R.+-}+or_elim :: (p -> Proof r) -> (q -> Proof r) -> (p || q) -> Proof r+or_elim _ _ _ = axiom++{-| Eliminate the first alternative in a conjunction.+-}+or_elimL :: (p -> Proof r) -> (p || q) -> (q -> Proof r) -> Proof r+or_elimL case1 disj case2 = or_elim case1 case2 disj++{-| Eliminate the second alternative in a conjunction.+-}+or_elimR :: (q -> Proof r) -> (p || q) -> (p -> Proof r) -> Proof r+or_elimR case2 disj case1 = or_elim case1 case2 disj++-- | Given "P imples Q" and P, produce a proof of Q.+--   (modus ponens)+impl_elim :: p -> (p --> q) -> Proof q+impl_elim _ _ = axiom++-- | @modus_ponens@ is just @impl_elim@ with the arguments+--   flipped. In this form, it is useful for partially+--   applying an implication.+modus_ponens :: (p --> q) -> p -> Proof q+modus_ponens = flip impl_elim++{-| Modus tollens lets you prove "Not P" from+    "P implies Q" and "Not Q".++    Modus tollens is not fundamental, and can be derived from+    other rules:++@+                                  -----         (assumption)+                        p --> q,    p+                       ---------------------    (modus ponens)+                 q,           Not q    +              --------------------------        (contradicts')+                      FALSE+          ------------------------------------- (not-intro)+                             Not p+@++We can encode this proof tree more-or-less directly as a @Proof@+to implement @modus_tollens@:++@+modus_tollens :: (p --> q) -> Not q -> Proof (Not p)++modus_tollens impl q' =+  do  modus_ponens impl+   |. contradicts' q'+   |\\ not_intro+@+-}++modus_tollens :: (p --> q) -> Not q -> Proof (Not p)+modus_tollens impl q' =+  do  modus_ponens impl+   |. contradicts' q'+   |\ not_intro++-- | From a falsity, prove anything.+absurd :: FALSE -> Proof p+absurd _ = axiom++-- | Given "For all x, P(x)" and any c, prove the proposition+--   "P(c)".+univ_elim :: ForAll x (p x) -> Proof (p c)+univ_elim _ = axiom++-- | Given a proof of Q from P(c) with c generic, and the+--   statement "There exists an x such that P(x)", produce+--   a proof of Q.+ex_elim :: (forall c. p c -> Proof q) -> Exists x (p x) -> Proof q+ex_elim _ _ = axiom+++{--------------------------------------------------+  Classical logic+--------------------------------------------------}++-- | The inference rules so far have all been valid in+--   constructive logic. Proofs in classical logic are+--   also allowed, but will be constrained by the+--   `Classical` typeclass.+class Classical++-- | Discharge a @Classical@ constraint, by saying+--   "I am going to allow a classical argument here."+--+--   NOTE: The existence of this function means that a proof+--   should only be considered constructive if it+--   does not have a @Classical@ constraint, *and*+--   it does not invoke @classically@.+classically :: (Classical => Proof p) -> Proof p+classically _ = axiom++-- | The Law of the Excluded Middle: for any proposition+--   P, assert that either P is true, or Not P is true.+lem :: Classical => Proof (p || Not p)+lem = axiom++{-| Proof by contradiction: this proof technique allows+     you to prove P by showing that, from "Not P", you+     can prove a falsehood.+  +     Proof by contradiction is not a theorem of+     constructive logic, so it requires the @Classical@+     constraint. But note that the similar technique+     of proof by contrapositive (not-introduction) /is/+     valid in constructive logic! For comparison, the two types are:++@+contradiction  :: Classical => (Not p -> Proof FALSE) -> p+not_intro      ::              (p     -> Proof FALSE) -> Not p+@++The derivation of proof by contradiction from the law of the excluded+middle goes like this: first, use the law of the excluded middle to+prove @p || Not p@. Then use or-elimination to prove @p@ for each+alternative. The first alternative is immediate; for the second+alternative, use the provided implication to get a proof of falsehood,+from which the desired conclusion is derived.++@+contradiction impl =+  do  lem             -- introduce p || Not p+   |$ or_elimL given  -- dispatch the first, straightforward case+   |/ impl            -- Now we're on the second case. Apply the implication..+   |. absurd          -- .. and, from falsity, conclude p.+@+-}+contradiction :: forall p. Classical => (Not p -> Proof FALSE) -> Proof p+contradiction impl =+  do  lem+   |$ or_elimL given+   |/ impl+   |. absurd+  +{-| Double-negation elimination. This is another non-constructive+    proof technique, so it requires the @Classical@ constraint.++    The derivation of double-negation elimination follows from+    proof by contradiction, since "Not (Not p)" contradicts "Not p".+@+not_not_elim p'' = contradiction (contradicts' p'')+@+-}++not_not_elim :: Classical => Not (Not p) -> Proof p+not_not_elim p'' = contradiction (contradicts' p'')++{--------------------------------------------------+  Algebraic properties+--------------------------------------------------}++instance Symmetric And+instance Symmetric Or++instance Associative And+instance Associative Or++instance DistributiveR And And+instance DistributiveR And Or+instance DistributiveR Or  And+instance DistributiveR Or  Or++instance DistributiveL And And+instance DistributiveL And Or+instance DistributiveL Or  And+instance DistributiveL Or  Or+
+ src/Theory/Equality.hs view
@@ -0,0 +1,136 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE FlexibleContexts      #-}++{-|+  Module      :  Theory.Equality+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Theory.Equality+  (+    Equals, type (==)++  -- ** Substitutions and equational reasoning+  , (==.)+  , apply+  , substitute+  , substituteL+  , substituteR++  -- ** Relating to other forms of equality+  , same+  , reflectEq+  , propEq+  ) where++import Data.Arguments+import Data.The+import Theory.Named+import Logic.Proof (Proof, axiom)++import Lawful++import Unsafe.Coerce+import Data.Type.Equality ((:~:)(..))++{--------------------------------------------------+  Theory of equality+--------------------------------------------------}++-- | The @Equals@ relation is used to express equality between two entities.+--   Given an equality, you are then able to substitute one side of the equality+--   for the other, anywhere you please.+newtype Equals x y = Equals Defn++-- | An infix alias for 'Equals'.+type x == y = x `Equals` y+infix 4 ==++instance Argument (Equals x y) 0 where+  type GetArg (Equals x y) 0    = x+  type SetArg (Equals x y) 0 x' = Equals x' y++instance Argument (Equals x y) 1 where+  type GetArg (Equals x y) 1    = y+  type SetArg (Equals x y) 1 y' = Equals x y'++instance Argument (Equals x y) LHS where+  type GetArg (Equals x y) LHS    = x+  type SetArg (Equals x y) LHS x' = Equals x' y++instance Argument (Equals x y) RHS where+  type GetArg (Equals x y) RHS    = y+  type SetArg (Equals x y) RHS y' = Equals x y'++-- | Chain equalities, a la Liquid Haskell.+(==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)+_ ==. _ = axiom++-- | Apply a function to both sides of an equality.+apply :: forall f n x x'. (Argument f n, GetArg f n ~ x)+    => Arg n -> (x == x') -> Proof (f == SetArg f n x')+apply _ _ = axiom++-- | Given a formula and an equality over ones of its arguments,+--   replace the left-hand side of the equality with the right-hand side.+substitute :: (Argument f n, GetArg f n ~ x)+    => Arg n -> (x == x') -> f -> Proof (SetArg f n x')+substitute _ _ _ = axiom++-- | Substitute @x'@ for @x@ under the function @f@, on the left-hand side+--   of an equality.+substituteL :: (Argument f n, GetArg f n ~ x)+    => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g)+substituteL _ _ _ = axiom++-- | Substitute @x'@ for @x@ under the function @f@, on the right-hand side+--   of an equality.+substituteR :: (Argument f n, GetArg f n ~ x)+    => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x')+substituteR _ _ _ = axiom++{--------------------------------------------------+  Theory of equality+--------------------------------------------------}++-- | Test if the two name arguments are equal an, if so, produce a proof+--   of equality for the names.+same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))+same (The x) (The y) = if x == y then Just axiom else Nothing++{-| Reflect an equality between @x@ and @y@ into a propositional+    equality between the /types/ @x@ and @y@.++@+newtype Bob = Bob Defn++bob :: Int ~~ Bob+bob = defn 42++needsBob :: (Int ~~ Bob) -> Int+needsBob x = the x + the x++isBob :: (Int ~~ name) -> Maybe (Proof (name == Bob))+isBob = same x bob++f :: (Int ~~ name) -> Int+f x = case reflectEq \<$\> isBob x of+  Nothing   -> 17+  Just Refl -> needsBob x x+@+-}+reflectEq :: Proof (x == y) -> (x :~: y)+reflectEq _ = unsafeCoerce (Refl :: a :~: a)++-- | Convert a propositional equality between the types @x@ and @y@+--   into a proof of @x == y@.+propEq :: (x :~: y) -> Proof (x == y)+propEq _ = axiom
+ src/Theory/Named.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}++{-|+  Module      :  Theory.Named+  Copyright   :  (c) Matt Noonan 2018+  License     :  BSD-style+  Maintainer  :  matt.noonan@gmail.com+  Portability :  portable+-}++module Theory.Named+  ( -- * Named values+    Named, type (~~)+  , name+  , name2, name3++  -- ** Definitions+  , Defining+  , Defn+  , defn+  ) where++import Data.The+import Data.Coerce++{--------------------------------------------------+  Named values+--------------------------------------------------}++-- | A value of type @a ~~ name@ has the same runtime+--   representation as a value of type @a@, with a+--   phantom "name" attached.+newtype Named name a = Named a++-- | An infix alias for 'Named'.+type a ~~ name = Named name a++instance The (Named name a) a++-- | Introduce a name for the argument, and pass the+--   named argument into the given function.+name :: a -> (forall name. a ~~ name -> t) -> t+name x k = k (coerce x)++-- | Same as 'name', but names two values at once.+name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t+name2 x y k = k (coerce x) (coerce y)++-- | Same as 'name', but names three values at once.+name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t+name3 x y z k = k (coerce x) (coerce y) (coerce z)+++{--------------------------------------------------+  Definitions+--------------------------------------------------}++{-| Library authors can introduce new names in a controlled way+    by creating @newtype@ wrappers of @Defn@. The constructor of+    the @newtype@ should *not* be exported, so that the library+    can retain control of how the name is introduced.++@+newtype Bob = Bob Defn++bob :: Int ~~ Bob+bob = defn 42+@+-}+data Defn = Defn++-- | The @Defining P@ constraint holds in any module where @P@+--   has been defined as a @newtype@ wrapper of @Defn@. It+--   holds /only/ in that module, if the constructor of @P@+--   is not exported.+type Defining p = (Coercible p Defn, Coercible Defn p)++-- | In the module where the name @f@ is defined, attach the+--   name @f@ to a value.+defn :: Defining f => a -> (a ~~ f)+defn = coerce