type-settheory 0.1.2 → 0.1.3
raw patch · 9 files changed
+131/−423 lines, 9 files
Files
- Control/SMonad.hs +0/−196
- Data/Category.hs +0/−184
- Data/Typeable/Extras.hs +2/−3
- Helper.hs +1/−1
- Type/Dummies.hs +14/−0
- Type/Function.hs +3/−1
- Type/Logic.hs +95/−26
- Type/Set.hs +8/−4
- type-settheory.cabal +8/−8
− Control/SMonad.hs
@@ -1,196 +0,0 @@---------------------------------------------------------------------------------------------------------------------------------------------------------------------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
@@ -1,184 +0,0 @@---------------------------------------------------------------------------------------------------------------------------------------------------------------------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-import Control.Category-import Prelude hiding(id,(.))- ---- | 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. a :∈: ob -> ExId hom a- -- | Composition- , getc :: forall a b c. - a :∈: ob ->- b :∈: ob ->- c :∈: ob ->- ExC hom a b c- }- --- | Existential wrapping of the identity function on a-data ExId hom a where- ExId :: ((a,a),aa) :∈: hom -> aa -> ExId hom a- --- | Existential wrapping of the composition for types a,b,c-data ExC hom a b c where- ExC ::- ((b,c), bc) :∈: hom ->- ((a,b), ab) :∈: hom ->- ((a,c), ac) :∈: hom ->- - (bc -> ab -> ac) ->-- ExC hom a b c-- -hask :: Cat Univ HaskFun-hask = Cat (extendCod haskFunIsFun auto)- (\_ -> ExId HaskFun id)- (\_ _ _ -> ExC HaskFun HaskFun HaskFun (.))- -kleisli :: Monad m => Cat Univ (KleisliHom m)-kleisli = Cat (extendCod kleisliHomIsFun auto)- (\_ -> ExId KleisliHom return)- (\_ _ _ -> ExC KleisliHom KleisliHom KleisliHom (<=<))- --fromControlCategory :: (Category hom) => Cat Univ (BiGraph hom)-fromControlCategory = Cat biGraphIsFun- (\_ -> ExId BiGraph id)- (\_ _ _ -> ExC BiGraph BiGraph BiGraph (.))-- --- | Lemma for constructing categories; abstracts the usage of the hom function's 'total'-makeCat :: ((ob :×: ob) :~>: Univ) hom -> - (forall a aa. ((a,a),aa) :∈: hom -> aa) ->- - (forall a b c bc ab ac.- ((b,c), bc) :∈: hom ->- ((a,b), ab) :∈: hom ->- ((a,c), ac) :∈: hom ->- - (bc -> ab -> ac)) ->--- Cat ob hom--makeCat hom k1 k2 =- Cat hom - (\a -> case total hom (a :×: a) of- ExSnd aa -> ExId aa (k1 aa))- (\a b c -> case ( total hom (b :×: c)- , total hom (a :×: b)- , total hom (a :×: c) ) of- - ( ExSnd bc- ,ExSnd ab- ,ExSnd ac ) -> -- ExC bc ab ac (k2 bc ab ac) )-- - - --- idAuto :: forall ob hom a aa. Fact (((a, a), aa) :∈: hom) => Cat ob hom -> aa--idauto :: (Fact (a :∈: ob)) => Cat ob hom -> ExId hom a-idauto cat = getid cat auto---- Cat ob hom -> bc -> ab -> ac---cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) =>- Cat ob hom -> ExC hom a b c-cauto cat = getc 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 GFunctor ob1 hom1 ob2 hom2 f = - GFunctor {- omapIsFun :: (ob1 :~>: ob2) f- , getfmap :: forall a b.- a :∈: ob1 ->- b :∈: ob1 ->- - ExFmap hom1 hom2 f a b- - }--data ExFmap hom1 hom2 f a b where- ExFmap ::- (a,fa) :∈: f ->- (b,fb) :∈: f ->- ((a,b),ab) :∈: hom1 ->- ((fa,fb),fafb) :∈: hom2 ->-- (ab -> fafb) ->-- ExFmap hom1 hom2 f a b--fromFunctor :: (Functor f) => GFunctor Univ HaskFun Univ HaskFun (Graph f)-fromFunctor = GFunctor graphIsFun (\_ _ -> ExFmap Graph Graph HaskFun HaskFun fmap)--- --- gmapCPS f afa bfb abab fafbfafb k--- = case ( total (homIsFun cat) (b :×: c)--- , total (homIsFun cat) (a :×: b)--- , total (homIsFun cat) (a :×: c) ) of- --- ( ExSnd bc--- ,ExSnd ab--- ,ExSnd ac ) -> k bc ab ac (cc cat bc ab ac) -
Data/Typeable/Extras.hs view
@@ -31,8 +31,7 @@ Just b' -> b' == b Nothing -> False -instance Ord TypeRep where- compare x y = -- compare the string representations first+compareTypeReps x y = -- compare the string representations first ((compare `on` show) x y) `mappend` -- not sure why 'typeRepKey' is in IO@@ -43,5 +42,5 @@ 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)+ Nothing -> let r = compareTypeReps (typeOf a) (typeOf b) in assert (r/=EQ) r
Helper.hs view
@@ -8,7 +8,7 @@ import Control.Monad import Data.Generics -decomposeForallT :: Type -> ([Type],Type)+decomposeForallT :: Type -> (Cxt,Type) decomposeForallT (ForallT _ cxt t) = case decomposeForallT t of (x,y) -> (cxt++x,y) decomposeForallT t = ([],t)
Type/Dummies.hs view
@@ -53,6 +53,20 @@ -- | Pair of types of kind @ SET3 @ data PAIR3 (a :: SET3) (b :: SET3) (x :: SET2) +data Bool0+data Bool1+ +data BOOL :: SET where+ Bool0 :: BOOL Bool0+ Bool1 :: BOOL Bool1+ +elimBOOL :: BOOL a -> r Bool0 -> r Bool1 -> r a+elimBOOL Bool0 x _ = x+elimBOOL Bool1 _ x = x+ +kelimBOOL :: BOOL a -> r -> r -> r+kelimBOOL Bool0 x _ = x+kelimBOOL Bool1 _ x = x -- data ΣPair (a :: SET) (b :: *)
Type/Function.hs view
@@ -404,7 +404,7 @@ -- | Composition data ((g :: SET) :○: (f :: SET)) :: SET where- Compo :: forall a b c. + Compo :: (b, c) :∈: g -> (a, b) :∈: f -> (g :○: f) (a, c)@@ -954,6 +954,8 @@ invId = SetEq (Subset (\(Inv (Incl xx)) -> Incl xx)) (Subset (\(Incl xx) -> (Inv (Incl xx)))) ++ -- TODO: inverse of composition
Type/Logic.hs view
@@ -42,13 +42,31 @@ import Data.Monoid hiding(All) import Control.Exception + +-- class Prop p where+-- proofs :: [p]+-- instance (Prop a, Prop b) => Prop (Either a b) where+-- proofs = diagonal [ fmap Left proofs, fmap Right proofs ]+ +-- instance (Prop a, Prop b) => Prop (a, b) where+-- proofs = liftM2 (,) proofs proofs+ +-- instance (Prop a, Prop b) => Prop (a -> b) where+-- proofs = case+ newtype Falsity = Falsity { elimFalsity :: forall a. a } deriving Typeable+ +-- instance Prop Falsity where proofs = []+ +-- instance Show Falsity where show _ = error "show: Proof of Falsity used" + data Truth = TruthProof deriving (Show,Typeable) -instance Show Falsity where show _ = error "show: Proof of Falsity used"+-- instance Prop Truth where proofs = [TruthProof]+ type Not a = a -> Falsity @@ -97,57 +115,98 @@ auto p q = q p -data Decidable a = Decidable { decide :: Either (Not a) a }- deriving (Show,Typeable)+-- data Decidable a = Decidable { decide :: Either (Not a) a }+-- deriving (Show,Typeable) -instance Fact (Decidable Falsity) where- auto = Decidable (Left id)+-- instance Fact (Decidable Falsity) where+-- auto = Decidable (Left id) -instance Fact (Decidable Truth) where- auto = Decidable (Right TruthProof)+-- 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+-- instance Fact (Decidable a -> Decidable b -> Decidable (a,b)) where+-- auto p1 p2 = Decidable (case (decide p1,decide p2) of+-- (Right p, Right q) -> Right (p,q)+-- (Left p, _) -> Left (p . fst)+-- (_, Left q) -> Left (q . snd)+-- )++-- instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where+-- auto p1 p2 = Decidable (case (decide p1,decide p2) of+-- (Left p, Left q) -> Left (either p q)+-- (Right p, _) -> Right (Left p)+-- (_, Right q) -> Right (Right q)+-- )++-- instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where+-- auto p1 p2 = Decidable (case decide p2 of+-- Right q -> Right (const q)+-- Left q -> case decide p1 of+-- Right p -> Left (\f -> q (f p))+-- Left p -> Right (elimFalsity . p)+-- )++-- instance Fact (Decidable a -> Decidable (Not a)) where+-- auto p1 = Decidable (case decide p1 of+-- Right p -> Left ($p)+-- Left p -> Right p+-- )++-- isLeft :: Either t t1 -> Bool+-- isLeft (Left _) = True+-- isLeft (Right _) = False++-- isRight = not . isLeft+ +-- instance Show (a :=: b) where show Refl = "Refl"++class Decidable a where decide :: Either (Not a) a+ +instance (Decidable Falsity) where+ decide = (Left id)+ +instance (Decidable Truth) where+ decide = (Right TruthProof)++instance (Decidable a, Decidable b) => Decidable (a,b) where+ decide = (case (decide ,decide ) of (Right p, Right q) -> Right (p,q) (Left p, _) -> Left (p . fst) (_, Left q) -> Left (q . snd) ) -instance Fact (Decidable a -> Decidable b -> Decidable (Either a b)) where- auto p1 p2 = Decidable (case (decide p1,decide p2) of+instance (Decidable a, Decidable b) => Decidable (Either a b) where+ decide = (case (decide ,decide ) of (Left p, Left q) -> Left (either p q) (Right p, _) -> Right (Left p) (_, Right q) -> Right (Right q) ) -instance Fact (Decidable a -> Decidable b -> Decidable (a -> b)) where- auto p1 p2 = Decidable (case decide p2 of+instance (Decidable a, Decidable b) => Decidable (a -> b) where+ decide = (case decide of Right q -> Right (const q)- Left q -> case decide p1 of+ Left q -> case decide 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+instance (Decidable a) => Decidable (Not a) where+ decide = (case decide 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+ Ex :: p b -> Ex p @@ -190,8 +249,18 @@ instance Show (a :=: b) where show Refl = "Refl" -+class Decidable1 s where+ decide1 :: Either (Not (s a)) (s a) +class Finite s where+ enum :: [Ex s] +instance Finite s => Decidable (Ex s) where+ decide = case enum of+ [] -> Left (\_ -> Falsity (assert False undefined))+ [x] -> Right x - +-- instance Finite s => Decidable (Ex s) where+-- decide = case enum of+-- [] -> Left (\_ -> Falsity (assert False undefined))+-- [x] -> Right x
Type/Set.hs view
@@ -51,7 +51,6 @@ 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)@@ -78,7 +77,6 @@ #include "../Defs.hs" - @@ -92,6 +90,8 @@ -- | 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 @@ -211,7 +211,7 @@ -- | Union of a family data Unions (fam :: SET) :: SET where- Unions :: forall s. Lower s :∈: fam -> a :∈: s -> Unions fam a+ Unions :: 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@@ -336,6 +336,10 @@ data ShowType :: SET where ShowType :: Show a => ShowType a instance Show a => Fact (a :∈: ShowType) where auto = ShowType+ +-- data ReflectShow a = ReflectShow (ShowType a) a+-- instance Show (ReflectShow a) where show (ReflectShow ShowType a) = show a+ -- | Example application getShow :: a :∈: ShowType -> a -> String@@ -472,7 +476,7 @@ -- | @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+ V :: s x -> x -> V s liftEq :: (s :⊆: EqType) -> (s :⊆: TypeableType) -> (V s -> V s -> Bool) liftEq s s2 (V px x) (V py y) =
type-settheory.cabal view
@@ -1,17 +1,19 @@ name: type-settheory-version: 0.1.2+version: 0.1.3 synopsis: - Type-level sets and functions expressed as types+ Sets and functions-as-relations in the type system 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:+ Type classes can express sets and functions on the type level, but they are not first-class. This package expresses type-level sets and functions as /types/ instead. + . + Instances are replaced by value-level proofs which can be directly manipulated; this makes quite a bit of (constructive) set theory expressible; 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 + * Unions (binary or of sets of sets), intersections, cartesian products, powersets, and a sort 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). + The proposition-types (derived from the ':=:' equality type) aren't meaningful purely by convention; they relate to the rest of Haskell as follows: A proof of @A :=: B@ gives us a safe coercion operator @A -> B@ (while the logic is inevitably inconsistent /at compile-time/ since 'undefined' proves anything, I think that we still have the property that if the 'Refl' value is successfully pattern-matched, then the two parameters in its type are actually equal). category: Math, Language license: BSD3@@ -27,7 +29,7 @@ location: http://code.haskell.org/~daniels/type-settheory Library- build-depends: base >= 4, base < 5+ build-depends: base >= 4, base < 5 , syb , type-equality , template-haskell@@ -39,8 +41,6 @@ Type.Function Type.Dummies Type.Nat- Data.Category Data.Typeable.Extras- Control.SMonad other-modules: Helper, Defs ghc-options: