I think this would be a BIG mistake. Whatever system GHC settles on is almost certain to become part of the Haskell standard, and this particular system has some deep limitations which could not be got round without ripping it all out and starting again. The problem with this (and other "Flex-like") systems is that they take record extension as the basic operation of record building, rather than record merging. This means that you can only ever add or update statically determined fields of a given record. An important application which is made impossible by this approach is functions with optional arguments. For example, if you look at the definition of R (the statistics system) every function has a small number of mandatory positional arguments, and a very large number of optional named arguments, which take sensible default values. I want to be able to write:
f opts x = let vals = {Opt1 =: default1, ... } |: opts in ... vals ... x ...
where '{Opt1 =: default1, ... }' is some fixed record of default values, and '|:' is record overwrite. The type of f should be
f :: (a `Subrecord` {Opt1 :=: t1, ...}) => a -> b -> c
where '{Opt1 :=: t1, ...}' is the (fixed) type of '{Opt1 =: default1, ... }' (and x::b, and c is the type of the result). The condition 'a `Subrecord` {Opt1 :=: t1, ...}' in the context of this type means that every field of 'opts :: a' must be a field of '{Opt1 :=: t1, ...}', but opts can have as few fields as you like. This is exactly what you want for optional arguments. This could never be defined in any "Flex-like" system, because these systems depend on the fact that their record types can be reduced to a type variable extended by a fixed set of labels. This is a major restriction to what you can do with them: you can never define operations like '|:' or '+:' where the second argument does not have a constant set of fields. This restriction does not hold for more flexible systems like that defined by Oleg & co using functional dependencies, or the one I proposed on this list using type families. Although these systems are much more flexible than the "scoped labels" system, they would take LESS work to add to GHC because they have less built-in syntax, and are almost entirely defined in a library. I second the call for a records system, but please don't limit us to something like scoped labels! Barney.
Hello Barney, Sunday, November 11, 2007, 2:34:14 PM, you wrote:
An important application which is made impossible by this approach is
i propose to start "Records project" by composing list of requirements/applications to fulfill; we can keep it on Wiki page. this will create base for language theorists to investigate various solutions. i think they will be more motivated seeing our large interest in this extension -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
On Sun, Nov 11, 2007 at 03:02:56PM +0300, Bulat Ziganshin wrote:
Hello Barney,
Sunday, November 11, 2007, 2:34:14 PM, you wrote:
An important application which is made impossible by this approach is
i propose to start "Records project" by composing list of requirements/applications to fulfill; we can keep it on Wiki page. this will create base for language theorists to investigate various solutions. i think they will be more motivated seeing our large interest in this extension
+1 Stefan
Bulat Ziganshin wrote:
i propose to start "Records project" by composing list of requirements/applications to fulfill; we can keep it on Wiki page.
Wiki page duly created http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords
I've tried to summarise the important differences between the various proposals on the wiki page, but it still needs lots of illustrative examples. Anyone who is interested, please contribute! Barney.
Whatever system GHC settles on is almost certain to become part of the Haskell standard, and this particular system has some deep limitations which could not be got round without ripping it all out and starting again.
i'd like to have "extensible records", but i'd rather like to decompose this complex language feature into its components, and then have better support for each of those components, which will be simpler, could be combined to support different record system variants, and are likely to have other applications. in light of this, what library-based record proposals have to offer are light-weight case studies of useability and feature composition. once we know which kind of record system we want, we can then think about which parts of it need better language and implementation support. even before we converge on any specific system, there might be features that are shared by all contending proposals. some time ago (was that really 2 years? trac claims it was), i suggested that any record system with first-class labels needs language support for type sharing: if i import modules A and B, each of which introduces a record-label X, i need some way of telling the type system that A.X ~ B.X (Trex solved that problem by not requiring label declarations at all, but Trex labels weren't first-class objects, either). i made a haskell prime ticket for it (which was duly classified as "maybe" and then ignored;-), to which i also attached an implementation of records that, in contrast to other record libraries, does not depend on label ordering, as an illustration: http://hackage.haskell.org/trac/haskell-prime/ticket/92 http://hackage.haskell.org/trac/haskell-prime/attachment/ticket/92/Data.Reco... the code was inspired by Daan's system, i think, because not removing label overlap made the type class hacking a lot easier, but went slightly beyond in supporting record concatenation (i've been waiting for type functions to support overlap resolution, so that i can port the code; the fact that this is still future work supports the argument that haskell'2006 should have appeared with a functional dependencies addendum instead of waiting for better things to happen?-): poor man's records using nested tuples and declared labels: apart from record extension (,), we've got field selection (#?), field removal (#-), field update (#!), field renaming (#@), symmetric record concatenation (##), .. anything missing? see main at the bottom for examples of use. submitted to support proposal for first class labels in Haskell'. Claus Reinke, February 2006 i just downloaded the old Data.Record code and it still loads and runs in a recent ghc head, giving examples of all operations (these days, one might want to clean up the syntax with some infix constructors, but at the time i was still hoping to get it to work in hugs as well..): *Data.Record> main records r1 : ((A,True),((B,'a'),((C,1),()))) r2 : ((A,False),((B,'b'),((C,2),((A,True),((B,'a'),((C,1),())))))) r3 : ((D,"hi there"),((B,["who's calling"]),())) symmetric record concatenation r4a = r1 ## r3: ((A,True),((B,'a'),((C,1),((D,"hi there"),((B,["who's calling"]),()))))) r4b = r3 ## r1: ((D,"hi there"),((B,["who's calling"]),((A,True),((B,'a'),((C,1),()))))) record selection x1 r = (r #? B, r #? C, r #? A) x1 r1: ('a',1,True) x1 r2: ('b',2,False) x1 r4a: ('a',1,True) x1 r4b: (["who's calling"],1,True) x2 r = (r #? B, r #? D) x2 r4a: ('a',"hi there") x2 r4b: (["who's calling"],"hi there") record field removal x3 r = r #- D #- B x3 r1: ((A,True),((C,1),())) x3 r2: ((A,False),((C,2),((A,True),((B,'a'),((C,1),()))))) x3 r3: () x3 r4a: ((A,True),((C,1),((B,["who's calling"]),()))) x3 r4b: ((A,True),((B,'a'),((C,1),()))) record field update (r2 #! B) "dingbats": ((B,"dingbats"),((A,False),((C,2),((A,True),((B,'a'),((C,1),())))))) record field renaming (r2 #@ D) C: ((D,2),((A,False),((B,'b'),((A,True),((B,'a'),((C,1),()))))))
f opts x = let vals = {Opt1 =: default1, ... } |: opts in ... vals ... x ...
where '{Opt1 =: default1, ... }' is some fixed record of default values, and '|:' is record overwrite. The type of f should be
f :: (a `Subrecord` {Opt1 :=: t1, ...}) => a -> b -> c
in Hugs' Trex that would be: Hugs.Trex> :t let f opts x = (opt1="default"|opts) in f let {...} in f :: a\opt1 => Rec a -> b -> Rec (opt1 :: [Char] | a) but that still doesn't give you things like record concatenation. in principle, the record-concatenation-for-free trick works with Trex, but it falls apart if you need to define type classes involving record types. because then you need to be specific about the types, making those labels explicit. (btw, what is "Flex-like"?) claus
Hugs.Trex> :t let f opts x = (opt1="default"|opts) in f let {...} in f :: a\opt1 => Rec a -> b -> Rec (opt1 :: [Char] | a)
This completely loses the aim of optional arguments: with this type, the argument 'opts' cannot have a field 'opt1' (as shown by the context 'a\opt1'). The type we want should say that 'opts' cannot have any fields except 'opt1' (though that is optional). Flex cannot express this type.
(btw, what is "Flex-like"?)
What I meant by "Flex-like" systems is that they can only extend record types by fixed fields. As well as the usual extraction and deletion of fields, I want first-class operators: (+:) :: r `Disjoint` s => r -> s -> r :+: s x +: y is the concatenation of two records x and y, under the condition that they have no fields in common r :+: s is the type of x +: y, assuming x::r and y::s (|:) :: r `Subrecord` s => s -> r -> s x |: y is the update of x by y, under the condition that every field of y is a field of x of the same type the type of x |: y is the same as the type of x The conditions on the types of these operators are important, as they catch common errors. For example, if a function 'f' has optional arguments 'opt1::x1, ... optn::xn' you want 'f {optt1 = val}' to give a type error because you've misspelled 'opt1', not simply to ignore it. In other words, you need a condition that the fields of the record argument of f are a subset of {opt1, .., optn}. These operators can be defined using type families: download the code from http://homepage.ntlworld.com/b.hilken/files/Records.hs This code would only need minimal extensions to GHC to make it completely useable.
some time ago (was that really 2 years? trac claims it was), i suggested that any record system with first-class labels needs language support for type sharing: if i import modules A and B, each of which introduces a record-label X, i need some way of telling the type system that A.X ~ B.X (Trex solved that problem by not requiring label declarations at all, but Trex labels weren't first-class objects, either).
I believe this issue is completely independent of records. Exactly the same problem would arise if the same datatype with the same constructors was defined in two different modules. To solve this we need a mechanism whereby identically defined types in different modules can be identified.
i propose to start "Records project" by composing list of requirements/applications to fulfill; we can keep it on Wiki page. this will create base for language theorists to investigate various solutions. i think they will be more motivated seeing our large interest in this extension
I am happy to contribute to this, but I am strongly biased in favour of my own records system! Barney.
Hugs.Trex> :t let f opts x = (opt1="default"|opts) in f let {...} in f :: a\opt1 => Rec a -> b -> Rec (opt1 :: [Char] | a)
This completely loses the aim of optional arguments: with this type, the argument 'opts' cannot have a field 'opt1' (as shown by the context 'a\opt1'). The type we want should say that 'opts' cannot have any fields except 'opt1' (though that is optional). Flex cannot express this type.
ok, then i misunderstood what you wanted to demonstrate with that example. but then this part doesn't seem to need any extensible records at all, in fact 'cannot have any fields except' requires non- extensibility. the standard type for optional things is Maybe thing, and if you want a record of optional things, a record with default value Nothing in each field, updated only on the fields you want to pass a value in, will do fine.
What I meant by "Flex-like" systems is that they can only extend record types by fixed fields.
thanks, i find the explanation more helpful than the name. there are already too many variations around, so unless there is a concrete implementation/specification, as in the case of Trex, Daan's system (i think he actually had several, so i should say 'Daan's scoped labels'), or Oleg's, your's and my libraries, it might be better to specify the features.
As well as the usual extraction and deletion of fields, I want first-class operators:
(+:) :: r `Disjoint` s => r -> s -> r :+: s x +: y is the concatenation of two records x and y, under the condition that they have no fields in common r :+: s is the type of x +: y, assuming x::r and y::s
this is a fairly complex operation, part of which includes a generalisation of the 'lacks' predicate in Trex to sets of labels, to catch common errors at the price of additional complexity. until i saw Daan's system, i would have agreed that this kind of disjointness/lacks guarantee was necessary for a useable record type system, but i'm no longer convinced that the additional complexity (not just in implementation, but in types) is worth it. but that is just one example of why we might need several design alternatives - no single system to please everyone all the time!-)
(|:) :: r `Subrecord` s => s -> r -> s x |: y is the update of x by y, under the condition that every field of y is a field of x of the same type the type of x |: y is the same as the type of x
i agree that something like this is useful (i should add it to my own code some time).
The conditions on the types of these operators are important, as they catch common errors. For example, if a function 'f' has optional arguments 'opt1::x1, ... optn::xn' you want 'f {optt1 = val}' to give a type error because you've misspelled 'opt1', not simply to ignore it. In other words, you need a condition that the fields of the record argument of f are a subset of {opt1, .., optn}.
again, that is achievable even with haskell's labelled fields, as it specifically rules out record extension as a programmer error. for a full record system, there are two parts of the problem: - opening closed record types to extension - closing extensible record types to prevent extension you argue that the second step is necessary, and suggest a generalisation of systems like Trex, Daan argued that a surprisingly large subset of practical problems can be addressed with the first step alone. since the second step isn't entirely for free (those 'lacks' and 'Disjoint' predicates keep piling up), there is something to be said for offering both the step 1 and the step 1+2 systems. there are several other features in which both kinds of system go beyond haskell's labelled fields, but many of those we might be able to agree on?-)
These operators can be defined using type families: download the code from http://homepage.ntlworld.com/b.hilken/files/Records.hs This code would only need minimal extensions to GHC to make it completely useable.
i still have your original announcement in my inbox!-) i just haven't got around to it yet, because i wanted to translate my own system to type functions first, and other things keep getting in the way..
.. (type sharing).. I believe this issue is completely independent of records. Exactly the same problem would arise if the same datatype with the same constructors was defined in two different modules. To solve this we need a mechanism whereby identically defined types in different modules can be identified.
indeed. record labels just raise the urgency of the issue as a real problem in programming practice.
but I am strongly biased in favour of my own records system!
who isn't?-) that is exactly why none of the systems have made it into haskell so far. and why we should allow for multiple options if we want to go any further than the numerous previous attempts. claus
| There seems to be widespread agreement that the current situation wrt | records is unacceptable, but the official GHC policy is that there are too | many good ideas to choose from - so nothing gets done! I hence humbly | propose that [http://www.cs.uu.nl/~daan/download/papers/scopedlabels.pdf] | be adapted to GHC. In my naivete, I assume that porting an existing | implementation would be much easier than starting from scratch. ... | I think this would be a BIG mistake. Whatever system GHC settles on | is almost certain to become part of the Haskell standard, and this | particular system has some deep limitations which could not be got | round without ripping it all out and starting again. That this thread has attracted so much traffic in such a short time illustrates both its importance and why we have done nothing about it in GHC for ages! It's a swamp with many use-cases, many design choices, and many local optima. (It's less clear whether there is a global optimum, but I hope there is.) I'm happy to see a Wiki page to summarise and contrast different approaches; that seems like a constructive thing to do. (Email discussions tend to evaporate and then be repeated.) A useful thing to do would be to give a series of use-cases, or examples, showing the kinds of thing one would like to be able to do. Then you can classify the approaches by what examples they can handle. Simon
http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords
I'm happy to see a Wiki page to summarise and contrast different approaches; that seems like a constructive >thing to do. (Email discussions tend to evaporate and then be repeated.) A useful thing to do would be to >give a series of use-cases, or examples, showing the kinds of thing one would like to be able to do. Then you >can classify the approaches by what examples they can handle.
i've added a link to the current version of my Data.Record (previously listed as "Poor Man's Records), which supports just about all operations that have been mentioned so far, including scoped labels, Has/Lacks, or the generalised extension-safe operations and predicates Barney prefers. and we still do not need the order on the field labels that plagues most other extensible record libraries (i'm quite amazed myself, and expect bug reports!-). i've also added the three language and implementation features i consider most important to make library-based extensible records useable in practice (none of which happen to be specific to records, btw;-). in trying to be comprehensive (mostly to explore the limitations of my approach), my code is not as simple and clean as the type families version. i don't want to duplicate the in-file comments on the wiki page for maintenance reasons, but i append them below, for the curious. claus {- poor man's extensible and concatenable records supporting both scoped and unique label records class Label label | record field labels label := value | record fields predicates: rec `Lacks` label | lacks predicate: record lacks field label rA `Disjoint` rB | record disjointness: records share no field labels scoped records operations: field :# rec | record extension rec #? label | field selection rec #- label | field removal (rec #! label) val | field update: update field label with value (rec #@ old) new | field renaming: rename existing field label old to new recA ## recB | symmetric record concatenation recA #^ recB | left-biased record field type intersection recA #^^ recB | left-biased record field label intersection recA #& recB | record projection: for each recB field, select matching recA field other record operations: field !:# rec | strict record extension: no duplicate field labels rec !#- label | strict field removal: remove existing field label from rec (rec !#! label) val | strict field update: update existing field label with value recA !## recB | symmetric disjoint record concatenation recA !#& recB | strict record projection: permute recA to match recB types: class Label l where label :: l class Has label rec lbool | label rec -> lbool class Lacks rec label class Disjoint recA recB label :: (Label l) => l (:=) :: label -> value -> label := value (:#) :: field -> record -> field :# record (!:#) :: (Lacks rec label) => (label := val) -> rec -> (label := val) :# rec (#?) :: (Select label val rec) => rec -> label -> val (#-) :: (Remove label rec rec') => rec -> label -> rec' (!#-) :: (Has label rec LTrue, Remove label rec rec') => rec -> label -> rec' (#!) :: (Remove label rec rec') => rec -> label -> value -> (label := value) :# rec' (!#!) :: (Has label rec LTrue, Remove label rec rec') => rec -> label -> value -> (label := value) :# rec' (#@) :: (Remove label1 rec rec', Select label1 val rec) => rec -> label -> label1 -> (label := val) :# rec' (##) :: (Concat recA recB recAB) => recA -> recB -> recAB (!##) :: (recA `Disjoint` recB, Concat recA recB recAB) => recA -> recB -> recAB (#^) :: (Intersect recA recB recAB) => recA -> recB -> recAB (#^^) :: (Intersect' recA recB recAB) => recA -> recB -> recAB (#&) :: (Project recA recB) => recA -> recB -> recB (!#&) :: (Project' recA recB) => recA -> recB -> recB see main at the bottom for examples of use. please let me know of any practically relevant missing operations Claus Reinke February 2006: submitted to support proposal for first class labels in Haskell' November 2007: added many more operations and predicates, replaced pairs with symbolic constructors, added strict operations -}
participants (6)
-
Barney Hilken -
Bulat Ziganshin -
Claus Reinke -
Simon Peyton-Jones -
Stefan O'Rear -
Voldermort