diff --git a/compdata.cabal b/compdata.cabal --- a/compdata.cabal +++ b/compdata.cabal @@ -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, - ), - 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, - ) 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. + ) as outlined in the + paper /Compositional data types/ (Workshop on Generic Programming, + 83-94, 2011, ). 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@ + -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 diff --git a/src/Data/Comp/Multi/Ops.hs b/src/Data/Comp/Multi/Ops.hs --- a/src/Data/Comp/Multi/Ops.hs +++ b/src/Data/Comp/Multi/Ops.hs @@ -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) diff --git a/src/Data/Comp/Ops.hs b/src/Data/Comp/Ops.hs --- a/src/Data/Comp/Ops.hs +++ b/src/Data/Comp/Ops.hs @@ -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) diff --git a/src/Data/Comp/SubsumeCommon.hs b/src/Data/Comp/SubsumeCommon.hs new file mode 100644 --- /dev/null +++ b/src/Data/Comp/SubsumeCommon.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-} + +-------------------------------------------------------------------------------- +-- | +-- Module : Data.Comp.SubsumeCommon +-- Copyright : (c) 2014 Patrick Bahr +-- License : BSD3 +-- Maintainer : Patrick Bahr +-- 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