compdata 0.8.1.0 → 0.8.1.1

raw patch · 4 files changed

+111/−133 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• compdata.cabal +32/−26
• src/Data/Comp/Multi/Ops.hs +15/−54
• src/Data/Comp/Ops.hs +16/−53
• src/Data/Comp/SubsumeCommon.hs +48/−0

@@ -1,22 +1,18 @@ Name:			compdata-Version:		0.8.1.0+Version:		0.8.1.1 Synopsis:            	Compositional Data Types Description: -  Based on Wouter Swierstra's Functional Pearl /Data types a la carte/+  This library implements the ideas of /Data types a la carte/   (Journal of Functional Programming, 18(4):423-436, 2008,-  <http://dx.doi.org/10.1017/S0956796808006758>),-  this package provides a framework for defining recursive-  data types in a compositional manner. The fundamental idea of-  /compositional data types/ (Workshop on Generic Programming, 83-94, 2011,-  <http://dx.doi.org/10.1145/2036918.2036930>) is to separate the-  signature of a data type-  from the fixed point construction that produces its recursive-  structure. By allowing to compose and decompose signatures,-  compositional data types enable to combine data types in a flexible-  way. The key point of Wouter Swierstra's original work is to define-  functions on compositional data types in a compositional manner as-  well by leveraging Haskell's type class machinery.+  <http://dx.doi.org/10.1017/S0956796808006758>) as outlined in the+  paper /Compositional data types/ (Workshop on Generic Programming,+  83-94, 2011, <http://dx.doi.org/10.1145/2036918.2036930>). The+  purpose of this library is to allow the programmer to construct data+  types -- as well as the functions defined on them -- in a modular+  fashion. The underlying idea is to separate the signature of a data+  type from the fixed point construction that produces its recursive+  structure. Signatures can then be composed and decomposed freely.   .   Building on that foundation, this library provides additional   extensions and (run-time) optimisations which make compositional data types@@ -26,10 +22,14 @@   suited for programming language implementations, especially, in an environment   consisting of a family of tightly interwoven /domain-specific languages/.   .-  In concrete terms, this package provides the following features:+  In concrete terms, this library provides the following features:   .   *  Compositional data types in the style of Wouter Swierstra's-     Functional Pearl /Data types a la carte/.+     Functional Pearl /Data types a la carte/. The implementation of+     signature subsumption is based on the paper+     /Composing and Decomposing Data Types/ (Workshop on Generic+     Programming, 2014, to appear), which makes signature composition more+     flexible.   .   *  Modular definition of functions on compositional data types through      catamorphisms and anamorphisms as well as more structured@@ -80,15 +80,20 @@    Examples of using (generalised) compositional data types are bundled   with the package in the folder @examples@.+  .+  Previous versions of this library contained a parametric variant of+  compositional data types. This former part of the library has been+  moved to a separate package: @compdata-param@+  <https://hackage.haskell.org/package/compdata-param> -Category:            	Generics-License:		BSD3-License-file:		LICENSE-Author:			Patrick Bahr, Tom Hvitved-Maintainer:		paba@diku.dk-Build-Type:		Simple+Category:               Generics+License:                BSD3+License-file:           LICENSE+Author:                 Patrick Bahr, Tom Hvitved+Maintainer:             paba@diku.dk+Build-Type:             Simple Cabal-Version:          >=1.9.2-bug-reports:            https://bitbucket.org/paba/compdata/issues+bug-reports:            https://github.com/pa-ba/compdata/issues  extra-source-files:   -- test files@@ -157,7 +162,8 @@                         Data.Comp.Multi.Generic                         Data.Comp.Multi.Desugar -  Other-Modules:        Data.Comp.Derive.Equality+  Other-Modules:        Data.Comp.SubsumeCommon+                        Data.Comp.Derive.Equality                         Data.Comp.Derive.Ordering                         Data.Comp.Derive.Arbitrary                         Data.Comp.Derive.Show@@ -213,6 +219,6 @@   source-repository head-  type:     hg-  location: https://bitbucket.org/paba/compdata+  type:     git+  location: https://github.com/pa-ba/compdata 

@@ -27,6 +27,7 @@ import Control.Monad import Control.Applicative +import Data.Comp.SubsumeCommon  infixr 6 :+: @@ -72,25 +73,21 @@ infixl 5 :<: infixl 5 :=: -data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos-data Emb = Found Pos | NotFound | Ambiguous-- type family Elem (f :: (* -> *) -> * -> *)                  (g :: (* -> *) -> * -> *) :: Emb where     Elem f f = Found Here-    Elem f (g1 :+: g2) = Choose f (g1 :+: g2) (Elem f g1) (Elem f g2)+    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g) +    Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)     Elem f g = NotFound  -type family Choose f g (e1 :: Emb) (r :: Emb) :: Emb where-    Choose f g (Found x) (Found y) = Ambiguous-    Choose f g Ambiguous y = Ambiguous-    Choose f g x Ambiguous = Ambiguous-    Choose f g (Found x) y = Found (Le x)-    Choose f g x (Found y) = Found (Ri y)-    Choose (f1 :+: f2) g x y =  Sum' (Elem f1 g) (Elem f2 g) -    Choose f g x y = NotFound+type family Choose (e1 :: Emb) (r :: Emb) :: Emb where+    Choose (Found x) (Found y) = Ambiguous+    Choose Ambiguous y = Ambiguous+    Choose x Ambiguous = Ambiguous+    Choose (Found x) y = Found (Le x)+    Choose x (Found y) = Found (Ri y)+    Choose x y = NotFound   type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where@@ -136,53 +133,17 @@                              _      -> Nothing  -type family Or (a :: Bool) (b :: Bool) :: Bool where-    Or  False  False  = False-    Or  a      b      = True --type family AnyDupl f g where-    AnyDupl f f = False -- ignore check for duplication if subsumption is reflexive-    AnyDupl f g = Or (Dupl f '[]) (Dupl g '[])--type family Dupl (f :: (* -> *) -> * -> *) (l :: [(* -> *) -> * -> *]) :: Bool where-    Dupl (f :+: g) l = Dupl f (g ': l)-    Dupl f l         = Or (Find f l) (Dupl' l)--type family Dupl' (l :: [(* -> *) -> * -> *]) :: Bool where-    Dupl' (f ': l) = Or (Dupl f l) (Dupl' l)-    Dupl' '[]      = False--type family Find (f :: (* -> *) -> * -> *) (l :: [(* -> *) -> * -> *]) :: Bool where-    Find f (g ': l) = Or (Find' f g) (Find f l)-    Find f '[]       = False--type family Find' (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *) :: Bool where-    Find' f (g1 :+: g2) = Or (Find' f g1) (Find' f g2)-    Find' f f = True-    Find' f g = False---class NoDupl f g s-instance NoDupl f g False---- | The :<: constraint is a conjunction of two constraints. The first--- one is used to construct the evidence that is used to implement the--- injection and projection functions. The first constraint alone--- would allow instances such as @F :+: F :<: F@ or @F :+: (F :+: G)--- :<: F :+: G@ which have multiple occurrences of the same--- sub-signature on the left-hand side. Such instances are usually--- unintended and yield injection functions that are not--- injective. The second constraint excludes such instances.-type f :<: g = (Subsume (Elem f g) f g , -                NoDupl f g (AnyDupl f g))+-- | A constraint @f :<: g@ expresses that the signature @f@ is+-- subsumed by @g@, i.e. @f@ can be used to construct elements in @g@.+type f :<: g = (Subsume (ComprEmb (Elem f g)) f g)   inj :: forall f g a . (f :<: g) => f a :-> g a-inj = inj' (P :: Proxy (Elem f g))+inj = inj' (P :: Proxy (ComprEmb (Elem f g)))  proj :: forall f g a . (f :<: g) => NatM Maybe (g a) (f a)-proj = prj' (P :: Proxy (Elem f g))+proj = prj' (P :: Proxy (ComprEmb (Elem f g)))  type f :=: g = (f :<: g, g :<: f)  

@@ -23,7 +23,9 @@  import Control.Applicative import Control.Monad hiding (sequence, mapM)+import Data.Comp.SubsumeCommon + import Prelude hiding (foldl, mapM, sequence, foldl1, foldr1, foldr)  @@ -81,24 +83,20 @@ infixl 5 :<: infixl 5 :=: -data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos-data Emb = Found Pos | NotFound | Ambiguous-- type family Elem (f :: * -> *) (g :: * -> *) :: Emb where     Elem f f = Found Here-    Elem f (g1 :+: g2) = Choose f (g1 :+: g2) (Elem f g1) (Elem f g2)+    Elem (f1 :+: f2) g =  Sum' (Elem f1 g) (Elem f2 g) +    Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)     Elem f g = NotFound  -type family Choose f g (e1 :: Emb) (r :: Emb) :: Emb where-    Choose f g (Found x) (Found y) = Ambiguous-    Choose f g Ambiguous y = Ambiguous-    Choose f g x Ambiguous = Ambiguous-    Choose f g (Found x) y = Found (Le x)-    Choose f g x (Found y) = Found (Ri y)-    Choose (f1 :+: f2) g x y =  Sum' (Elem f1 g) (Elem f2 g) -    Choose f g x y = NotFound+type family Choose (e1 :: Emb) (r :: Emb) :: Emb where+    Choose (Found x) (Found y) = Ambiguous+    Choose Ambiguous y = Ambiguous+    Choose x Ambiguous = Ambiguous+    Choose (Found x) y = Found (Le x)+    Choose x (Found y) = Found (Ri y)+    Choose x y = NotFound   type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where@@ -143,51 +141,16 @@                              _      -> Nothing  -type family Or (a :: Bool) (b :: Bool) :: Bool where-    Or  False  False  = False-    Or  a      b      = True -type family AnyDupl f g where-    AnyDupl f f = False -- ignore check for duplication if subsumption is reflexive-    AnyDupl f g = Or (Dupl f '[]) (Dupl g '[])--type family Dupl (f :: * -> *) (l :: [* -> *]) :: Bool where-    Dupl (f :+: g) l = Dupl f (g ': l)-    Dupl f l         = Or (Find f l) (Dupl' l)--type family Dupl' (l :: [* -> *]) :: Bool where-    Dupl' (f ': l) = Or (Dupl f l) (Dupl' l)-    Dupl' '[]      = False--type family Find (f :: * -> *) (l :: [* -> *]) :: Bool where-    Find f (g ': l) = Or (Find' f g) (Find f l)-    Find f '[]       = False--type family Find' (f :: * -> *) (g :: * -> *) :: Bool where-    Find' f (g1 :+: g2) = Or (Find' f g1) (Find' f g2)-    Find' f f = True-    Find' f g = False---class NoDupl f g s-instance NoDupl f g False---- | The :<: constraint is a conjunction of two constraints. The first--- one is used to construct the evidence that is used to implement the--- injection and projection functions. The first constraint alone--- would allow instances such as @F :+: F :<: F@ or @F :+: (F :+: G)--- :<: F :+: G@ which have multiple occurrences of the same--- sub-signature on the left-hand side. Such instances are usually--- unintended and yield injection functions that are not--- injective. The second constraint excludes such instances.-type f :<: g = (Subsume (Elem f g) f g, -                NoDupl f g (AnyDupl f g))+-- | A constraint @f :<: g@ expresses that the signature @f@ is+-- subsumed by @g@, i.e. @f@ can be used to construct elements in @g@.+type f :<: g = (Subsume (ComprEmb (Elem f g)) f g)  inj :: forall f g a . (f :<: g) => f a -> g a-inj = inj' (P :: Proxy (Elem f g))+inj = inj' (P :: Proxy (ComprEmb (Elem f g)))  proj :: forall f g a . (f :<: g) => g a -> Maybe (f a)-proj = prj' (P :: Proxy (Elem f g))+proj = prj' (P :: Proxy (ComprEmb (Elem f g)))  type f :=: g = (f :<: g, g :<: f)  

@@ -0,0 +1,48 @@+{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.SubsumeCommon+-- Copyright   :  (c) 2014 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@diku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- Shared parts of the implementation of signature subsumption for+-- both the base and the multi library.+--+--------------------------------------------------------------------------------++module Data.Comp.SubsumeCommon where++data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos+data Emb = Found Pos | NotFound | Ambiguous++type family ComprPos (p :: Pos) :: Pos where+    ComprPos Here = Here+    ComprPos (Le p) = Le (ComprPos p)+    ComprPos (Ri p) = Ri (ComprPos p)+    ComprPos (Sum l r) = CombineMaybe (Sum l r) (Combine (ComprPos l) (ComprPos r))++type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where+    CombineMaybe p (Just p') = p'+    CombineMaybe p p'        = p++type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where+    Combine (Le l) (Le r) = Le' (Combine l r)+    Combine (Ri l) (Ri r) = Ri' (Combine l r)+    Combine (Le Here) (Ri Here) = Just Here+    Combine l r = Nothing++type family Ri' (p :: Maybe Pos) :: Maybe Pos where+    Ri' Nothing = Nothing+    Ri' (Just p) = Just (Ri p)++type family Le' (p :: Maybe Pos) :: Maybe Pos where+    Le' Nothing = Nothing+    Le' (Just p) = Just (Le p)++type family ComprEmb (e :: Emb) :: Emb where+    ComprEmb (Found p) = Found (ComprPos p)+    ComprEmb e = e