diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,25 @@ +Copyright © 2007–2010 Brandenburgische Technische Universität Cottbus +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 the copyright holders nor the names of the 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 HOLDERS 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. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#!/usr/bin/env runghc + +> import Distribution.Simple +> main = defaultMain diff --git a/records.cabal b/records.cabal new file mode 100644 --- /dev/null +++ b/records.cabal @@ -0,0 +1,44 @@ +Name: records +Version: 0.0.0.0 +Cabal-Version: >= 1.2.3 +Build-Type: Simple +License: BSD3 +License-File: LICENSE +Copyright: © 2007–2010 Brandenburgische Technische Universität Cottbus +Author: Wolfgang Jeltsch +Maintainer: jeltsch@tu-cottbus.de +Stability: provisional +Homepage: http://community.haskell.org/~jeltsch/records/ +Bug-Reports: jeltsch@tu-cottbus.de +Package-URL: http://hackage.haskell.org/packages/archive/records/0.0.0.0/records-0.0.0.0.tar.gz +Synopsis: A flexible record system +Description: This package provides a flexible record system which has some novel features: + . + * Using record type families, the type system can be used to describe relationships + between field types. + . + * Record scheme induction permits the implementation of polymorphic record + combinators that work on whole records instead of only a fixed set of fields. + . + * Subkind polymorphism for sorts makes it possible to impose varying restrictions on + the structure of field types. +Category: Data, Records +Tested-With: GHC == 6.10.4 + +Library + Build-Depends: base >= 3.0 && < 4.1, + kinds >= 0.0 && < 0.1, + type-functions >= 0.0 && < 0.1 + Extensions: EmptyDataDecls + FlexibleContexts + FlexibleInstances + FunctionalDependencies + MultiParamTypeClasses + RankNTypes + ScopedTypeVariables + TypeFamilies + TypeOperators + UndecidableInstances + Exposed-Modules: Data.Record + Data.Record.Combinators + HS-Source-Dirs: src diff --git a/src/Data/Record.hs b/src/Data/Record.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record.hs @@ -0,0 +1,242 @@ +-- |Record core support. +module Data.Record ( + + -- * Record basics + -- $RecordBasics + X (X), + (:&) ((:&)), + (:::) ((:=)), + Name (name), + Record (fold), + Expander (Expander), + + -- * Record conversion + -- $RecordConversion + Convertible (convert), + + -- * Field separation + Separation (separate) + +) where + + import Data.Kind as Kind + import Data.TypeFun as TypeFun + + -- * Record basics + infixl 2 :& + infix 3 :::, := + + {-$RecordBasics + A record is a list of name-value pairs. Such pairs are called fields and are constructed + using the data constructor @(:=)@. Records are built from fields using the data + constructors @X@ (for the empty record) and @(:&)@ (for non-empty records that + consist of an initial record and a last field each). For example, the following expression + denotes a record that contains some information about the author of these lines: + + @ + X :& Surname := \"Jeltsch\" :& Age := 33 :& Room := \"HG/2.39\" + @ + + The type of a record has the form @/r/ /s/@ where @/r/@ is a record scheme and + @/s/@ is a representation of a type-level function, called the record style. A record + scheme is a list of name-sort pairs, which correspond to the name-value pairs of the record. + The type constructors @X@ and @(:&)@ are used to form record schemes. Name-sort + pairs are constructed using the type constructor @(:::)@. + + The name of a name-sort pair equals the name of the corresponding record field. Applying the + style to the sort yields the type of the corresponding field value. For example, the above + record has the following type: + + @ + (X :& Surname ::: String :& Age ::: Int :& Room ::: String) 'Id' + @ + + If we replace the type @Id@ by @Id -> Id@, we get a type that covers all records with a + @Surname@, an @Age@, and a @Room@ field that contain values of type @String -> String@, @Int + -> Int@, and @String -> String@, respectively. (Note that the type @Id -> Id@ represents the + type-level function @\\t -> (t -> t)@ according to the @(->)@ instance of 'TypeFun'.) + So by varying the style, we can generate a family of related record types from a single + record scheme. + -} + + -- |The empty record scheme. + data X style = X + -- ^The empty record. + deriving (Show) + + {-| + Non-empty record schemes. + -} + data (rec :& field) style = !(rec style) :& !(field style) + -- ^Non-empty records. + + {- + We use an explicit instance declaration to avoid parantheses around the first arguments of + (:&). Our instance declaration will lead to missing parantheses if a first argument of (:&) + is an application of an operator that has the same fixity as :& and is right- or + non-associative. + -} + instance (Show (rec style), Show name, Show (App style sort)) => + Show ((rec :& name ::: sort) style) where + + showsPrec enclPrec (rec :& field) = showParen (enclPrec > snocPrec) $ + showsPrec snocPrec rec . + showString " :& " . + showsPrec (succ snocPrec) field where + + snocPrec = 2 + + -- |The type of record fields. + data (name ::: sort) style = !name := App style sort + -- ^Constructs a record field from a name and a value. + + {- + We use an explicit instance declaration because the use of the type synonym family App + makes deriving (currently) impossible. + -} + instance (Show name, Show (App style sort)) => Show ((name ::: sort) style) where + + showsPrec enclPrec (name := val) = showParen (enclPrec > assignPrec) $ + showsPrec (succ assignPrec) name . + showString " := " . + showsPrec (succ assignPrec) val where + + assignPrec = 3 + + {-| + The class of name types. For each field name /N/, there should be a declaration of the + following form: + + @ + data /N/ = /N/ deriving (Show) + @ + + That way, the name can be represented in types by the type constructor /N/, and in + expressions and patterns by the data constructor /N/. Furthermore, the following + instance declaration should be added: + + @ + instance Name /N/ where +   + name = /N/ + @ + + Such instance declarations allow record combinators to construct value-level representations + of names from type-level representations. + -} + class Name name where + + -- |The sole inhabitant of the name type. + name :: name + + {-| + An instance @Record /k/ /r/@ exists if and only if /r/ is a record scheme whose sorts + are of the subkind represented by /k/. + -} + class (Kind kind) => Record kind rec where + + {-| + Folding of record schemes. This function can be used to define combinators whose types + have the form @(Record rec) => t rec@ by induction on the @rec@ parameter. + -} + fold :: thing X + -- ^ the definition of the combinator for the empty record scheme + -> (forall rec name. (Record kind rec, Name name) => + All kind (Expander thing rec name)) + {-^ + turns the definition of the combinator for a record scheme @/r/@ into the + definition for any record scheme @/r/ :& /n/ ::: /s/@ + -} + -> thing rec + -- ^ the resulting combinator that works for all record schemes + + {-| + Transformations from the definition of a record combinator for some record scheme into its + definition for an expanded record scheme. + -} + newtype Expander thing rec name sort = Expander (thing rec -> thing (rec :& name ::: sort)) + + instance (Kind kind) => Record kind X where + + fold nilAlt _ = nilAlt + + instance (Record kind rec, Name name, Inhabitant kind sort) => + Record kind (rec :& name ::: sort) where + + fold nilAlt expander = let + + Expander snocAlt = specialize expander + + in snocAlt (fold nilAlt expander) + + -- * Record conversion + {-$RecordConversion + Records are lists, so their fields are totally ordered. This order can be used to + distinguish fields that have the same name. For each name, we index the fields of this name + from right to left. We identify a field by its name and its index. However, the order of + fields with different names is superfluous. Therefore, it is worthwhile that it can be + modified. Furthermore, it is often beneficial if unnecessary fields can be ignored. That + way, record operations can be made more general since they can also work with records that + contain more than the expected fields. + + Record conversion reorders and drops fields in such a way that all remaining fields keep + their identification. So record conversion keeps the order of fields that share a common + name, and it drops a field only if all preceding fields of the same name are also dropped. + The scheme of the destination record is generated from the scheme of the source record by + applying the same reorderings and droppings that are used to transform the source record + into the destination record. The style is not changed. + -} + + -- NOTE: Convertible does not ensure that all names in the source record are instances of Name. + {-| + An instance @Convertible /r/ /r'/@ exists if and only if /r/ and /r'/ are record + schemes, and records of a type @/r/ /s/@ can be converted into records of the type @/r'/ + /s/@. + -} + class Convertible rec rec' where + + -- |Converts a record into another record. + convert :: rec style -> rec' style + + instance Convertible rec X where + + convert _ = X + + instance (Separation rec remain name' sort', Convertible remain rec') => + Convertible rec (rec' :& name' ::: sort') where + + convert rec = convert remain :& field' where + + (remain,field') = separate rec + + -- * Field separation + -- NOTE: Separate does not ensure that all names in the source record are instances of Name. + {-| + An instance @Separation /r/ /r'/ /n/ /s/@ exists if and only if the following conditions are + met: + + * @/r/@ is a record scheme that contains the name @/n/@. + + * The last name-sort pair with the name @/n/@ contains the sort @/s/@. + + * Removing that name-sort pair from @/r/@ yields @/r'/@. + -} + class (Name sepName) => Separation rec remain sepName sepSort | rec sepName -> remain where + + {-| + Extracts the last field of the respective name and returns the remaining record and the + extracted field. + -} + separate :: rec style -> (remain style,(sepName ::: sepSort) style) + + instance (Name name, sort ~ sepSort) => + Separation (rec :& name ::: sort) rec name sepSort where + + separate (rec :& field) = (rec,field) + + instance (Separation rec remain sepName sepSort, (remain :& name ::: sort) ~ extRemain) => + Separation (rec :& name ::: sort) extRemain sepName sepSort where + + separate (rec :& field) = (remain :& field,sepField) where + + (remain,sepField) = separate rec diff --git a/src/Data/Record/Combinators.hs b/src/Data/Record/Combinators.hs new file mode 100644 --- /dev/null +++ b/src/Data/Record/Combinators.hs @@ -0,0 +1,246 @@ +-- |Record combinators built on top of the record core that "Data.Record" provides. +module Data.Record.Combinators ( + + -- * Catenation + Cat, + cat, + + -- * Applicative functor operations + repeat, + (<<*>>), + map, + zipWith, + + -- * Modification + modify, + + -- * Conversion + -- FIXME: maybe don’t use the term “conversion” because of “record conversion” + toList + +) where + + -- Prelude + import Prelude hiding (repeat, map, zipWith) + import qualified Prelude -- only for documentation + + -- Data + import Data.Kind as Kind + import Data.TypeFun as TypeFun + import Data.Record as Record + + -- Control + import Control.Applicative as Applicative hiding (Const) -- only for documentation + + -- * Catenation + -- |Catenation of two record schemes. + type family Cat (rec1 :: * -> *) (rec2 :: * -> *) :: * -> * + type instance Cat rec1 X = rec1 + type instance Cat rec1 (rec2 :& name2 ::: sort2) = Cat rec1 rec2 :& name2 ::: sort2 + + -- |Catenation of two records. + cat :: (TypeFun style, Record (Domain style) rec1, Record (Domain style) rec2) => + rec1 style -> rec2 style -> Cat rec1 rec2 style + cat = let + + CatThing cat = fold catNilAlt catExpander + + in cat + + newtype CatThing style rec1 rec2 = CatThing (rec1 style -> rec2 style -> Cat rec1 rec2 style) + + catNilAlt:: (TypeFun style, Record (Domain style) rec1) => CatThing style rec1 X + catNilAlt = CatThing nilCat where + + nilCat rec1 X = rec1 + + catSnocAlt :: (TypeFun style, Record (Domain style) rec1, + Record (Domain style) rec2, Name name, Inhabitant (Domain style) sort) => + CatThing style rec1 rec2 -> CatThing style rec1 (rec2 :& name ::: sort) + catSnocAlt (CatThing cat) = CatThing snocCat where + + snocCat rec1 (rec2 :& field2) = cat rec1 rec2 :& field2 + + catExpander :: (TypeFun style, Record (Domain style) rec1, + Record (Domain style) rec2, Name name) => + All (Domain style) (Expander (CatThing style rec1) rec2 name) + catExpander = closed (Expander catSnocAlt) + + -- * Record schemes as a kind of applicative functor + {-| + Generates a record whose fields all contain the same value. In contrast to the + 'Prelude.repeat' function from the Prelude, this function generates a finite data structure. + Thereby, the size of the generated record is determined by its type. @repeat@ is almost a + proper implementation of 'pure' from the 'Applicative' class. The only problem is that the + argument of @repeat@ uses the 'Universal' type. + -} + repeat :: (TypeFun style, Record (Domain style) rec) => Universal style -> rec style + repeat = let + + RepeatThing repeat = fold repeatNilAlt repeatExpander + + in repeat + + newtype RepeatThing style rec = RepeatThing (Universal style -> rec style) + + repeatNilAlt :: (TypeFun style) => RepeatThing style X + repeatNilAlt = RepeatThing nilRepeat where + + nilRepeat _ = X + + repeatSnocAlt :: forall style rec name sort. (TypeFun style, + Record (Domain style) rec, + Name name, + Inhabitant (Domain style) sort) => + RepeatThing style rec -> RepeatThing style (rec :& name ::: sort) + repeatSnocAlt (RepeatThing repeat) = RepeatThing snocRepeat where + + snocRepeat :: Universal style -> (rec :& name ::: sort) style + snocRepeat wrappedVal = repeat wrappedVal :& + name := unwrapApp (wrappedVal :: WrappedApp style sort) + + repeatExpander :: (TypeFun style, Record (Domain style) rec, Name name) => + All (Domain style) (Expander (RepeatThing style) rec name) + repeatExpander = closed (Expander repeatSnocAlt) + + zipWithApp :: (TypeFun style, TypeFun style', Domain style ~ Domain style', + Record (Domain (style -> style')) rec) => + rec (style -> style') -> rec style -> rec style' + zipWithApp = let + + ZipWithAppThing zipWithApp = fold zipWithAppNilAlt zipWithAppExpander + + in zipWithApp + + newtype ZipWithAppThing style style' rec = ZipWithAppThing (rec (style -> style') -> + rec style -> + rec style') + + zipWithAppNilAlt :: (TypeFun style, TypeFun style', Domain style ~ Domain style') => + ZipWithAppThing style style' X + zipWithAppNilAlt = ZipWithAppThing nilZipWithApp where + + nilZipWithApp X X = X + + zipWithAppSnocAlt :: (TypeFun style, TypeFun style', Domain style ~ Domain style', + Record (Domain (style -> style')) rec, + Name name, + Inhabitant (Domain style) sort) => + ZipWithAppThing style style' rec -> + ZipWithAppThing style style' (rec :& name ::: sort) + zipWithAppSnocAlt (ZipWithAppThing zipWithApp) = ZipWithAppThing snocZipWithApp where + + snocZipWithApp (funRec :& name := fun) + (argRec :& _ := arg) = zipWithApp funRec argRec :& name := fun arg + + zipWithAppExpander :: (TypeFun style, TypeFun style', Domain style ~ Domain style', + Record (Domain (style -> style')) rec, Name name) => + All (Domain style) (Expander (ZipWithAppThing style style') rec name) + zipWithAppExpander = closed (Expander zipWithAppSnocAlt) + + infixl 4 <<*>> + {-| + Merges a record of functions and a record of arguments by applying the functions to the + corresponding arguments. The @(\<\<*\>\>)@ function would be a proper implementation + of @(\<*\>)@ from the 'Applicative' class. + -} + (<<*>>) :: (TypeFun style, TypeFun style', Domain style ~ Domain style', + Record (Domain (style -> style')) rec) => + rec (style -> style') -> rec style -> rec style' + (<<*>>) = zipWithApp + + -- ** Derived combinators + -- |Transforms a record by applying a function to all its field values. + map :: (TypeFun style, TypeFun style', Domain style ~ Domain style', + Record (Domain (style -> style')) rec) => + Universal (style -> style') -> rec style -> rec style' + map fun argRec = repeat fun <<*>> argRec + + -- |Merges two records by applying a function to each pair of corresponding field values. + zipWith :: (TypeFun style1, TypeFun style2, TypeFun style', + Domain style1 ~ Domain style2, Domain style2 ~ Domain style', + Record (Domain (style1 -> style2 -> style')) rec) => + Universal (style1 -> style2 -> style') -> rec style1 -> rec style2 -> rec style' + zipWith fun argRec1 argRec2 = repeat fun <<*>> argRec1 <<*>> argRec2 + + -- * Modification + {-| + Modifies a record by changing some of its field values. The first argument of @modify@ is + called the modification record, and the second argument is called the data record. The + result is formed by applying each field value of the modification record to the + corresponding field value of the data record and replacing the latter by the result of the + application. Data record fields that have no corresponding field in the modification record + are left unchanged. + -} + modify :: (TypeFun style, + Record (Domain style) rec, + Record (Domain style) modRec, + Convertible rec modRec) => + modRec (style -> style) -> rec style -> rec style + modify modRec = foldr (.) id $ toList (convert updateFuns <<*>> modRec) + + type UpdateFunStyle rec style = (style -> style) -> + Const (Domain style) (rec style -> rec style) + + updateFuns :: (TypeFun style, Record (Domain style) rec) => rec (UpdateFunStyle rec style) + updateFuns = let + + UpdateFunsThing updateFuns = fold updateFunsNilAlt updateFunsExpander + + in updateFuns + + newtype UpdateFunsThing style rec = UpdateFunsThing (rec (UpdateFunStyle rec style)) + + updateFunsNilAlt :: (TypeFun style) => UpdateFunsThing style X + updateFunsNilAlt = UpdateFunsThing nilUpdateFuns where + + nilUpdateFuns = X + + updateFunsSnocAlt :: (TypeFun style, + Record (Domain style) rec, Name name, Inhabitant (Domain style) sort) => + UpdateFunsThing style rec -> + UpdateFunsThing style (rec :& name ::: sort) + updateFunsSnocAlt (UpdateFunsThing updateFuns) = UpdateFunsThing snocUpdateFuns where + + snocUpdateFuns = map (WrapApp (onInit .)) updateFuns :& + name := updateFun + + updateFun mod (rec :& name := val) = rec :& name := mod val + + updateFunsExpander :: (TypeFun style, Record (Domain style) rec, Name name) => + All (Domain style) (Expander (UpdateFunsThing style) rec name) + updateFunsExpander = closed (Expander updateFunsSnocAlt) + + onInit :: (rec style -> rec style) -> + ((rec :& name ::: sort) style -> (rec :& name ::: sort) style) + onInit fun (rec :& field) = fun rec :& field + + -- * Conversion + -- |Converts a record whose style is a constant function into the list of its field values. + toList :: (Kind kind, Record kind rec) => rec (Const kind val) -> [val] + toList = reverse . toRevList + + toRevList :: (Kind kind, Record kind rec) => rec (Const kind val) -> [val] + toRevList = let + + ToRevListThing toRevList = fold toRevListNilAlt toRevListExpander + + in toRevList + + newtype ToRevListThing kind val rec = ToRevListThing (rec (Const kind val) -> [val]) + + toRevListNilAlt :: (Kind kind) => ToRevListThing kind val X + toRevListNilAlt = ToRevListThing nilToRevList where + + nilToRevList X = [] + + toRevListSnocAlt :: (Kind kind, Record kind rec, Name name, Inhabitant kind sort) => + ToRevListThing kind val rec -> + ToRevListThing kind val (rec :& name ::: sort) + toRevListSnocAlt (ToRevListThing toRevList) = ToRevListThing snocToRevList where + + snocToRevList (rec :& _ := val) = val : toRevList rec + + toRevListExpander :: (Kind kind, Record kind rec, Name name) => + All kind (Expander (ToRevListThing kind val) rec name) + toRevListExpander = closed (Expander toRevListSnocAlt)