type-settheory 0.1 → 0.1.1
raw patch · 6 files changed
+259/−18 lines, 6 filesdep −category-extras
Dependencies removed: category-extras
Files
- Type/Function.hs +68/−12
- Type/Logic.hs +8/−0
- Type/Nat.hs +173/−0
- Type/Set.hs +7/−2
- Type/Set/Example.hs +0/−2
- type-settheory.cabal +3/−2
Type/Function.hs view
@@ -41,7 +41,6 @@ import Type.Logic import Type.Set import Data.Type.Equality-import Control.Functor.Combinators.Flip import Control.Arrow import Helper import Type.Dummies@@ -58,6 +57,19 @@ data ExSnd (f :: SET) (a :: *) :: * where ExSnd :: (a, ex) :∈: f -> ExSnd f a +-- | Totality+type Total dom f =+ (forall (a :: *). a :∈: dom -> ExSnd f a) ++-- | Single-valuedness (CPS)+type Sval f =+ (forall a b1 b2 r.++ (a, b1) :∈: f -> + (a, b2) :∈: f -> + ((b1 ~ b2) => r) ->+ r)+ -- * Functions @@ -74,17 +86,11 @@ (f :⊆: (dom :×: cod)) -- Totality- -> (forall (a :: *). a :∈: dom -> ExSnd f a) + -> Total dom f - -- Single-valuedness (CPS)- -> (forall a b1 b2 r.-- (a, b1) :∈: f -> - (a, b2) :∈: f -> - ((b1 ~ b2) => r) ->- r)+ -> Sval f - -> (dom :~>: cod) f+ -> (dom :~>: cod) f infixr 6 :~>:, :~~>: @@ -451,7 +457,19 @@ compo_idr f = funEq (compoIsFun f idIsFun) f (Subset (\(Compo fxy (Incl x)) -> fxy)) - + ++compo_assoc+ ::+ (:~>:) s2 cod g+ -> (:~>:) s21 s2 f+ -> (:~>:) dom s21 f1+ -> ((g :○: f) :○: f1) :==: (g :○: (f :○: f1))++compo_assoc h g f = funEq ((compoIsFun h g) `compoIsFun` f)+ (h `compoIsFun` (g `compoIsFun` f))+ (Subset (\(Compo (Compo vh vg) vf) ->+ Compo vh (Compo vg vf))) -- * Equalisers -- | Equalisers :D@@ -642,7 +660,44 @@ where auto = targetTuplingIsFun auto auto+ ++fst_tupling :: + (dom :~>: cod1) f1 ->+ (dom :~>: cod2) f2 ->+ + Fst cod1 cod2 :○: (f1 :***: f2) :==: f1+ +fst_tupling f1 f2 = funEq (compoIsFun fstIsFun (targetTuplingIsFun f1 f2)) f1+ (Subset (\(Compo (Fst _ _) (vf1 :***: _)) -> vf1))+ +snd_tupling :: + (dom :~>: cod1) f1 ->+ (dom :~>: cod2) f2 ->+ + Snd cod1 cod2 :○: (f1 :***: f2) :==: f2+ +snd_tupling f1 f2 = funEq (compoIsFun sndIsFun (targetTuplingIsFun f1 f2)) f2+ (Subset (\(Compo (Snd _ _) (_ :***: vf2)) -> vf2))+ ++tupling_eta :: + (dom :~>: (cod1 :×: cod2)) f ->++ ((Fst cod1 cod2 :○: f)+ :***: + (Snd cod1 cod2 :○: f))++ :==: f+ +tupling_eta f = funEq (targetTuplingIsFun (fstIsFun `compoIsFun` f) + (sndIsFun `compoIsFun` f)) f++ (Subset (\((Compo (Fst _ _) vf) :***: (Compo (Snd _ _) vf')) ->+ case sval f vf vf' of+ Refl -> vf))+ -- * Particular functions -- | The type-level function:@@ -926,9 +981,10 @@ ,'injective_Inv, 'inclusion_Injective, 'invId ,'preimage_Image, 'image_Preimage+ ,'compo_assoc - + ,'fst_tupling, 'snd_tupling, 'tupling_eta ])
Type/Logic.hs view
@@ -40,6 +40,7 @@ import Control.Monad.Cont import Data.Typeable import Data.Monoid hiding(All)+import Control.Exception newtype Falsity = Falsity { elimFalsity :: forall a. a } deriving Typeable@@ -187,3 +188,10 @@ deriving instance Typeable2 (:=:) instance Show (a :=: b) where show Refl = "Refl"+++++++
+ Type/Nat.hs view
@@ -0,0 +1,173 @@+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+--Module : Type.Nat+--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 FlexibleContexts #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# OPTIONS -Wall #-}++-- | TODO+--+-- * Prove that 'Initor' is an 'NMorphism'+--+-- * Prove that it is uniquely so+--+module Type.Nat where++import Type.Set+import Type.Dummies()+import Type.Function+import Type.Logic()+import Data.Type.Equality+import Control.Monad()+import Control.Exception++#include "defs.h.hs"+ +-- | Sets equipped with a constant and a function to itself+data NStructure set z succ where+ NStructure :: z :∈: set -> (set :~>: set) succ ->+ NStructure set z succ++-- | Structure-preserving maps of 'NStructure's+data NMorphism set1 z1 succ1 set2 z2 succ2 (f :: SET) where+ NMorphism :: NStructure set1 z1 succ1 ->+ NStructure set2 z2 succ2 ->+ (set1 :~>: set2) f ->+ (f z1 :=: z2) ->+ (f :○: succ1 + :==:+ succ2 :○: f) ->++ NMorphism set1 z1 succ1 z2 set2 succ2 f+ +-- | Expresses that @(set1,z1,succ1)@ is initial in the cat of 'NStructure's, in other words, that it is isomorphic to the natural numbers+data NInitial set1 z1 succ1 where+ NInitial :: (forall z2 set2 succ2. ExUniq1 (NMorphism set1 z1 succ1 z2 set2 succ2))+ -> NInitial set1 z1 succ1+ ++-- data IsPeano nat z succ = +-- IsPeano {+-- succ_fun :: (nat :~>: nat) succ+-- , succ_inj :: Injective succ+-- , not_succ_zero :: forall n. n :∈: nat -> Not ((n,z) :∈: succ)+-- , induction :: forall set. z :∈: set -> +-- (forall n n1. n :∈: set -> +-- (n,n1) :∈: succ ->+-- n1 :∈: set) ->++-- set :==: nat+-- }++-- | Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let's call these /TNats/+data TNat z s :: SET where+ IsZ :: TNat z s z+ IsS :: TNat z s n -> TNat z s (s n)+-- | Successor function made from a unary type constructor+data Succ z s :: SET where + Succ :: n :∈: TNat z s -> Succ z s (n,s n)+ +succFun :: (TNat z s :~>: TNat z s) (Succ z s)+succFun = IsFun (Subset (\(Succ n) -> n :×: IsS n))+ (ExSnd . Succ)+ (\(Succ _) (Succ _) k -> k)+ +tyconNStruct :: NStructure (TNat z s) z (Succ z s)+tyconNStruct = NStructure IsZ succFun+ +-- | The unique morphism from an 'TNat' to any 'NStructure' +--+-- NB: @s@ is a type constructor, but @succ2@ is a Function ('IsFun')+data Initor z s z2 succ2 :: SET where+ InitorZ :: Initor z s z2 succ2 (z,z2)+ InitorS :: Initor z s z2 succ2 (n1, n2) -> + (n2,sn2) :∈: succ2 ->+ Initor z s z2 succ2 (s n1, sn2)+ ++initorFun :: forall z s set2 z2 succ2. NStructure set2 z2 succ2 -> + (TNat z s :~>: set2) (Initor z s z2 succ2)+ +initorFun (NStructure z2 succ2) =++ let + prelation :: pair :∈: Initor z s z2 succ2 -> + pair :∈: TNat z s :×: set2+ + prelation InitorZ = IsZ :×: z2+ prelation (InitorS i0 p) = case prelation i0 of+ q1 :×: _ -> + IsS q1 + :×: + inCod succ2 p+ + ptotal :: n :∈: TNat z s -> ExSnd (Initor z s z2 succ2) n+ ptotal IsZ = ExSnd InitorZ+ ptotal (IsS n) = + case ptotal n of+ ExSnd (inn2 :: Initor z s z2 succ2 (n,n2)) -> + + (let+ succ2ofn2 :: ExSnd succ2 n2+ succ2ofn2 =+ case prelation inn2 of+ _ :×: n2 ->+ total succ2 n2+ in+ case succ2ofn2 of + ExSnd e -> ExSnd (InitorS inn2 e))+ + psval :: Initor z s z2 succ2 (n,n2) ->+ Initor z s z2 succ2 (m,m2) ->+ n2 :=: m2+ + psval InitorZ InitorZ = Refl+ psval (InitorS inn2 succ2n2) (InitorS inn2' succ2'n2') = + case psval inn2 inn2' of+ Refl ->+ case sval succ2 succ2n2 succ2'n2' of+ Refl -> Refl+ + -- Currently impossible without 'undefined' :-(++ -- http://www.nabble.com/Is-it-possible-to-prove-type-*non*-equality-in-Haskell--to25142999.html + psval (InitorS _ _) InitorZ = assert False undefined+ psval InitorZ (InitorS _ _) = assert False undefined+ in+ IsFun (Subset prelation) ptotal (\p1 p2 k -> case psval p1 p2 of + Refl -> k)+++-- tyconPeano :: IsPeano (TNat z s) z (Succ z s)+-- tyconPeano = IsPeano succFun+-- (Injective (\(Succ _) (Succ _) k -> k))+ +-- undefined undefined+++
Type/Set.hs view
@@ -45,8 +45,6 @@ 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@@ -456,6 +454,13 @@ -- => Fact (s1 :⊆: s3) where -- auto = subsetTrans auto auto++-- * Unique existence of sets++-- | Unique existence, unlowered+data ExUniq1 (p :: SET -> *) where+ ExUniq1 :: p b -> (forall b'. p b' -> b :==: b') -> ExUniq1 p+
Type/Set/Example.hs view
@@ -19,8 +19,6 @@ 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
type-settheory.cabal view
@@ -1,5 +1,5 @@ name: type-settheory-version: 0.1+version: 0.1.1 synopsis: Type-level sets and functions expressed as types description: @@ -30,7 +30,7 @@ Library build-depends: base >= 4, base < 5 , syb- , category-extras, type-equality+ , type-equality , template-haskell , mtl , containers@@ -39,6 +39,7 @@ Type.Set.Example Type.Function Type.Dummies+ Type.Nat Data.Category Data.Typeable.Extras Control.SMonad