type-settheory (empty) → 0.1
raw patch · 13 files changed
+2332/−0 lines, 13 filesdep +basedep +category-extrasdep +containerssetup-changed
Dependencies added: base, category-extras, containers, mtl, syb, template-haskell, type-equality
Files
- Control/SMonad.hs +196/−0
- Data/Category.hs +100/−0
- Data/Typeable/Extras.hs +47/−0
- Helper.hs +51/−0
- LICENSE +10/−0
- Setup.lhs +3/−0
- Type/Dummies.hs +83/−0
- Type/Function.hs +934/−0
- Type/Logic.hs +189/−0
- Type/Set.hs +541/−0
- Type/Set/Example.hs +76/−0
- Type/defs.h.hs +56/−0
- type-settheory.cabal +46/−0
+ Control/SMonad.hs view
@@ -0,0 +1,196 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Type.SMonad+--Author : Daniel Schüssler+--License : BSD3+--Copyright : Daniel Schüssler+--+--Maintainer : Daniel Schüssler+--Stability : Experimental+--Portability : Uses various GHC extensions+--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+++++{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}++-- | Example application of sets+--+-- This is quite similar to what the /rmonad/ package does, but we use preexisting sets rather than an associated datatype+--+-- * The apostrophed variants take proof objects as arguments+--+-- * The plain variants use 'auto'; that is, they assume that membership has been proved by an instance of 'Fact'+--+module Control.SMonad where+ +import Type.Set+import Type.Logic+import Data.Set as Set+ +++class SFunctor dom f | f -> dom where+ sfmap' :: x :∈: dom ->+ y :∈: dom ->+ (x -> y) -> f x -> f y++class SFunctor dom f => SApplicative dom f | f -> dom where+ spure' :: x :∈: dom ->+ x -> f x++ sap' :: x :∈: dom ->+ y :∈: dom ->+ (x -> y) :∈: dom -> + + f (x -> y) -> f x -> f y++class SApplicative dom m => SMonad dom m | m -> dom where+ sbind' :: x :∈: dom ->+ y :∈: dom ->+ m x -> (x -> m y) -> m y+ +-- * Variants using auto for the domain-membership proofs++sfmap :: ( SFunctor dom f+ , Fact (x :∈: dom)+ , Fact (y :∈: dom) )+ =>+ (x -> y) -> f x -> f y+sfmap = sfmap' auto auto++spure :: ( SApplicative dom f+ , Fact (x :∈: dom) )+ + =>+ x -> f x+spure = spure' auto++sap :: ( SApplicative dom f+ , Fact (x :∈: dom)+ , Fact (y :∈: dom)+ , Fact ((x -> y) :∈: dom) )+ + =>+ f (x->y) -> f x -> f y+sap = sap' auto auto auto+++sreturn' :: (SMonad dom f) => (x :∈: dom) -> x -> f x+sreturn' = spure'+ ++sreturn :: (SMonad dom f, Fact (x :∈: dom)) => x -> f x+sreturn = spure++sbind+ :: (Fact (x :∈: dom), Fact (y :∈: dom), SMonad dom m) =>+ m x -> (x -> m y) -> m y+sbind = sbind' auto auto+ +-- * Derived combinators++sjoin'+ :: (SMonad dom m) => (m y :∈: dom) -> (y :∈: dom) -> m (m y) -> m y+sjoin' p1 p2 y = sbind' p1 p2 y id+++sjoin+ :: (Fact (m y :∈: dom), Fact (y :∈: dom), SMonad dom m) =>+ m (m y) -> m y+sjoin y = sbind y id++-- | 'sfmap'' in terms of 'spure'' and 'sbind''+sfmap'Default+ :: (SMonad dom m) =>+ (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> m x -> m y+sfmap'Default px py f x = sbind' px py x (\x0 -> sreturn' py (f x0))+ +-- | 'sap'' in terms of 'spure'' and 'sbind''+sap'Default+ :: (SMonad dom m) =>+ (x :∈: dom)+ -> (y :∈: dom)+ -> ((x -> y) :∈: dom)+ -> m (x -> y)+ -> m x+ -> m y+sap'Default px py pxy f x = sbind' pxy py f+ (\f0 -> sbind' px py x (\x0 -> sreturn' py (f0 x0)))+++++sliftA2'+ :: (SApplicative dom f) =>+ (x :∈: dom)+ -> (y :∈: dom)+ -> (z :∈: dom)+ -> ((y -> z) :∈: dom)+ -> (x -> y -> z)+ -> f x+ -> f y+ -> f z+sliftA2' px py pz pyz f x y = ++ sap' py pz pyz+ (sfmap' px pyz f x)+ y++++sliftA2+ :: (Fact ((x1 -> y) :∈: dom),+ Fact (y :∈: dom),+ Fact (x1 :∈: dom),+ SApplicative dom f,+ Fact (x :∈: dom)) =>+ (x -> x1 -> y) -> f x -> f x1 -> f y+sliftA2 f x y = sfmap f x `sap` y+++ssequence'+ :: (SApplicative dom f) =>+ (a :∈: dom)+ -> ([a] :∈: dom)+ -> (([a] -> [a]) :∈: dom)+ + -> [f a]+ -> f [a]++ssequence' px pxs pxsxs = go+ where+ go [] = spure' pxs []+ go (x:xs) = sliftA2' px pxs pxs pxsxs (:) x (go xs)+++ssequence+ :: (Fact (a :∈: dom),+ Fact ([a] :∈: dom),+ Fact (([a] -> [a]) :∈: dom),+ SApplicative dom f) =>+ [f a] -> f [a]+ssequence = ssequence' auto auto auto++++++instance SFunctor OrdType Set where+ sfmap' OrdType OrdType = Set.map++instance SApplicative OrdType Set where+ spure' OrdType = singleton+ sap' = sap'Default++instance SMonad OrdType Set where+ sbind' OrdType OrdType xs f = Set.fold (\x r -> Set.union (f x) r) Set.empty xs
+ Data/Category.hs view
@@ -0,0 +1,100 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Data.Category+--Author : Daniel Schüssler+--License : BSD3+--Copyright : Daniel Schüssler+--+--Maintainer : Daniel Schüssler+--Stability : Experimental+--Portability : Uses various GHC extensions+--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------++++{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}++-- | This module is a stub!+module Data.Category where++import Type.Set+import Type.Dummies+import Type.Function+import Type.Logic+import Data.Type.Equality+import Control.Monad+ ++-- | Category with type-level set of objects and type-level /hom/ function, but value-level composition and value-level definition of identity functions.+data Cat ob hom =+ Cat {+ homIsFun :: ((ob :×: ob) :~>: Univ) hom+ , getId :: forall a aa. ((a,a), aa) :∈: hom -> aa+ -- | Composition+ , cc :: forall a b c bc ab ac. + ((b,c), bc) :∈: hom ->+ ((a,b), ab) :∈: hom ->+ ((a,c), ac) :∈: hom ->++ bc -> ab -> ac+ }+ +hask :: Cat Univ HaskFun+hask = Cat (extendCod haskFunIsFun auto)+ (\HaskFun -> id)+ (\HaskFun HaskFun HaskFun -> (.))+ +kleisli :: Monad m => Cat Univ (KleisliHom m)+kleisli = Cat (extendCod kleisliHomIsFun auto)+ (\KleisliHom -> return)+ (\KleisliHom KleisliHom KleisliHom -> (<=<))++idEx :: Cat ob hom -> ob a -> (forall aa. ((a,a),aa) :∈: hom -> aa -> r) -> r+idEx cat a k = case total (homIsFun cat) (a :×: a) of+ ExSnd faa -> k faa (getId cat faa)+ +-- idAuto :: forall ob hom a aa. Fact (((a, a), aa) :∈: hom) => Cat ob hom -> aa+-- -- idAuto cat _ = idn cat auto+-- idAuto cat _ = case total (homIsFun cat) ++idAuto :: forall a aa hom ob. (Fact (((a, a), aa) :∈: hom)) => Cat ob hom -> aa+idAuto cat = getId cat (auto :: ((a,a),aa) :∈: hom)+ +-- ccAuto :: forall a b c bc ab ac hom ob.+-- (Fact (((b, c), bc) :∈: hom),+-- Fact (((a, b), ab) :∈: hom),+-- Fact (((a, c), ac) :∈: hom)) =>+-- Cat ob hom -> bc -> ab -> ac+ccAuto cat = cc cat auto auto auto++test :: a -> a+test = idAuto hask+++test2 :: (b -> c) -> (a -> b) -> a -> c+test2 = ccAuto hask+ ++test3 :: forall m a. Monad m => a -> m a+test3 = idAuto kleisli+ +-- foo :: forall a. a -> a+-- foo = idEx hask (Univ :: Univ a) go+-- where+-- go :: (((a, a), aa) :∈: HaskFun) -> aa -> (a -> a)+-- go HaskFun x = x++ +-- data Functor omap
+ Data/Typeable/Extras.hs view
@@ -0,0 +1,47 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Data.Typeable.Extras+--Author : Daniel Schüssler+--License : BSD3+--Copyright : Daniel Schüssler+--+--Maintainer : Daniel Schüssler+--Stability : Experimental+--Portability : Uses various GHC extensions+--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+++++module Data.Typeable.Extras where++import Control.Monad+import Data.Typeable+import System.IO.Unsafe -- this is just for the missing Ord instance for Data.Typeable.TypeRep +import Data.Monoid+import Data.Function+import Control.Exception++dynEq :: (Typeable a, Typeable b, Eq b) => a -> b -> Bool+dynEq a b = case cast a of+ Just b' -> b' == b+ Nothing -> False++instance Ord TypeRep where+ compare x y = -- compare the string representations first+ ((compare `on` show) x y)+ `mappend`+ -- not sure why 'typeRepKey' is in IO+ (unsafePerformIO (liftM2 compare + (typeRepKey x) + (typeRepKey y)))++dynCompare :: (Typeable b, Typeable a, Ord b) => a -> b -> Ordering+dynCompare a b = case cast a of+ Just b' -> compare b' b+ Nothing -> let r = compare (typeOf a) (typeOf b)+ in assert (r/=EQ) r
+ Helper.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS -fno-warn-overlapping-patterns #-}+module Helper where+ ++import Language.Haskell.TH+import Control.Monad+import Data.Generics+ +decomposeForallT :: Type -> ([Type],Type)+decomposeForallT (ForallT _ cxt t) = case decomposeForallT t of+ (x,y) -> (cxt++x,y)+decomposeForallT t = ([],t)+++lemma :: Name -> Name -> Q [Dec]+lemma cls prf = do+ prfInfo <- reify prf++ let+ typ = case prfInfo of+ VarI _ typ _ _ -> unmangleNames typ+ _ -> error ("expected ValI, got "++show prfInfo)++ info <- reify cls+ let methodId = case info of+ ClassI (ClassD _ _ _ _ [SigD x _]) -> x+ _ -> error ("expected ClassI, got "++show info)+ + (cxt,bodyT) = decomposeForallT typ++ -- sig <- sigD prfId (return typ)+ + inst <- instanceD (return cxt) + (conT cls `appT` return bodyT) [valD (varP methodId)+ (normalB (varE prf))+ []+ ]+ + return [inst]+++unmangleName :: Name -> Name+unmangleName = mkName . fst . break (=='[') . nameBase++unmangleNames :: (Data a) => a -> a+unmangleNames = everywhere (mkT unmangleName)++lemmata :: Name -> [Name] -> Q [Dec]+lemmata cls xs = fmap concat (mapM (lemma cls) xs)
+ LICENSE view
@@ -0,0 +1,10 @@+Copyright (c) 2009, Daniel Schüssler+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 the <ORGANIZATION> nor the names of its 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 HOLDER 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.
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain
+ Type/Dummies.hs view
@@ -0,0 +1,83 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Type.Dummies+--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 GADTs #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies #-}++module Type.Dummies where+ +#include "defs.h.hs"+ +-- | \"Kind-cast\" @ SET @ to @*@+data Lower (a :: SET)+ +-- | \"Kind-cast\" @ SET1 @ to @ SET @. Also lower elements using 'Lower'.+data Lower1 (a :: SET1) :: SET where+ LowerElement :: u x -> Lower1 u (Lower x)+ +-- | \"Kind-cast\" @ SET2 @ to @ SET1 @. Also lower elements using 'Lower1'.+data Lower2 (a :: SET2) :: SET1 where+ Lower1Element :: u x -> Lower2 u (Lower1 x)+ +-- | \"Kind-cast\" @ SET3 @ to @ SET2 @. Also lower elements using 'Lower2'.+data Lower3 (a :: SET3) :: SET2 where+ Lower2Element :: u x -> Lower3 u (Lower2 x)++-- | Pair of types of kind @ SET @+data PAIR (a :: SET) (b :: SET) x+-- | Pair of types of kind @ SET1 @+data PAIR1 (a :: SET1) (b :: SET1) (x :: SET) +-- | Pair of types of kind @ SET2 @+data PAIR2 (a :: SET2) (b :: SET2) (x :: SET1)+-- | Pair of types of kind @ SET3 @+data PAIR3 (a :: SET3) (b :: SET3) (x :: SET2)+ +++-- data ΣPair (a :: SET) (b :: *)+ +-- type DependentPair = ΣPair++-- type Curry f a b = f (a,b)+ +-- type family Uncurry (f :: * -> * -> *) (ab :: *) :: *+-- type instance Uncurry g (a,b) = g a b+++-- type Curry2 f a b = f (Pair2 a b)+ +-- type family Uncurry2 (g :: SET -> SET -> *) (ab :: SET) :: *+-- type instance Uncurry2 g (Pair2 a b) = g a b++ +-- type Curry3 f a b = f (Pair3 a b)+ +-- type family Uncurry3 (g :: SET1 -> SET1 -> *) (ab :: SET1) :: *+-- type instance Uncurry3 g (Pair3 a b) = g a b++ +-- type Curry4 f a b = f (Pair4 a b)+ +-- type family Uncurry4 (g :: SET2 -> SET2 -> *) (ab :: SET2) :: *+-- type instance Uncurry4 g (Pair4 a b) = g a b
+ Type/Function.hs view
@@ -0,0 +1,934 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Type.Function+--Author : Daniel Schüssler+--License : BSD3+--Copyright : Daniel Schüssler+--+--Maintainer : Daniel Schüssler+--Stability : Experimental+--Portability : Uses various GHC extensions+--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------++{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE IncoherentInstances #-}++++-- | Notes+--+-- * Functions are coded as functional relations (in particular, functions are sets)+--+-- * Extensional equality of functions coincedes with extensional equality of sets.+module Type.Function where+ +import Type.Logic+import Type.Set+import Data.Type.Equality+import Control.Functor.Combinators.Flip+import Control.Arrow+import Helper+import Type.Dummies++ ++#include "defs.h.hs"++ +-- * Preliminary+ + +-- | Existential quantification over the first component of a pair+data ExSnd (f :: SET) (a :: *) :: * where+ ExSnd :: (a, ex) :∈: f -> ExSnd f a+ + +-- * Functions+ +-- | Functions are encoded as functional relations; the three arguments to the construcor are:+--+-- * Is a relation+--+-- * Totality+--+-- * Single-valuedness (CPS-encoded; using ':=:' would work just as well. I hope that the CPS variant makes the optimizer more happy, but this is pure speculation)+data ((dom :: SET) :~>: (cod :: SET)) :: SET1 where+ IsFun ::+ -- Is a relation+ (f :⊆: (dom :×: cod)) ++ -- Totality+ -> (forall (a :: *). a :∈: dom -> ExSnd f a) + + -- Single-valuedness (CPS)+ -> (forall a b1 b2 r.++ (a, b1) :∈: f -> + (a, b2) :∈: f -> + ((b1 ~ b2) => r) ->+ r)+ + -> (dom :~>: cod) f+ +infixr 6 :~>:, :~~>:++-- | Functions are relations+ +relation :: (dom :~>: cod) f -> f :⊆: (dom :×: cod)+relation (IsFun p _ _) = p+ ++-- | Functions are total+total :: (dom :~>: cod) f -> a :∈: dom -> ExSnd f a+total (IsFun _ p _) = p+ ++-- | /The detailed type variable names help debugging proofs/+totalCPS :: (dom :~>: cod) f -> a :∈: dom -> + (forall totalCPS_y. (a,totalCPS_y) :∈: f -> totalCPS_return) ->+ totalCPS_return+totalCPS f a k = case total f a of+ ExSnd fab -> k fab+++ +-- | Functions are single-valued (reified equality version)+sval :: forall dom cod a b1 b2 f.+ (dom :~>: cod) f ->+ (a, b1) :∈: f -> + (a, b2) :∈: f -> + b1 :=: b2+ +sval f fab1 fab2 = svalCPS f fab1 fab2 (Refl :: b1 ~ b2 => b1 :=: b2)+-- | Perform coercion using the single-valuedness+svalCoerce :: forall dom cod a b1 b2 f.+ (dom :~>: cod) f ->+ (a, b1) :∈: f -> + (a, b2) :∈: f -> + b1 -> b2+svalCoerce f p1 p2 x = svalCPS f p1 p2 (x :: b1 ~ b2 => b2)+ +-- | Functions are single-valued (CPS version)+svalCPS :: (dom :~>: cod) f ->+ (a, b1) :∈: f -> + (a, b2) :∈: f -> + + ((b1 ~ b2) => r) ->++ r+svalCPS (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 k + +svalCPS' :: (dom :~>: cod) f ->+ (a, b1) :∈: f -> + (a, b2) :∈: f -> + + (b1 :=: b2 -> r) ->++ r+svalCPS' (IsFun _ _ p) fab1 fab2 k = p fab1 fab2 (k Refl) + + +-- | Shortcut for unpacking 'relation'+rel :: (dom :~>: cod) f -> pair :∈: f -> pair :∈: (dom :×: cod)+rel f fp = relation f `scoerce` fp+ ++relCPS :: (dom :~>: cod) f -> pair :∈: f -> + (forall relCPS_x relCPS_y. (pair ~ (relCPS_x,relCPS_y)) => dom relCPS_x -> cod relCPS_y -> relCPS_return)+ -> relCPS_return+relCPS f fxy k = case rel f fxy of+ x :×: y -> k x y+ ++-- | If @f a = b@, then @a@ is in the domain of @f@+inDom :: (dom :~>: cod) f -> (a, b) :∈: f -> a :∈: dom+inDom f p = fstPrf (relation f `scoerce` p) ++-- | If @f a = b@, then @b@ is in the codomain of @f@+inCod :: (dom :~>: cod) f -> (a, b) :∈: f -> b :∈: cod+inCod f p = sndPrf (relation f `scoerce` p)+ +-- | The domain of a function is uniquely determined+domUniq :: (dom :~>: cod) f -> (dom2 :~>: cod) f -> dom :==: dom2+domUniq f f' = SetEq (domUniq0 f f') (domUniq0 f' f)+ where+ domUniq0 f f' = Subset (\a -> case total f a of+ ExSnd fa -> inDom f' fa)+ +-- ** Set of functions++-- | Kind-casted variant (function space as a set)+--+-- Convention: Instances of 'Fact' should always prove ':~>:' rather than this type.+type (dom :~~>: cod) = Lower1 (dom :~>: cod)++-- data ((dom :: SET) :~~>: (cod :: SET)) :: SET where+-- IsFun' :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f)+ +instance (Fact ((dom :~>: cod) f), Lower f ~ lf) => (Fact ((dom :~~>: cod) lf))+ where+ auto = LowerElement auto++lowerFun :: (dom :~>: cod) f -> (dom :~~>: cod) (Lower f)+lowerFun = LowerElement+ +raiseFun :: (dom :~~>: cod) (Lower f) -> (dom :~>: cod) f+raiseFun (LowerElement x) = x+ +-- | This is stronger than 'raiseFun' since it introduces the knowledge that @lf@ is of the form @Lower f@, rather than assuming it.+raiseFunCPS :: (dom :~~>: cod) lf -> + (forall f. (lf ~ Lower f) => (dom :~>: cod) f -> r) -> r+raiseFunCPS (LowerElement x) k = k x+ +-- * Images++-- | Image of a set under the function+data Image (f :: SET) (s :: SET) :: SET where+ Image :: a :∈: s -> + (a, b) :∈: f -> + Image f s b+ +-- | Every image is a subset of every possible codomain+imageCod :: (dom :~>: cod) f -> Image f s :⊆: cod+imageCod f = Subset (\(Image _ p) -> inCod f p)+ +-- | The full image is a codomain+setCodToImage :: (dom :~>: cod) f -> (dom :~>: Image f dom) f+setCodToImage f = adjustCod f subsetRefl+ + +-- | Change the codomain by proving that the full image is included in the new codomain+adjustCod :: (dom :~>: cod) f -> + (Image f dom :⊆: cod') + -> (dom :~>: cod') f+ +adjustCod f p = + IsFun (Subset (\fab -> case relation f `scoerce` fab of+ p1 :×: _ -> p1 :×: p `scoerce` + (Image p1 fab )))++ (total f) (\p1 p2 k -> svalCPS f p1 p2 k)+ ++-- | Enlargen the codomain+extendCod :: (dom :~>: cod) f -> + (cod :⊆: cod')+ -> (dom :~>: cod') f+ +extendCod f q = adjustCod f (Subset (\(Image _ fab) -> q `scoerce` inCod f fab))+ + +imageMonotonic :: (s1 :⊆: s2) -> Image f s1 :⊆: Image f s2 +imageMonotonic p = Subset( \(Image x fxy) -> Image (p `scoerce` x) fxy)+ +imageEmpty :: Image f Empty :==: Empty+imageEmpty = SetEq (Subset (\(Image (Empty e) _) -> Empty e)) emptySubset+ ++imageOfInclusion :: Image (Incl dom cod) s :==: (s :∩: dom)+imageOfInclusion = SetEq (Subset (\(Image s (Incl dom)) -> Inter s dom))+ (Subset (\(Inter s dom) -> Image s (Incl dom)))+ +fullImageOfInclusion :: dom :⊆: cod -> Image (Incl dom cod) dom :==: dom+fullImageOfInclusion s = imageOfInclusion `setEqTrans` interIdempotent++ +-- | Image distributes over union (in general not over intersection)+imageUnion :: forall dom cod s1 s2 f.+ (dom :~>: cod) f -> + + (Image f (s1 :∪: s2) )+ :==:+ (Image f s1 :∪: Image f s2)++imageUnion f = SetEq+ (Subset + (\(Image x fxy) -> case elimUnion x of+ Left x1 -> (Union . Left) (Image x1 fxy)+ Right x1 -> (Union . Right) (Image x1 fxy)))+ + (unionMinimal+ (imageMonotonic auto)+ (imageMonotonic auto)+ )+ + + +instance (cod' ~ cod'_copy, Fact ((dom :~>: cod) f)) => + Fact (+ (cod :⊆: cod'_copy)+ -> (dom :~>: cod') f+ )+ where+ auto x = extendCod auto x+ + + +-- -- | This is a helper type for bringing the knowledge into scope that if @f pair@, and @f@ is a function, then @pair@ must be a tuple+-- data Rel (dom,cod) f pair where+-- Rel :: dom a -> cod b -> Rel (dom,cod) f (PAIR a b)+ + + +-- * Equality++ +-- | Very useful lemma for proving equality of functions.+--+-- Given the properties of functions, it is enough to show that @f@ is a subset of @f'@ to prove @f = f'@.+funEq :: forall dom cod cod' f f'.+ (dom :~>: cod) f + -> (dom :~>: cod') f' + -> f :⊆: f' + -> f :==: f'++-- guardSameType :: a -> a -> b -> b+-- guardSameType _ _ = id++funEq f f' pSub = + SetEq pSub+ (Subset (\(f'ab :: ab :∈: f') -> + relCPS f' f'ab+ (\(a :: dom a) _ ->+ totalCPS f a (\ (fab' :: (a,b') :∈: f) ->+ case pSub `scoerce` fab' of+ (f'ab' :: (a,b') :∈: f') -> + svalCPS f' f'ab' f'ab + (fab' :: ab :∈: f))+ )))+ ++-- | 'funEq' with the inclusion argument flipped+funEq' ::+ (dom :~>: cod) f + -> (dom :~>: cod') f' + -> f' :⊆: f + -> f :==: f'++funEq' f f' pSub = setEqSym (funEq f' f pSub) + ++-- | Expresses the fact that /f = f' ==> f x = f' x/+equal_f :: (d :~>: c) f' -> + f :==: f' -> + (x,y) :∈: f -> + (x,y') :∈: f' -> + y :=: y'+equal_f f' eq fxy fxy' = sval f' (eq `ecoerce` fxy) fxy'+ +-- | Perform coercion using a function equality+equal_f_coerce :: (d :~>: c) f' -> + f :==: f' -> + (x,y) :∈: f -> + (x,y') :∈: f' -> + y -> y'+equal_f_coerce f' eq fxy fxy' = coerce (equal_f f' eq fxy fxy')++isFun_congruence :: (d :~>: c) f ->+ f :==: f' ->+ (d :~>: c) f'++isFun_congruence f eq = IsFun+ (Subset (\p -> rel f (eq `ecoerceFlip` p)))+ (\p -> totalCPS f p (\fxy -> ExSnd (eq `ecoerce` fxy)))+ (\p1 p2 k -> svalCPS f + (eq `ecoerceFlip` p1) + (eq `ecoerceFlip` p2)+ k)+++-- * Inclusion functions, identity, composition+ +-- | Inclusion function of a subset+--+-- Inclusions /do/ know their codomain (somewhat arbitrary design decision)+data Incl (dom :: SET) (cod :: SET) :: SET where+ Incl :: dom a -> Incl dom cod (a,a)+ + +-- inclCoerce :: (pair1 EQUAL pair2) ->+-- Incl dc pair1 ->+-- Incl dc pair2+-- inclCoerce + ++-- elimIncl :: pair ELEMENT Incl domcod -> +-- (forall a b dom cod r. ((PAIR0 a b) :∈: Incl domcod) -> r (PAIR0 a b))+-- -> r pair+ +-- | Identity function on @dom@+type Id dom = Incl dom dom++-- | Inclusion is a function+inclusionIsFun :: dom :⊆: cod -> (dom :~>: cod) (Incl dom cod)+inclusionIsFun q = IsFun+ (Subset (\(Incl p1) -> p1 :×: (q `scoerce` p1)))+ (\p -> ExSnd (Incl p))+ (\(Incl _) (Incl _) k -> k)+ ++instance (Fact (dom :⊆: cod))+ => Fact ((dom :~>: cod) (Incl dom cod))++ where+ auto = inclusionIsFun auto+++ +-- | Id is a function+idIsFun :: (dom :~>: dom) (Id dom)+idIsFun = inclusionIsFun subsetRefl+ ++-- | Composition+data ((g :: SET) :○: (f :: SET)) :: SET where+ Compo :: forall a b c. + (b, c) :∈: g -> + (a, b) :∈: f -> + (g :○: f) (a, c)+ +infixr 5 :○:+ + +-- | The composition is a function+compoIsFun :: (s2 :~>: s3) g -> + (s1 :~>: s2) f -> + (s1 :~>: s3) (g :○: f)+compoIsFun g f = + IsFun + (Subset (\(Compo gbc fab) -> case (rel g gbc, rel f fab) of+ ( _ :×: pc+ , pa :×: _ ) ->+ pa :×: pc))++ (\p -> case total f p of+ ExSnd fab ->+ case total g (inCod f fab) of+ ExSnd gbc -> + ExSnd (Compo gbc fab))++ (\(Compo gbc fab) (Compo gbc' fab') k -> svalCPS f fab fab'+ (svalCPS g gbc gbc' k)) + -- case sval f fab fab' of+ -- Refl -> case sval g gbc gbc' of+ -- Refl -> Refl)+ + +instance + ( Fact ( (s2 :~>: s3) g )+ , Fact ( (s1 :~>: s2) f ) + )++ =>+ Fact ((s1 :~>: s3) (g :○: f))+ + where+ auto = compoIsFun (auto :: (s2 :~>: s3) g) auto++-- | 'Id' is a left identity for composition +compo_idl :: (d :~>: c) f -> (Id c :○: f) :==: f+compo_idl f = funEq (compoIsFun idIsFun f) f+ (Subset (\(Compo (Incl y) fxy) -> fxy)) + +-- | 'Id' is a right identity for composition +compo_idr :: (d :~>: c) f -> (f :○: Id d) :==: f+compo_idr f = funEq (compoIsFun f idIsFun) f+ (Subset (\(Compo fxy (Incl x)) -> fxy)) ++ +-- * Equalisers++-- | Equalisers :D+--+-- In our category, the equaliser of two parallel functions @f1@ and @f2@ is the set of types on which @f1@ and @f2@ agree; that is:+--+-- /Equaliser f1 f2 = { x | f1 x = f2 x }/+data Equaliser (f1 :: SET) (f2 :: SET) :: SET where+ Equaliser :: (a, b) :∈: f1 -> (a, b) :∈: f2 -> Equaliser f1 f2 a+ +-- | Inclusion of the equaliser into the domain of the parallel functions+type EqualiserIncl s f1 f2 = Incl (Equaliser f1 f2) s+ + +-- | The equaliser is a subset of the domain of the parallel functions +equaliserSubset :: (s :~>: t) f1 + -> (Equaliser f1 f2) :⊆: s + +equaliserSubset f = Subset (\(Equaliser p _) -> inDom f p)+ ++++ +-- | The equaliser inclusion is a function+equaliserIsFun :: (s :~>: t) f1 + -> ((Equaliser f1 f2) :~>: s) + (EqualiserIncl s f1 f2)+ +equaliserIsFun f = inclusionIsFun (equaliserSubset f)+ + +-- The mediator is the same as the original function...++-- data EqualiserMed f1 f2 g :: (* -> * -> *) where+-- EqualiserMed :: Compo f1 g d a+-- -> Compo f2 g d a+-- -> EqualiserMed f1 f2 g d a++-- restrictDom :: IsFun (dom,cod) f -> (Subset dom' dom) -> IsFun dom' cod f+-- restrictDom (IsFun t s d c) (Subset p) = IsFun t s d (p . c)+++ +-- | Universal property of equalisers:+--+-- @f1 . g = f2 . g@ ==> @g@ factors uniquely through @Equaliser f1 f2@+--+-- Uniqueness is trivial in our case because the function into the equaliser is+-- identical to @g@ (our functions don't know their codomain)+equaliserUni :: (s0 :~>: s) g+ -> (s :~>: t) f1+ -> (f1 :○: g) :==: (f2 :○: g)+ -> (s0 :~>: (Equaliser f1 f2)) g ++equaliserUni g f1 pEq = ++ adjustCod g+ (Subset (\(Image _ gab) -> + case total f1 (inCod g gab) of+ ExSnd f1bc -> + case pEq `ecoerce` (Compo f1bc gab) of+ Compo f2b'c gab' ->+ case sval g gab gab' of+ Refl -> Equaliser f1bc f2b'c))+++-- * Injectivity++-- | Injective functions+--+-- (NB: Surjectivity is meaningless here because our functions don't know their codomain, but we have 'Image')+data Injective (f :: SET) :: * where+ Injective :: (forall a1 a2 b r.+ ( a1, b) :∈: f -> + ( a2, b) :∈: f -> + (a1 ~ a2 => r) ->+ r)+ + -> Injective f+ + +injective :: forall f a1 a2 b . + Injective f -> ((a1, b) :∈: f) -> ((a2, b) :∈: f) -> + a1 :=: a2+ +injective (Injective p) p1 p2 = p p1 p2 (Refl :: (a1 ~ a2) => a1 :=: a2)+ ++inclusion_Injective :: Injective (Incl dom cod)+inclusion_Injective = Injective (\(Incl _) (Incl _) k -> k) ++ +-- data Surjective (f :: SET) :: PROP where +-- Surjective :: (forall b. Image f b) -> Surjective f+ +++-- * Preimages++ +data Preimage (f :: SET) (s :: SET) :: SET where+ Preimage :: (a, b) :∈: f -> b :∈: s -> Preimage f s a+ + +preimage_Image :: + (dom :~>: cod) f ->+ set :⊆: dom -> + set :⊆: Preimage f (Image f set)+ +preimage_Image f s = Subset + (\x -> + let+ dom_x = s `scoerce` x+ in+ totalCPS f dom_x+ (\fxy -> Preimage fxy (Image x fxy)))++image_Preimage ::+ (dom :~>: cod) f ->+ Image f (Preimage f set) :⊆: set+ +image_Preimage f = Subset + (\(Image (Preimage fxy y) fxy') -> case sval f fxy fxy' of+ Refl -> y)+ ++-- * Binary product projections, target tupling++data Fst (s1 :: SET) (s2 :: SET) :: SET where + Fst :: a :∈: s1 -> b :∈: s2 -> Fst s1 s2 ((,) ((,) a b) a)+data Snd (s1 :: SET) (s2 :: SET) :: SET where + Snd :: a :∈: s1 -> b :∈: s2 -> Snd s1 s2 ((,) ((,) a b) b)+ +-- | Analogous to '***'+data ((f1 :: SET) :***: (f2 :: SET)) :: SET where+ (:***:) :: ((,) a b1) :∈: f1 -> + ((,) a b2) :∈: f2 -> + (f1 :***: f2) (a,((,) b1 b2))+ +infixr 3 :***:+ + +fstIsFun :: ((s1 :×: s2) :~>: s1) (Fst s1 s2)+fstIsFun = IsFun + (Subset (\(Fst p q) -> (p :×: q) :×: p))+ (\(p :×: q) -> ExSnd (Fst p q))+ (\(Fst _ _) (Fst _ _) k -> k)+ ++++ +sndIsFun :: ( (s1 :×: s2) :~>: s2) (Snd s1 s2)+sndIsFun = IsFun + (Subset (\(Snd p q) -> (p :×: q) :×: q))+ (\(p :×: q) -> ExSnd (Snd p q))+ (\(Snd _ _) (Snd _ _) k -> k)+ + ++ +targetTuplingIsFun :: (dom :~>: cod1) f1+ -> (dom :~>: cod2) f2 + -> (dom :~>: (cod1 :×: cod2)) (f1 :***: f2)+targetTuplingIsFun f1 f2 = IsFun+ (Subset (\(p1 :***: p2) -> inDom f1 p1+ :×:+ (inCod f1 p1 :×: inCod f2 p2)))++ (\p -> case (total f1 p , total f2 p) of + (ExSnd p1, ExSnd p2) -> ExSnd (p1 :***: p2))+ + (\(p1 :***: p2)+ (q1 :***: q2) k + -> svalCPS f1 p1 q1 + (svalCPS f2 p2 q2 k))+ ++instance (+ Fact ((dom :~>: cod1) f1)+ , Fact ((dom :~>: cod2) f2)+ )+ => Fact (+ (dom :~>: (cod1 :×: cod2)) + (f1 :***: f2)+ )+ + where+ auto = targetTuplingIsFun auto auto++-- * Particular functions+ +-- | The type-level function:+--+-- /HaskFun(a,b) = (a -> b)/+data HaskFun :: SET where+ HaskFun :: HaskFun ((,) ((,) a b) (a -> b))+ +instance (a_copy~a, b_copy~b) => Fact (((a_copy, b_copy), a -> b) :∈: HaskFun) where+ auto = HaskFun++haskFunIsFun :: ((Univ :×: Univ) :~>: FunctionType) HaskFun+haskFunIsFun = IsFun+ (Subset (\HaskFun -> ((Univ :×: Univ) :×: FunctionType)))+ (\(_ :×: _) -> ExSnd HaskFun)+ (\HaskFun HaskFun k -> k)++ +haskFunInjective :: Injective HaskFun+haskFunInjective = Injective (\HaskFun HaskFun k -> k)+ ++ +-- | The type-level function:+--+-- /KleisliHom(a,b) = (a -> m b)/+data KleisliHom (m :: * -> *) :: SET where+ KleisliHom :: KleisliHom m ((,) ((,) a b) (a -> m b))++kleisliHomIsFun :: ((Univ :×: Univ) :~>: (KleisliType m)) (KleisliHom m)+kleisliHomIsFun = IsFun+ (Subset (\KleisliHom -> ((Univ :×: Univ) :×: KleisliType)))+ (\(_ :×: _) -> ExSnd KleisliHom)+ (\KleisliHom KleisliHom k -> k)+ + +kleisliHomInjective :: Injective (KleisliHom m)+kleisliHomInjective = Injective (\KleisliHom KleisliHom k -> k)+ +instance (a1~a, b1~b, m1~m) => Fact (((a1, b1), a -> m1 b) :∈: KleisliHom m) where+ auto = KleisliHom+ +++-- * Conversions type constructors \<-\> type-level functions+ +-- | Graph of a @SET@ type constructor+data Graph f :: SET where+ Graph :: Graph f (a, (f a))+ +graphIsFun :: (Univ :~>: Univ) (Graph f)+graphIsFun = IsFun+ (Subset (\Graph -> Univ :×: Univ))+ (\_ -> ExSnd Graph)+ (\Graph Graph k -> k)+ + +graphCPS :: pair :∈: Graph f ->+ (forall a. (pair ~ (a,f a)) => r) ->+ r+graphCPS Graph k = k + + ++-- | Type constructors are injective+graphInjective :: Injective (Graph f)+graphInjective = Injective (\Graph Graph k -> k)+ ++imageGraphList ::+ [a] :∈: Image (Graph []) Univ+ + +imageGraphList = Image Univ Graph++ +instance (a~a_copy) => Fact ((a_copy, f a) :∈: Graph f) where+ auto = Graph++++data ToTyCon (f::SET) x = forall y. ToTyCon ((x,y) :∈: f) y+ +introToTyCon :: ((x, y) :∈: f) -> y -> ToTyCon f x+introToTyCon = ToTyCon + ++-- | NB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness+elimToTyCon :: (dom :~>: cod) f -> ToTyCon f x -> ((x,z) :∈: f) -> z+elimToTyCon f (ToTyCon fxy y) fxz = svalCoerce f fxy fxz y + +-- this is actually false; the two functions are just isomorphic+-- graph_TyCon :: Injective f -> (Univ :~>: cod) f -> Graph (TyCon f) :==: f++toTCG :: f x -> ToTyCon (Graph f) x+toTCG fx = ToTyCon Graph fx+ +fromTCG :: ToTyCon (Graph f) x -> f x+fromTCG (ToTyCon Graph fx) = fx+ ++-- | Graph of a @(* -> * -> *)@ type constructor+data BiGraph f :: SET where+ BiGraph :: BiGraph f ((a,b) , (f a b))+ +biGraphIsFun :: ((Univ :×: Univ) :~>: Univ) (BiGraph f)+biGraphIsFun = IsFun+ (Subset (\BiGraph -> (Univ :×: Univ) :×: Univ))+ (\(_ :×: _) -> ExSnd BiGraph)+ (\BiGraph BiGraph k -> k)+ ++-- | Type constructors are injective+biGraphInjective :: Injective (BiGraph f)+biGraphInjective = Injective (\BiGraph BiGraph k -> k)+ +instance (a~a_copy, b~b_copy) => Fact (((a_copy,b_copy), f a b) :∈: BiGraph f) where+ auto = BiGraph+ ++-- | Example of an extensional equation between functions+biGraph_eq_HaskFun :: BiGraph (->) :==: HaskFun+biGraph_eq_HaskFun = funEq biGraphIsFun haskFunIsFun+ (Subset (\BiGraph -> HaskFun))+ +-- * Constant functions++data Const dom x :: SET where+ Const :: a :∈: dom -> Const dom x (a,x)+ +constIsFun :: x :∈: cod -> (dom :~>: cod) (Const dom x)+constIsFun x = IsFun + (Subset (\(Const a) -> a :×: x))+ (\a -> ExSnd (Const a))+ (\(Const a) (Const a') k -> k)+ ++constEq :: Ex dom -> Const dom x :==: Const dom' x' -> x :=: x'+constEq (Ex a) eq = case eq `ecoerce` (Const a) of+ Const _ -> Refl++ ++-- * Dependent product++-- | NB: @fam@ must be a function mapping some set to a set of sets, or the second condition in the constructor is vacuous+data (Π (fam :: SET)) (f :: SET) where+ Π ::+ (base :~>: Unions fam) f+ ->+ (forall x y s. (x,y) :∈: f ->+ (x,Lower s) :∈: fam ->+ + x :∈: s)+ ->+ Π fam f+ ++-- -- | We represent dependent products as spaces of sections.+-- --+-- -- Let /bundleMap : total -> base/ +-- -- +-- -- Then our @(Pi) bundleMap@, in more common notation, represents:+-- --+-- -- /(Pi) (x : base). { y : total | bundleMap y = x }/+-- --++-- * Sections++-- | Expresses that @f@ is a section of @bundleMap@+data (Section (bundleMap :: SET)) (f::SET) where+ Section ::+ (forall x y. (x,y) :∈: f -> (y,x) :∈: bundleMap)+ ->+ Section bundleMap f++-- | Lemma for proving a function equal to the identity+idLemma :: ((dom :~>: dom) f) -> + (forall x y. (x,y) :∈: f -> x :=: y) ->+ (Id dom :==: f)++idLemma f p = funEq idIsFun f+ (Subset (\(Incl x) -> case total f x of+ ExSnd fxy -> case p fxy of+ Refl -> fxy))++-- | Is section ==> composition is /id/+section_CompoId ::+ + (total :~>: base) bun ->+ (base :~>: total) f ->+ ( Section bun f ) ->++ (bun :○: f :==: Id base) + +section_CompoId bun f (Section s) =+ setEqSym (idLemma (compoIsFun bun f)+ + (\(Compo bun_yx f_xy) -> case sval bun bun_yx (s f_xy) of+ Refl -> Refl)+ + )++-- | Composition is /id/ ==> is section+compoId_Section ::+ ( (total :~>: base) bun ) ->+ ( (base :~>: total) f ) ->+ (bun :○: f :==: Id base) + + -> ( Section bun f )++ +compoId_Section bun f eq =+ Section (\f_xy -> case rel f f_xy of+ (x :×: y) -> + case total bun y of+ ExSnd bun_yx' -> + case equal_f + idIsFun + eq + (Compo bun_yx' f_xy) + (Incl x) of++ Refl -> bun_yx')++ +-- * Inverses++data Inv (f :: SET) :: SET where+ Inv :: (a,b) :∈: f -> Inv f (b,a)+ +invInv0 :: Inv (Inv f) :⊆: f+invInv0 = Subset (\(Inv (Inv p)) -> p)+ ++invInv :: (dom :~>: cod) f -> (Inv (Inv f)) :==: f+invInv f = SetEq invInv0+ (Subset (\fxy -> case rel f fxy of+ _ :×: _ -> Inv (Inv fxy)))+++-- | An injective function has an inverse, with domain the image+injective_Inv :: (dom :~>: cod) f -> Injective f -> + (Image f dom :~>: dom) (Inv f)+ +injective_Inv f (Injective inj) = + IsFun+ (Subset (\(Inv fxy) -> case rel f fxy of+ x :×: _ -> Image x fxy :×: x)) + (\(Image _ fxy) -> ExSnd (Inv fxy))+ (\(Inv fxy) (Inv fx'y) k -> inj fxy fx'y k)+ +invId :: Inv (Id dom) :==: Id dom+invId = SetEq (Subset (\(Inv (Incl xx)) -> Incl xx))+ (Subset (\(Incl xx) -> (Inv (Incl xx))))+++ +-- TODO: inverse of composition+++$(lemmata ''Fact ['targetTuplingIsFun,'fstIsFun,'sndIsFun+ ,'haskFunIsFun, 'haskFunInjective+ ,'kleisliHomIsFun, 'kleisliHomInjective+ ,'compoIsFun, 'idIsFun, 'inclusionIsFun + ,'sval,'relation,'rel,'total + , 'graphInjective, 'graphIsFun+ , 'biGraphInjective, 'biGraphIsFun+ , 'funEq+ , 'extendCod+ , 'equaliserSubset, 'equaliserUni, 'equaliserIsFun+ , 'equal_f+ ,'inDom,'inCod,'domUniq+ ,'imageUnion+ ,'compo_idl,'compo_idr+ ,'lowerFun, 'raiseFun+ ,'constIsFun, 'constEq+ ++ ,'section_CompoId,'compoId_Section+ + ,'injective_Inv, 'inclusion_Injective, 'invId+ ,'preimage_Image, 'image_Preimage+++ + ])++
+ Type/Logic.hs view
@@ -0,0 +1,189 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--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)++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)) ++ " >>"+ + + +-- | 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"++-- | Existential quantification +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))++-- | 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"
+ Type/Set.hs view
@@ -0,0 +1,541 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Type.Set+--Author : Daniel Schüssler+--License : BSD3+--Copyright : Daniel Schüssler+--+--Maintainer : Daniel Schüssler+--Stability : Experimental+--Portability : Uses various GHC extensions+--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+++{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE IncoherentInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# OPTIONS + #-}+{-# OPTIONS -fwarn-missing-signatures #-}+++-- |+--+-- * Sets are encoded as certain types of kind @* -> *@+-- +-- * A value of type @S X@ is a proof that the type @X@ is a member of @S@+--+module Type.Set where+ +import Data.Type.Equality+import Type.Logic+import Type.Dummies+import Data.Monoid+import Control.Functor.Extras+import Control.Functor.Combinators.Flip+import Control.Monad+import Helper+import Control.Applicative+import Data.Typeable.Extras+import Data.Data hiding (DataType)+ + ++{----------------------------- +emacs snippets for the funny characters (move behind the final parenthesis, press C-x C-e)++(progn+ (yas/define 'haskell-mode "subs" ":⊆:")+ (yas/define 'haskell-mode "union" ":∪:")+ (yas/define 'haskell-mode "inter" ":∩:")+ (yas/define 'haskell-mode "times" ":×:")+ (yas/define 'haskell-mode "elt" ":∈:")+ (yas/define 'haskell-mode "elt1" "::∈:")+ (yas/define 'haskell-mode "circ" ":○:")+ (yas/define 'haskell-mode "Sigma" "Σ")+ (yas/define 'haskell-mode "Pi" "Π")+ (yas/define 'haskell-mode "-->" ":~>:")+ (yas/define 'haskell-mode "--->" ":~~>:")+)++-----------------------------}++++#include "defs.h.hs"+ + ++ +++-- * Subsets, equality++type a :∈: set = set a++infix 4 :∈:+++-- | Represents a proof that @set1@ is a subset of @set2@+data (set1 :: SET) :⊆: (set2 :: SET) where+ Subset :: (forall a. a :∈: set1 -> a :∈: set2) -> set1 :⊆: set2++-- | Coercion from subset to superset+scoerce :: (set1 :⊆: set2) -> a :∈: set1 -> a :∈: set2 +scoerce (Subset x) = x+ +infix 4 :⊆:+ +type Subset = (:⊆:)++-- | Extensional equality of sets+data (set1 :: (SET)) :==: (set2 :: (SET)) = SetEq (set1 :⊆: set2) (set2 :⊆: set1)+ +infix 4 :==:++instance Fact (set1 :⊆: set2 -> a :∈: set1 -> a :∈: set2) where auto = scoerce+ +-- | Coercion using a set equality+ecoerce :: (s1 :==: s2) -> a :∈: s1 -> a :∈: s2+ecoerce (SetEq p _) = scoerce p++-- | Coercion using a set equality (flipped)+ecoerceFlip :: (s1 :==: s2) -> a :∈: s2 -> a :∈: s1+ecoerceFlip (SetEq _ q) = scoerce q++subsetRefl :: s :⊆: s+subsetRefl = Subset id ++subsetTrans :: (s1 :⊆: s2 -> s2 :⊆: s3 -> s1 :⊆: s3);+subsetTrans p1 p2 = Subset (scoerce p2 . scoerce p1)+ ++setEqRefl :: s :==: s;+setEqRefl = SetEq subsetRefl subsetRefl++setEqSym :: s1 :==: s2 -> s2 :==: s1;+setEqSym (SetEq p1 p2) = SetEq p2 p1+ + +setEqTrans :: (s1 :==: s2 -> s2 :==: s3 -> s1 :==: s3);+setEqTrans (SetEq p1 p2) (SetEq q1 q2) = SetEq+ (p1 `subsetTrans` q1)+ (q2 `subsetTrans` p2)+ + +type Singleton a = (:=:) a+ +instance Fact (Singleton a a) where auto = Refl+ +instance (Fact (a :∈: set)) => (Fact (Singleton a :⊆: set)) where+ auto = Subset (\Refl -> auto)+ + +-- * Union, intersection, difference++-- | Binary union+data (s1 :: SET) :∪: (s2 :: SET) :: SET where + Union :: Either (a :∈: s1) (a :∈: s2) -> (s1 :∪: s2) a++elimUnion :: a :∈: (s1 :∪: s2) -> Either (a :∈: s1) (a :∈: s2)+elimUnion (Union x) = x+ + +infixr 5 :∪:+type Union = (:∪:)+ +unionL :: s1 :⊆: (s1 :∪: s2)+unionL = Subset (Union . Left)+unionR :: s2 :⊆: (s1 :∪: s2)+unionR = Subset (Union . Right)+ +++++ +unionMinimal :: s1 :⊆: t -> s2 :⊆: t -> (s1 :∪: s2) :⊆: t+unionMinimal p1 p2 = Subset (\(Union q) -> case q of+ Left q1 -> scoerce p1 q1+ Right q2 -> scoerce p2 q2)+ +++unionIdempotent :: s :∪: s :==: s+unionIdempotent = SetEq (unionMinimal auto auto) unionL+ +instance (Fact (s1 :⊆: t), Fact (s2 :⊆: t)) => Fact (s1 :∪: s2 :⊆: t) where+ auto = unionMinimal auto auto+++-- | Binary intersection+data ((s1 :: SET) :∩: (s2 :: SET)) :: SET where+ Inter :: a :∈: s1 -> a :∈: s2 -> (s1 :∩: s2) a+ +elimInter :: a :∈: (s1 :∩: s2) -> (a :∈: s1, a :∈: s2)+elimInter (Inter x y) = (x,y)+ +interFst :: (s1 :∩: s2) :⊆: s1+interFst = Subset (fst . elimInter)+interSnd :: (s1 :∩: s2) :⊆: s2+interSnd = Subset (snd . elimInter)+ +infixr 6 :∩:+type Inter = (:∩:)+ ++interMaximal :: (t :⊆: s1 -> t :⊆: s2 -> t :⊆: (s1 :∩: s2))+interMaximal p1 p2 = Subset (\q -> Inter (scoerce p1 q) (scoerce p2 q))+ + +instance (Fact (t :⊆: s1), Fact (t :⊆: s2)) => Fact (t :⊆: (s1 :∩: s2)) where + auto = interMaximal auto auto+ + +interIdempotent :: s :∩: s :==: s+interIdempotent = SetEq interFst (interMaximal auto auto)+ + +-- | Union of a family+data Unions (fam :: SET) :: SET where+ Unions :: forall s. Lower s :∈: fam -> a :∈: s -> Unions fam a+ +elimUnions :: Unions fam a -> (forall s. Lower s :∈: fam -> a :∈: s -> r) -> r+elimUnions (Unions p1 p2) k = k p1 p2+ +instance Fact (Lower s :∈: fam -> s :⊆: (Unions fam)) where auto p = Subset (Unions p)+ + ++-- | Dependent sum+data Σ (fam :: SET) :: SET where+ Σ :: Lower s :∈: fam -> + a :∈: s -> + Σ fam (Lower s, a)++type DependentSum = Σ++ + ++-- | Intersection of a family+data Inters (fam :: SET) :: SET where+ Inters :: (forall s. (Lower s) :∈: fam -> a :∈: s) -> Inters fam a+ +elimInters :: Inters fam a -> (Lower s) :∈: fam -> s a +elimInters (Inters x) = x+ +instance Fact ((Lower s) :∈: fam -> (Inters fam) :⊆: s ) where + auto p = Subset (($ p) . elimInters)+ +-- | Complement+data Complement (s :: SET) :: SET where + Complement :: Not (a :∈: s) -> Complement s a+ ++elimComplement :: a :∈: Complement s -> Not (a :∈: s)+elimComplement (Complement x) = x+ +type Disjoint s1 s2 = (s1 :∩: s2) :⊆: Empty+ +complContradiction :: Not (s a, Complement s a)+complContradiction (p, Complement q) = q p+ +complEmpty :: Disjoint s (Complement s)+complEmpty = Subset (elimFalsity . complContradiction . elimInter)+ +complMaximal :: Disjoint s t -> (t :⊆: Complement s)+complMaximal p = Subset (\q -> Complement (\r -> elimEmpty (p `scoerce` (Inter r q))))+ + +-- | Set difference+data Diff (s :: SET) (t :: SET) :: SET where+ Diff :: a :∈: s -> Not (a :∈: t) -> Diff s t a +++elimDiff :: a :∈: Diff s t -> (a :∈: s, Not (a :∈: t))+elimDiff (Diff x y) = (x,y)+ +-- * Products++-- | Binary products+data (s1 :: SET) :×: (s2 :: SET) :: SET where+ (:×:) :: a :∈: s1 -> b :∈: s2 -> (s1 :×: s2) (a, b)+ +infixr 6 :×:+type Prod = (:×:)+ +fstPrf :: (a, b) :∈: (s1 :×: s2) -> a :∈: s1;+fstPrf (p :×: _) = p+sndPrf :: (a, b) :∈: (s1 :×: s2) -> b :∈: s2;+sndPrf (_ :×: q) = q+ + +-- | Product is monotonic wrt. subset inclusion+prodMonotonic :: s1 :⊆: t1 + -> s2 :⊆: t2 + -> s1 :×: s2 :⊆: t1 :×: t2;++prodMonotonic p1 p2 = Subset (\(q1 :×: q2) -> scoerce p1 q1 :×: scoerce p2 q2)+ ++-- * Particular sets+-- | Empty set (barring cheating with 'undefined')+data Empty :: SET where + Empty :: (forall b. b) -> Empty a++elimEmpty :: Empty a -> b+elimEmpty (Empty x) = x+ +emptySubset :: (Empty :⊆: s)+emptySubset = Subset elimEmpty+ +-- | Set of /all/ types of kind *+data Univ :: SET where Univ :: Univ a+ +univSubset :: (s :⊆: Univ) +univSubset = Subset (const Univ)+ +data FunctionType :: SET where+ FunctionType :: FunctionType (a -> b)+functionType :: (a -> b) :∈: FunctionType+functionType = FunctionType+ ++data KleisliType m :: SET where+ KleisliType :: KleisliType m (a -> m b)+kleisliType :: (a -> m b) :∈: (KleisliType m)+kleisliType = KleisliType++data CoKleisliType w :: SET where+ CoKleisliType :: CoKleisliType w (w a -> b)+ +coKleisliType :: (w a -> b) :∈: (CoKleisliType w)+coKleisliType = CoKleisliType+ +-- *** Sets from common typeclasses++-- (yas/define 'haskell-mode "class-set" "data $1Type :: SET where $1Type :: $1 a => $1Type a\ninstance $1 a => Fact (a :∈: $1Type) where auto = $1Type\n$0")++++-- (yas/define 'haskell-mode "class-set1" "data $1Type :: SET where $1Type :: $1 a => $1Type (Lower a)\ninstance $1 a => Fact (Lower a :∈: $1Type) where auto = $1Type\n$0")++data ShowType :: SET where ShowType :: Show a => ShowType a+instance Show a => Fact (a :∈: ShowType) where auto = ShowType+ +-- | Example application+getShow :: a :∈: ShowType -> a -> String+getShow ShowType = show +++data ReadType :: SET where ReadType :: Read a => ReadType a+instance Read a => Fact (a :∈: ReadType) where auto = ReadType+data EqType :: SET where EqType :: Eq a => EqType a+instance Eq a => Fact (a :∈: EqType) where auto = EqType+getEq :: a :∈: EqType -> a -> a -> Bool+getEq EqType = (==) +data OrdType :: SET where OrdType :: Ord a => OrdType a+instance Ord a => Fact (a :∈: OrdType) where auto = OrdType+ +getCompare :: a :∈: OrdType -> a -> a -> Ordering+getCompare OrdType = compare +data EnumType :: SET where EnumType :: Enum a => EnumType a+instance Enum a => Fact (a :∈: EnumType) where auto = EnumType+data BoundedType :: SET where BoundedType :: Bounded a => BoundedType a+instance Bounded a => Fact (a :∈: BoundedType) where auto = BoundedType+data NumType :: SET where NumType :: Num a => NumType a+instance Num a => Fact (a :∈: NumType) where auto = NumType+data IntegralType :: SET where IntegralType :: Integral a => IntegralType a+instance Integral a => Fact (a :∈: IntegralType) where auto = IntegralType+data MonoidType :: SET where MonoidType :: Monoid a => MonoidType a+instance Monoid a => Fact (a :∈: MonoidType) where auto = MonoidType+data FractionalType :: SET where FractionalType :: Fractional a => FractionalType a+instance Fractional a => Fact (a :∈: FractionalType) where auto = FractionalType+ +data TypeableType :: SET where TypeableType :: Typeable a => TypeableType a+instance Typeable a => Fact (a :∈: TypeableType) where auto = TypeableType++data DataType :: SET where DataType :: Data a => DataType a+instance Data a => Fact (a :∈: DataType) where auto = DataType+++-- ** Kind (* -> *)++data FunctorType :: SET where FunctorType :: Functor a => FunctorType (Lower a)+instance Functor a => Fact (Lower a :∈: FunctorType) where auto = FunctorType+ +getFmap :: Lower f :∈: FunctorType -> (a -> b) -> (f a -> f b)+getFmap FunctorType = fmap+ +data MonadType :: SET where MonadType :: Monad a => MonadType (Lower a)+instance Monad a => Fact (Lower a :∈: MonadType) where auto = MonadType++data MonadPlusType :: SET where MonadPlusType :: MonadPlus a => MonadPlusType (Lower a)+instance MonadPlus a => Fact (Lower a :∈: MonadPlusType) where auto = MonadPlusType++data ApplicativeType :: SET where ApplicativeType :: Applicative a => ApplicativeType (Lower a)+instance Applicative a => Fact (Lower a :∈: ApplicativeType) where auto = ApplicativeType+++++-- * Powerset++-- | Membership of a set in a set representing a set of sets+type a ::∈: set = set (Lower a)++infix 4 ::∈:++-- (yas/define 'haskell-mode "k2" "SET -> *")++++-- | Powerset+data (Powerset (u :: SET)) :: SET where+ Powerset :: s :⊆: u -> Powerset u (Lower s)+ +powersetWholeset :: u ::∈: Powerset u+powersetWholeset = Powerset subsetRefl+ +powersetEmpty :: Empty ::∈: Powerset u+powersetEmpty = Powerset emptySubset+ +powersetUnion :: s1 ::∈: Powerset u -> s2 ::∈: Powerset u -> (s1 :∪: s2) ::∈: Powerset u+powersetUnion (Powerset p1) (Powerset p2) = Powerset (unionMinimal p1 p2)+ +powersetInter :: s1 ::∈: Powerset u -> s2 ::∈: Powerset u -> (s1 :∩: s2) ::∈: Powerset u+powersetInter (Powerset p1) (Powerset _) = Powerset (subsetTrans auto p1)+ + +powersetMonotonic :: (u1 :⊆: u2) -> s ::∈: Powerset u1 -> s ::∈: Powerset u2+powersetMonotonic p (Powerset q) = Powerset (Subset (scoerce p . scoerce q))+ +powersetClosedDownwards :: (s1 :⊆: s2) -> s2 ::∈: Powerset u -> s1 ::∈: Powerset u+powersetClosedDownwards p (Powerset q) = Powerset (Subset (scoerce q . scoerce p))+ +-- * Misc +autosubset :: Fact (s :⊆: t) => s :⊆: t+autosubset = auto++autoequality :: Fact (s :==: t) => s :==: t+autoequality = auto+ +data ProofSet (s :: SET) :: SET where+ ProofSet :: s x -> ProofSet s (s x)+ ++#define SUBCLASS(X,Y)\+ instance Fact (X :⊆: Y) where\+ auto = Subset (\ X -> Y )+ ++SUBCLASS(OrdType,EqType)+SUBCLASS(NumType,EqType)+SUBCLASS(IntegralType,NumType)+SUBCLASS(MonadPlusType,MonadType)+ ++-- instance ( Fact1 (s1 :⊆: s2)+-- , Fact1 (s2 :⊆: s3))++-- => Fact (s1 :⊆: s3) where+ +-- auto = subsetTrans auto auto+++ +-- * From sets to the value level+++++-- | @V s@ is the sum of all types @x@ such that @s x@ is provable.+data V (s :: SET) where+ V :: forall x. s x -> x -> V s++liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> (V s -> V s -> Bool)+liftEq s s2 (V px x) (V py y) = + case ( s `scoerce` px+ , s `scoerce` py+ , s2 `scoerce` px+ , s2 `scoerce` py) of+ + (EqType, EqType, TypeableType, TypeableType) -> dynEq x y+ ++instance ( ( Fact (s :⊆: EqType)+ , Fact (s :⊆: TypeableType) )+ + => Eq (V s) )+ where+ (==) = liftEq auto auto+ ++ +liftCompare :: (s :⊆: OrdType) -> (s :⊆: TypeableType) -> (V s -> V s -> Ordering)+liftCompare s s2 (V px x) (V py y) = + case ( s `scoerce` px+ , s `scoerce` py+ , s2 `scoerce` px+ , s2 `scoerce` py) of+ + (OrdType, OrdType, TypeableType, TypeableType) -> dynCompare x y++instance ( ( Fact (s :⊆: OrdType)+ , Fact (s :⊆: TypeableType) + , Eq (V s) )+ + => Ord (V s) )+ + where+ compare = liftCompare auto auto+ ++liftShowsPrec :: Typeable1 s => (s :⊆: ShowType) -> (s :⊆: TypeableType) -> (Int -> V s -> ShowS)+liftShowsPrec s s2 prec (V px x) =+ case ( s `scoerce` px+ , s2 `scoerce` px ) of+ + (ShowType, TypeableType) ->+ + showParen (prec > 10)+ (showString "V " .+ showString "<< proof of " . shows (typeOf px) .+ showString " >> " .+ showsPrec 11 x)+++++$(lemmata ''Fact + [ 'fstPrf,'sndPrf,'prodMonotonic+ , 'complEmpty, 'complContradiction+ , 'elimEmpty, 'emptySubset+ , 'ecoerce,'ecoerceFlip+ , 'subsetRefl+ , 'subsetTrans,'setEqRefl,'setEqSym,'setEqTrans+ , 'univSubset, 'complMaximal+ , 'powersetClosedDownwards+ , 'powersetMonotonic+ , 'interMaximal, 'unionMinimal+ , 'functionType, 'kleisliType, 'coKleisliType+ , 'interFst, 'interSnd+ ,'unionL,'unionR+ + ])+
+ Type/Set/Example.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE IncoherentInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# OPTIONS -fwarn-missing-signatures #-}++module Type.Set.Example where+ +import Data.Type.Equality+import Type.Logic+import Type.Set+import Type.Function+import Type.Dummies+import Data.Monoid+import Control.Functor.Extras+import Control.Functor.Combinators.Flip+import Control.Monad+import Helper+import Control.Applicative+import qualified Data.Map as M++#define CXT\+ (Fact (set :⊆: OrdType),\+ Fact (set :⊆: TypeableType),\+ Fact (set :⊆: EqType))++-- | A 'Map' whose keys are taken from any type which is a member of /set/+newtype SMap set a = SMap (M.Map (V set) a)+ ++singleton :: CXT =>+ k :∈: set ->+ k -> a -> SMap set a+singleton p k v = SMap (M.singleton (V p k) v)++insert :: CXT =>+ k :∈: set -> + k -> a -> SMap set a -> SMap set a++insert p k v (SMap map) = SMap (M.insert (V p k) v map)++lookup :: CXT =>+ k :∈: set ->+ k -> SMap set a -> Maybe a++lookup p k (SMap map) = M.lookup (V p k) map+ +-- | Either 'Typeable' 'Integral's, or 'String's+type ExampleSet = (TypeableType :∩: IntegralType) :∪: (Singleton String)+ +instance Fact (ExampleSet :⊆: TypeableType) where+ auto = unionMinimal interFst auto++instance Fact (ExampleSet :⊆: OrdType) where+ auto = unionMinimal (interSnd `subsetTrans` (Subset (\IntegralType -> OrdType))) auto++instance Fact (ExampleSet :⊆: EqType) where+ auto = auto `subsetTrans` (auto :: OrdType :⊆: EqType)++stringInExampleSet :: String :∈: ExampleSet+stringInExampleSet = Union (Right Refl)+++intInExampleSet :: Int :∈: ExampleSet+intInExampleSet = Union (Left (Inter auto auto))+++test :: SMap ExampleSet Integer+test = singleton stringInExampleSet "hi" 10
+ Type/defs.h.hs view
@@ -0,0 +1,56 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- |+--Module : +--Author : +--License : +--Copyright : +--+--Maintainer : +--Stability : +--Portability : +--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------++--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- |+--Module : +--Author : +--License : +--Copyright : +--+--Maintainer : +--Stability : +--Portability : +--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------++--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+-- |+--Module : +--Author : +--License : +--Copyright : +--+--Maintainer : +--Stability : +--Portability : +--+--------------------------------------------------------------------------------+--Description : +--------------------------------------------------------------------------------+--------------------------------------------------------------------------------++#define PROP *+#define SET (* -> PROP)+#define SET1 (SET -> PROP)+#define SET2 (SET1 -> PROP)+#define SET3 (SET2 -> PROP)
+ type-settheory.cabal view
@@ -0,0 +1,46 @@+name: type-settheory+version: 0.1+synopsis: + Type-level sets and functions expressed as types+description: + Type classes can express sets and functions on the type level, but they are not first-class citizens. Here we take the approach of expressing type-level sets and functions as /types/. The instance system is replaced by value-level proofs which can be directly manipulated. In this way the Haskell type level can support a quite expressive constructive set theory; for example, we have:+ .+ * Subsets and extensional set equality+ .+ * Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a kind of dependent sum and product + .+ * Functions and their composition, images, preimages, injectivity+ .+ The meaning of the proposition-types here is /not/ purely by convention; it is actually grounded in GHC \"reality\": A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inconsistent /at compile-time/ due to the fact that Haskell has general recursion, we still have that proofs of falsities are 'undefined' or non-terminating programs, so for example if 'Refl' is successfully pattern-matched, the proof must have been correct). + +category: Math, Language+license: BSD3+license-file: LICENSE+author: Daniel Schüssler+maintainer: daniels@community.haskell.org+build-type: Simple+cabal-version: >= 1.6+extra-source-files: Type/defs.h.hs+stability: Alpha++source-repository head+ type: darcs+ location: http://code.haskell.org/~daniels/type-settheory++Library+ build-depends: base >= 4, base < 5+ , syb+ , category-extras, type-equality+ , template-haskell+ , mtl+ , containers+ exposed-modules: Type.Logic+ Type.Set+ Type.Set.Example+ Type.Function+ Type.Dummies+ Data.Category+ Data.Typeable.Extras+ Control.SMonad+ other-modules: Helper+ ghc-options: