free-categories (empty) → 0.1.0.0

raw patch · 6 files changed

+328/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

CHANGELOG.md +5/−0
LICENSE +30/−0
README.md +31/−0
Setup.hs +2/−0
free-categories.cabal +21/−0
src/Control/Category/Free.hs +239/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for free-categories++## 0.1.0.0 -- 2019-10-01++* First version.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2019, Eitan Chatav++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 Eitan Chatav nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,31 @@+# free-categories++Consider the category of Haskell "quivers" with++* objects are types of higher kind+  * `p :: k -> k -> Type`+* morphisms are terms of `RankNType`,+  * `forall x y. p x y -> q x y`+* identity is `id`+* composition is `.`++Now, consider the subcategory of Haskell `Category`s with++* constrained objects `Category c => c`+* morphisms act functorially+  * `t :: (Category c, Category d) => c x y -> d x y`+  * `t id = id`+  * `t (g . f) = t g . t f`++The [free category functor](https://ncatlab.org/nlab/show/free+category)+from quivers to `Category`s may be defined up to isomorphism as++* the functor `Path` of type-aligned lists++* the functor `FoldPath` of categorical folds++* abstractly as `CFree path => path`, the class of+  left adjoints to the functor which+  forgets the constraint on `Category c => c`++* or as any isomorphic data structure

+ Setup.hs view

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

+ free-categories.cabal view

@@ -0,0 +1,21 @@+cabal-version:       >=1.10++name:                free-categories+version:             0.1.0.0+synopsis:            free categories+description:         free categories, paths, and categorical folds+homepage:            http://github.com/morphismtech/free-categories+bug-reports:         http://github.com/morphismtech/free-categories/issues+license:             BSD3+license-file:        LICENSE+author:              Eitan Chatav+maintainer:          eitan@morphism.tech+category:            Control+build-type:          Simple+extra-source-files:  CHANGELOG.md, README.md++library+  exposed-modules:     Control.Category.Free+  build-depends:       base >=4.12 && <=5+  hs-source-dirs:      src+  default-language:    Haskell2010

+ src/Control/Category/Free.hs view

@@ -0,0 +1,239 @@+{-|+Module: Control.Category.Free+Description: free categories+Copyright: (c) Eitan Chatav, 2019+Maintainer: eitan@morphism.tech+Stability: experimental++Consider the category of Haskell "quivers" with++* objects are types of higher kind+  * @p :: k -> k -> Type@+* morphisms are terms of @RankNType@,+  * @forall x y. p x y -> q x y@+* identity is `id`+* composition is `.`++Now, consider the subcategory of Haskell `Category`s with++* constrained objects `Category` @c => c@+* morphisms act functorially+  * @t :: (Category c, Category d) => c x y -> d x y@+  * @t id = id@+  * @t (g . f) = t g . t f@++The [free category functor](https://ncatlab.org/nlab/show/free+category)+from quivers to `Category`s may be defined up to isomorphism as++* the functor `Path` of type-aligned lists++* the functor `FoldPath` of categorical folds++* abstractly as `CFree` @path => path@, the class of+  left adjoints to the functor which+  forgets the constraint on `Category` @c => c@++* or as any isomorphic data structure+-}++{-# LANGUAGE+    FlexibleInstances+  , GADTs+  , LambdaCase+  , MultiParamTypeClasses+  , PatternSynonyms+  , PolyKinds+  , QuantifiedConstraints+  , RankNTypes+  , StandaloneDeriving+#-}++module Control.Category.Free+  ( Path (..)+  , pattern (:<<)+  , FoldPath (..)+  , Category (..)+  , CFunctor (..)+  , CFoldable (..)+  , CTraversable (..)+  , CFree (..)+  , toPath+  , EndoL (..)+  , EndoR (..)+  , MCat (..)+  , ApCat (..)+  ) where++import Control.Category+import Prelude hiding (id, (.))++{- | A `Path` with steps in @p@ is a singly linked list of+"type-aligned" constructions of @p@.++>>> :{+let+  path :: Path (->) String Int+  path = length :>> (\x -> x^2) :>> Done+in+  cfold path "hello"+:}+25+-}+data Path p x y where+  Done :: Path p x x+  (:>>) :: p x y -> Path p y z -> Path p x z+infixr 7 :>>+{- | The snoc pattern for right-to-left composition.-}+pattern (:<<) :: Path p y z -> p x y -> Path p x z+pattern ps :<< p = p :>> ps+infixl 7 :<<+deriving instance (forall x y. Show (p x y)) => Show (Path p x y)+instance x ~ y => Semigroup (Path p x y) where+  (<>) = (>>>)+instance x ~ y => Monoid (Path p x y) where+  mempty = Done+  mappend = (>>>)+instance Category (Path p) where+  id = Done+  (.) path = \case+    Done -> path+    p :>> ps -> p :>> (ps >>> path)+instance CFunctor Path where+  cmap _ Done = Done+  cmap f (p :>> ps) = f p :>> cmap f ps+instance CFoldable Path where+  cfoldMap _ Done = id+  cfoldMap f (p :>> ps) = f p >>> cfoldMap f ps+  ctoMonoid _ Done = mempty+  ctoMonoid f (p :>> ps) = f p <> ctoMonoid f ps+  ctoList _ Done = []+  ctoList f (p :>> ps) = f p : ctoList f ps+  ctraverse_ _ Done = pure id+  ctraverse_ f (p :>> ps) = (>>>) <$> f p <*> ctraverse_ f ps+instance CTraversable Path where+  ctraverse _ Done = pure Done+  ctraverse f (p :>> ps) = (:>>) <$> f p <*> ctraverse f ps+instance CFree Path where csingleton p = p :>> Done++{- | Encodes a path as its `cfoldMap` function.-}+newtype FoldPath p x y = FoldPath+  {getFoldPath :: forall q. Category q => (forall x y. p x y -> q x y) -> q x y}+instance x ~ y => Semigroup (FoldPath p x y) where+  (<>) = (>>>)+instance x ~ y => Monoid (FoldPath p x y) where+  mempty = id+  mappend = (>>>)+instance Category (FoldPath p) where+  id = FoldPath $ \ _ -> id+  FoldPath g . FoldPath f = FoldPath $ \ k -> g k . f k+instance CFunctor FoldPath where cmap f = cfoldMap (csingleton . f)+instance CFoldable FoldPath where cfoldMap k (FoldPath f) = f k+instance CTraversable FoldPath where+  ctraverse f = getApCat . cfoldMap (ApCat . fmap csingleton . f)+instance CFree FoldPath where csingleton p = FoldPath $ \ k -> k p++{- | A functor from quivers to `Category`s.++prop> cmap _ id = id+prop> cmap f (c >>> c') = f c >>> f c'+-}+class (forall p. Category (c p)) => CFunctor c where+  cmap :: (forall x y. p x y -> q x y) -> c p x y -> c q x y++{- | Generalizing `Foldable` from `Monoid`s to `Category`s.++prop> cmap f = cfoldMap (csingleton . f)+-}+class CFunctor c => CFoldable c where+  {- | Map each element of the structure to a `Category`,+  and combine the results.-}+  cfoldMap :: Category q => (forall x y. p x y -> q x y) -> c p x y -> q x y+  {- | Combine the elements of a structure using a `Category`.-}+  cfold :: Category q => c q x y -> q x y+  cfold = cfoldMap id+  {- | Right-associative fold of a structure.++  In the case of `Path`s, `cfoldr`, when applied to a binary operator,+  a starting value, and a `Path`, reduces the `Path` using the binary operator,+  from right to left:++  prop> cfoldr (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == p1 ? (p2 ? ... (pn ? q) ...)+  -}+  cfoldr :: (forall x y z . p x y -> q y z -> q x z) -> q y z -> c p x y -> q x z+  cfoldr (?) q c = getEndoR (cfoldMap (\ x -> EndoR (\ y -> x ? y)) c) q+  {- | Left-associative fold of a structure.++  In the case of `Path`s, `cfoldl`, when applied to a binary operator,+  a starting value, and a `Path`, reduces the `Path` using the binary operator,+  from left to right:++  prop> cfoldl (?) q (p1 :>> p2 :>> ... :>> pn :>> Done) == (... ((q ? p1) ? p2) ? ...) ? pn+  -}+  cfoldl :: (forall x y z . q x y -> p y z -> q x z) -> q x y -> c p y z -> q x z+  cfoldl (?) q c = getEndoL (cfoldMap (\ x -> EndoL (\ y -> y ? x)) c) q+  {- | Map each element of the structure to a `Monoid`,+  and combine the results.-}+  ctoMonoid :: Monoid m => (forall x y. p x y -> m) -> c p x y -> m+  ctoMonoid f = getMCat . cfoldMap (MCat . f)+  {- | Map each element of the structure, and combine the results in a list.-}+  ctoList :: (forall x y. p x y -> a) -> c p x y -> [a]+  ctoList f = ctoMonoid (pure . f)+  {- | Map each element of a structure to an `Applicative` on a `Category`,+  evaluate from left to right, and combine the results.-}+  ctraverse_+    :: (Applicative m, Category q)+    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (q x y)+  ctraverse_ f = getApCat . cfoldMap (ApCat . f)++{- | Generalizing `Traversable` to `Category`s.-}+class CFoldable c => CTraversable c where+  {- | Map each element of a structure to an `Applicative` on a quiver,+  evaluate from left to right, and collect the results.-}+  ctraverse+    :: Applicative m+    => (forall x y. p x y -> m (q x y)) -> c p x y -> m (c q x y)++{- | Unpacking the definition of a left adjoint to the forgetful functor+from `Category`s to quivers, there must be a function `csingleton`,+such that any function++@f :: Category d => p x y -> d x y@++factors uniquely through @c p x y@ as++prop> cfoldMap f . csingleton = f+-}+class CTraversable c => CFree c where csingleton :: p x y -> c p x y++{- | `toPath` collapses any `CFoldable` into a `CFree`.+It is the unique isomorphism which exists+between any two `CFree` functors.+-}+toPath :: (CFoldable c, CFree path) => c p x y -> path p x y+toPath = cfoldMap csingleton++{- | Used in the default definition of `cfoldr`.-}+newtype EndoR p y x = EndoR {getEndoR :: forall z. p x z -> p y z}+instance Category (EndoR p) where+  id = EndoR id+  EndoR f1 . EndoR f2 = EndoR (f2 . f1)++{- | Used in the default definition of `cfoldr`.-}+newtype EndoL p x y = EndoL {getEndoL :: forall w . p w x -> p w y}+instance Category (EndoL p) where+  id = EndoL id+  EndoL f1 . EndoL f2 = EndoL (f1 . f2)++{- | Turn a `Monoid` into a `Category`,+used in the default definition of `ctoMonoid`.-}+newtype MCat m x y = MCat {getMCat :: m} deriving (Eq, Ord, Show)+instance Monoid m => Category (MCat m) where+  id = MCat mempty+  MCat g . MCat f = MCat (f <> g)++{- | Turn an `Applicative` over a `Category` into a `Category`,+used in the default definition of `ctraverse_`.-}+newtype ApCat m c x y = ApCat {getApCat :: m (c x y)} deriving (Eq, Ord, Show)+instance (Applicative m, Category c) => Category (ApCat m c) where+  id = ApCat (pure id)+  ApCat g . ApCat f = ApCat ((.) <$> g <*> f)