constrained-category (empty) → 0.1.0.0

raw patch · 9 files changed

+369/−0 lines, 9 filesdep +algdep +basedep +categorysetup-changed

Dependencies added: alg, base, category, constrained-category, constraint, criterion, smallcheck, tasty, tasty-smallcheck, unconstrained

Files

Control/Category/Constrained.hs +90/−0
Data/Functor/Constrained.hs +107/−0
LICENSE +30/−0
Prelude.hs +14/−0
README.md +1/−0
Setup.hs +2/−0
bench/Main.hs +6/−0
constrained-category.cabal +111/−0
test/Main.hs +8/−0

+ Control/Category/Constrained.hs view

@@ -0,0 +1,90 @@+module Control.Category.Constrained (Semigroupoid (..), Category (..), Groupoid (..), Valid, NT (..), mkNT', nt') where++import Control.Categorical.Functor (map)+import qualified Control.Category as Base+import qualified Control.Category.Groupoid as Base+import Data.Constraint.Lifting+import Data.Type.Coercion+import Data.Type.Equality++class Semigroupoid (s :: α -> α -> Type) where+    (∘) :: s b c -> s a b -> s a c++type family Valid (s :: α -> α -> Type) :: α -> Constraint++class Semigroupoid s => Category s where+    id :: Valid s a => s a a+    id = id' Dict++    id' :: Dict (Valid s a) -> s a a+    id' Dict = id++class Category s => Groupoid s where+    invert :: (Valid s a, Valid s b) => s a b -> s b a+    invert = invert' Dict Dict++    invert' :: Dict (Valid s a) -> Dict (Valid s b) -> s a b -> s b a+    invert' Dict Dict = invert++instance {-# INCOHERENT #-} Base.Category s => Semigroupoid s where (∘) = (Base..)+instance {-# INCOHERENT #-} (Base.Category s, Valid s ~ Unconstrained1) => Category s where id = Base.id+instance {-# INCOHERENT #-} (Base.Groupoid s, Valid s ~ Unconstrained1) => Groupoid s where invert = Base.invert++instance {-# INCOHERENT #-} (Category s, Valid s ~ Unconstrained1) => Base.Category s where+    id = id+    (.) = (∘)++instance {-# INCOHERENT #-} (Groupoid s, Valid s ~ Unconstrained1) => Base.Groupoid s where+    invert = invert++type instance Valid (:~:) = Unconstrained1+instance Category (:~:) where id = Refl+instance Groupoid (:~:) where invert Refl = Refl++type instance Valid (:~~:) = Unconstrained1+instance Category (:~~:) where id = HRefl+instance Groupoid (:~~:) where invert HRefl = HRefl++type instance Valid Coercion = Unconstrained1+instance Category Coercion where id = Coercion+instance Groupoid Coercion where invert Coercion = Coercion++instance Semigroupoid (,) where (_, c) ∘ (a, _) = (a, c)+instance Semigroupoid Const where _ ∘ Const a = Const a++type instance Valid (->) = Unconstrained1+type instance Valid (:-) = Unconstrained1+instance Category (->) where id = Base.id+instance Category (:-) where id = Base.id++newtype NT s f g = NT { nt :: ∀ a . Valid s a => s (f a) (g a) }++instance Semigroupoid s => Semigroupoid (NT s) where NT f ∘ NT g = NT (f ∘ g)++type instance Valid (NT s) = Endolifting (Valid s)+instance Category s => Category (NT s) where+    id' d = NT (id' (lift' d))++instance Groupoid s => Groupoid (NT s) where+    invert' ad bd (NT f) = NT (invert' (lift' ad) (lift' bd) f)++lift' :: c a => Dict (Lifting c d f) -> Dict (d (f a))+lift' d = map (go d) Dict+  where go :: Dict (Lifting c d f) -> c a :- d (f a)+        go d = withDict d lift++instance Semigroupoid k => Semigroupoid (Dual k) where+    Dual f ∘ Dual g = Dual (g ∘ f)++type instance Valid (Dual k) = Valid k+instance Category k => Category (Dual k) where+    id = Dual id++instance Groupoid k => Groupoid (Dual k) where+    invert = Dual ∘ invert ∘ dual++nt' :: NT s f g -> Dict (Valid s a) -> s (f a) (g a)+nt' (NT f) Dict = f++mkNT' :: (∀ a . Dict (Valid s a) -> s (f a) (g a)) -> NT s f g+mkNT' f = NT (f Dict)

+ Data/Functor/Constrained.hs view

@@ -0,0 +1,107 @@+module Data.Functor.Constrained where++import qualified Control.Categorical.Functor as U+import Control.Category.Constrained+import qualified Data.Functor as Base++-- | Laws:+--+-- @+-- 'map' (f '∘' g) = 'map' f '∘' 'map' g+-- @+class (Semigroupoid s, Semigroupoid t) => SGM (s :: α -> α -> *) (t :: β -> β -> *) (f :: α -> β) where+    map :: s a b -> t (f a) (f b)++-- | Laws:+--+-- @+-- 'map' 'id' = 'id'+-- @+class (SGM s t f, Category s, Category t) => Functor s t f++type Endofunctor s = Functor s s++infixl 4 <$>+(<$>) :: SGM s (->) f => s a b -> f a -> f b+(<$>) = map++instance {-# INCOHERENT #-} Base.Functor f => SGM (->) (->) f where map = Base.fmap+instance {-# INCOHERENT #-} Base.Functor f => Functor (->) (->) f++instance SGM (:-) (->) Dict where map = U.map+instance Functor (:-) (->) Dict++instance (SGM s (->) f, Valid s ~ Unconstrained1) => SGM (NT s) (NT (->)) (Compose f) where+    map (NT f) = NT (\ (Compose x) -> Compose (map f x))+instance (Functor s (->) f, Valid s ~ Unconstrained1) => Functor (NT s) (NT (->)) (Compose f)++instance SGM (NT (->)) (NT (NT (->))) Compose where+    map (NT f) = NT (NT (\ (Compose x) -> Compose (f x)))+instance Functor (NT (->)) (NT (NT (->))) Compose++instance (SGM s (->) f, SGM s (->) g) => SGM s (->) (Sum f g) where+    map f (InL x) = InL (f <$> x)+    map f (InR y) = InR (f <$> y)+instance (Functor s (->) f, Functor s (->) g) => Functor s (->) (Sum f g)++instance SGM (NT (->)) (NT (->)) (Sum f) where+    map (NT f) = NT (\ case InL x -> InL x+                            InR y -> InR (f y))+instance Functor (NT (->)) (NT (->)) (Sum f)++instance SGM (NT (->)) (NT (NT (->))) Sum where+    map (NT f) = NT (NT (\ case InL x -> InL (f x)+                                InR y -> InR y))+instance Functor (NT (->)) (NT (NT (->))) Sum++instance (SGM s (->) f, SGM s (->) g) => SGM s (->) (Product f g) where+    map f (Pair x y) = Pair (f <$> x) (f <$> y)+instance (Functor s (->) f, Functor s (->) g) => Functor s (->) (Product f g)++instance SGM (NT (->)) (NT (->)) (Product f) where+    map (NT f) = NT (\ (Pair x y) -> Pair x (f y))+instance Functor (NT (->)) (NT (->)) (Product f)++instance SGM (NT (->)) (NT (NT (->))) Product where+    map (NT f) = NT (NT (\ (Pair x y) -> Pair (f x) y))+instance Functor (NT (->)) (NT (NT (->))) Product++instance Semigroupoid s => SGM s (->) (Const a) where+    map _ (Const a) = Const a+instance Category s => Functor s (->) (Const a)++instance SGM (->) (NT (->)) Const where+    map f = NT (\ (Const a) -> Const (f a))+instance Functor (->) (NT (->)) Const++instance SGM (->) (->) Identity where+    map f (Identity a) = Identity (f a)+instance Functor (->) (->) Identity++instance Semigroupoid s => SGM s (->) Proxy where+    map _ Proxy = Proxy+instance Category s => Functor s (->) Proxy++instance SGM (->) (->) ((,) a) where+    map f (a, b) = (a, f b)+instance Functor (->) (->) ((,) a)++instance SGM (->) (NT (->)) (,) where+    map f = NT (\ (a, b) -> (f a, b))+instance Functor (->) (NT (->)) (,)++instance SGM (->) (->) (Either a) where+    map _ (Left a) = Left a+    map f (Right b) = Right (f b)+instance Functor (->) (->) (Either a)++instance SGM (->) (NT (->)) Either where+    map f = NT (\ case Left a -> Left (f a)+                       Right b -> Right b)+instance Functor (->) (NT (->)) Either++instance Semigroupoid s => SGM s (->) (s a) where map = (∘)+instance Category s => Functor s (->) (s a)++instance Semigroupoid s => SGM (Dual s) (NT (->)) s where map (Dual f) = NT (∘ f)+instance Category s => Functor (Dual s) (NT (->)) s

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright Author name here © 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.

+ Prelude.hs view

@@ -0,0 +1,14 @@+module Prelude (module A) where++import Algebra as A (Semigroup (..), Monoid (..), Group)+import Control.Category.Dual as A (Dual (..))+import Data.Constraint as A+import Data.Either as A (Either (..))+import Data.Functor.Compose as A (Compose (..))+import Data.Functor.Identity as A (Identity (..))+import Data.Functor.Const as A (Const (..))+import Data.Functor.Product as A (Product (..))+import Data.Functor.Sum as A (Sum (..))+import Data.Proxy as A (Proxy (..))+import Data.Kind as A (Constraint, Type)+import Unconstrained as A (Unconstrained1)

+ README.md view

@@ -0,0 +1,1 @@+# constrained-category

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ bench/Main.hs view

@@ -0,0 +1,6 @@+module Main where++import Criterion.Main++main :: IO ()+main = defaultMain []

+ constrained-category.cabal view

@@ -0,0 +1,111 @@+name:                constrained-category+version:             0.1.0.0+synopsis:            Constrained Categories+-- description:+license:             BSD3+license-file:        LICENSE+author:              Author name here+maintainer:          example@example.com+copyright:           2018 Author name here+-- category:            +build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++library+  hs-source-dirs:      .+  exposed-modules:     Control.Category.Constrained+                     , Data.Functor.Constrained+  other-modules:       Prelude+  build-depends:       base >= 4.7 && < 5+                     , alg >=0.2 && <0.3+                     , category >= 0.2.2 && < 0.3+                     , constraint >= 0.1.3 && < 0.2+                     , unconstrained >= 0.1 && < 0.2+  default-language:    Haskell2010+  default-extensions:  UnicodeSyntax+                     , LambdaCase+                     , EmptyCase+                     , TypeOperators+                     , InstanceSigs+                     , PartialTypeSignatures+                     , RankNTypes+                     , PolyKinds+                     , ConstraintKinds+                     , FlexibleContexts+                     , FlexibleInstances+                     , TypeFamilies+                     , MultiParamTypeClasses+                     , MonadComprehensions+                     , StandaloneDeriving+                     , GeneralizedNewtypeDeriving+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing+                       -Wincomplete-record-updates -Wincomplete-uni-patterns+                       -Werror=incomplete-patterns+                       -Werror=incomplete-uni-patterns+                       -Werror=incomplete-record-updates+                       -Werror=missing-fields+                       -Werror=missing-methods++test-suite test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             Main.hs+  build-depends:       base >=4.11 && <5+                     , smallcheck >=1.1.4+                     , tasty >=1.0+                     , tasty-smallcheck >=0.8+                     , constrained-category+  default-language:    Haskell2010+  default-extensions:  UnicodeSyntax+                     , LambdaCase+                     , EmptyCase+                     , InstanceSigs+                     , PartialTypeSignatures+                     , PolyKinds+                     , ConstraintKinds+                     , FlexibleContexts+                     , FlexibleInstances+                     , MonadComprehensions+                     , StandaloneDeriving+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing+                       -Wincomplete-record-updates -Wincomplete-uni-patterns+                       -Werror=incomplete-patterns+                       -Werror=incomplete-uni-patterns+                       -Werror=incomplete-record-updates+                       -Werror=missing-fields+                       -Werror=missing-methods++benchmark bench+  type:                exitcode-stdio-1.0+  hs-source-dirs:      bench+  main-is:             Main.hs+  build-depends:       base >=4.11 && <5+                     , criterion >=1.4.1+                     , constrained-category+  default-language:    Haskell2010+  default-extensions:  UnicodeSyntax+                     , LambdaCase+                     , EmptyCase+                     , InstanceSigs+                     , PartialTypeSignatures+                     , PolyKinds+                     , ConstraintKinds+                     , FlexibleContexts+                     , FlexibleInstances+                     , MonadComprehensions+                     , StandaloneDeriving+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing+                       -Wincomplete-record-updates -Wincomplete-uni-patterns+                       -Werror=incomplete-patterns+                       -Werror=incomplete-uni-patterns+                       -Werror=incomplete-record-updates+                       -Werror=missing-fields+                       -Werror=missing-methods++source-repository head+  type:     git+  location: https://github.com/githubuser/constrained-category.hs

+ test/Main.hs view

@@ -0,0 +1,8 @@+module Main where++import Test.SmallCheck+import Test.Tasty+import Test.Tasty.SmallCheck++main :: IO ()+main = defaultMain $ testGroup "" []