valuations 0.0.4 → 0.0.5

raw patch · 7 files changed

+93/−10 lines, 7 filessetup-changed

Files

• Setup.hs +1/−1
• changelog.md +4/−0
• examples/Data/Valuation/PresheafExample.hs +68/−0
• src/Data/Valuation.hs +2/−1
• src/Data/Valuation/Presheaf.hs +4/−0
• test/Main.hs +10/−7
• valuations.cabal +4/−1

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

@@ -1,3 +1,7 @@+0.0.5++* Include example of usage of `Presheaf`+ 0.0.4  * Generalise data types over the Profunctor and not (->)

@@ -0,0 +1,68 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# OPTIONS_GHC -Wall -Werror #-}++-- | Take the category with 2 objects 1 and 2 and one arrow between then 1 -> 2 .+--+-- This is equivalent to the poset 1 <= 2 .+--+-- Take a presheaf that sends 2 to the set of strings {\"cat\"}  and 1  to the set of strings {\"animal\", \"vegetable\"} .+--+-- The restriction function is defined so that \"cat\" | 1 = \"animal\"  .+--+-- How can we define this in haskell?+module Data.Valuation.PresheafExample where++import Data.Kind (Type)+import Data.Semigroupoid (Semigroupoid (..))+import Data.Valuation.Presheaf (Presheaf (..), runPresheaf)++-- Objects of the category+data Obj = One | Two deriving (Eq, Show)++-- Morphisms (finite category)+data Cat :: Obj -> Obj -> Type where+  Id1 :: Cat 'One 'One+  Id2 :: Cat 'Two 'Two+  OneToTwo :: Cat 'One 'Two++instance Semigroupoid Cat where+  Id1 `o` Id1 = Id1+  Id2 `o` Id2 = Id2+  OneToTwo `o` Id1 = OneToTwo+  Id2 `o` OneToTwo = OneToTwo++-- Values associated with each object+data OneVal = Animal | Vegetable deriving (Eq, Show)++data TwoVal = Cat deriving (Eq, Show)++-- GADT for the presheaf object mapping+data F :: Obj -> Type where+  FOne :: OneVal -> F 'One+  FTwo :: TwoVal -> F 'Two++-- Example presheaf+presheafExample :: Presheaf Cat (->) F+presheafExample = Presheaf go+  where+    go :: Cat a b -> F b -> F a+    -- identities+    go Id1 x = x+    go Id2 x = x+    -- restriction along One -> Two+    go OneToTwo (FTwo Cat) = FOne Animal++-- Add Show instance for F+instance Show (F 'One) where+  show (FOne x) = show x++instance Show (F 'Two) where+  show (FTwo x) = show x++-- Example usage+example :: F 'One+example = runPresheaf presheafExample OneToTwo (FTwo Cat)

@@ -115,7 +115,7 @@ -- -- === Presheaf ----- A reified presheaf: 'Presheaf' @cat f cat'@ wraps @forall a b. cat a b -> cat' (f b) (f a)@, representing a contravariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is exactly 'Data.Functor.Contravariant.contramap'. Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Contravariant.Predicate', 'Data.Functor.Contravariant.Comparison', 'Data.Functor.Contravariant.Equivalence', 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@).+-- A reified presheaf: 'Presheaf' @cat f cat'@ wraps @forall a b. cat a b -> cat' (f b) (f a)@, representing a contravariant mapping from a source category @cat@ to a target category @cat'@ acting on a type constructor @f@. When both categories are @(->)@, this specialises to 'Presheaf'' @f@ wrapping @forall a b. (a -> b) -> f b -> f a@, which is exactly 'Data.Functor.Contravariant.contramap'. Unlike 'Data.Functor.Contravariant.Contravariant' which is a type class (one instance per type), this is a value — and it is generalised over the source and target categories. Values are provided for standard types ('Data.Functor.Contravariant.Predicate', 'Data.Functor.Contravariant.Comparison', 'Data.Functor.Contravariant.Equivalence', 'Data.Proxy.Proxy', @'Data.Functor.Const.Const' r@). For a worked example of defining a 'Presheaf' over a finite category, see "Data.Valuation.PresheafExample". -- -- === CovariantFunctor --@@ -204,6 +204,7 @@ -- * "Data.Valuation.Valuation" — Domain-information pairs -- * "Data.Valuation.ValuationAlgebra" — Full algebra with unit and zero -- * "Data.Valuation.ValuationAlgebraOp" — Operations on valuation algebras (@set var -> v@)+-- * "Data.Valuation.PresheafExample" — Worked example: a presheaf over a finite category module Data.Valuation   ( module V,   )

@@ -1,3 +1,4 @@+{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -18,6 +19,9 @@ -- newtype 'Presheaf' cat cat' f = 'Presheaf' (forall a b. cat a b -> cat' (f b) (f a)) -- type 'Presheaf'' f = 'Presheaf' (->) (->) f -- @+--+-- For a worked example of defining a 'Presheaf' over a finite category,+-- see "Data.Valuation.PresheafExample". module Data.Valuation.Presheaf   ( Presheaf (..),     Presheaf',

@@ -6,10 +6,13 @@ import System.Process (rawSystem)  main :: IO ()-main = exitWith =<< rawSystem "cabal"-  [ "repl"-  , "--with-compiler=doctest"-  , "--repl-options=-w"-  , "--repl-options=-Wdefault"-  , "lib:valuations"-  ]+main =+  exitWith+    =<< rawSystem+      "cabal"+      [ "repl",+        "--with-compiler=doctest",+        "--repl-options=-w",+        "--repl-options=-Wdefault",+        "lib:valuations"+      ]

@@ -1,6 +1,6 @@ cabal-version:        2.4 name:                 valuations-version:              0.0.4+version:              0.0.5 synopsis:             Valuations description:          Valuations: Valuation and Valuation Algebra license:              BSD-3-Clause@@ -35,6 +35,8 @@                       Data.Valuation.ValuationAlgebra                       Data.Valuation.ValuationAlgebraOp +                      Data.Valuation.PresheafExample+   build-depends:        base >= 4.8 && < 6                       , adjunctions >= 4.4 && < 5                       , bifunctors >= 5 && < 6@@ -50,6 +52,7 @@                       , witherable >= 0.4 && < 1    hs-source-dirs:     src+                      examples    default-language:   Haskell2010