Am Montag, den 07.11.2011, 17:53 +0000 schrieb Barney Hilken:
Here is my understanding of the current state of the argument:
Instead of Labels, there will be a new kind String, which is not a subkind of *, so its elements are not types. The elements of String are strings at the type level, written just like normal strings. If you want labels, you can define them yourself, either empty:
data Label (a :: String)
or inhabited
data Label (a :: String) = Label
these definitions give you a family of types of the form Label "name", in the first case empty (except for undefined), in the second case inhabited by a single element (Label :: Label "name")
There are several similar proposals for extensible records defined using labels, all of which (as far as I can see) could be defined just as easily using the kind String.
The problem with this approach is that different labels do not have different representations at the value level. In my record system, I use label definitions like the following ones: data MyName1 = MyName1 data MyName2 = MyName2 This allows me to pattern match records, since I can construct record patterns that contain fixed labels: X :& MyName1 := myValue1 :& MyName2 := myValue2 I cannot see how this could be done using kind String. Do you see a solution for this? A similar problem arises when you want to define a selector function. You could implement a function get that receives a record and a label as arguments. However, you could not say something like the following then: get myRecord MyName1 Instead, you would have to write something like this: get myRecord (Label :: MyName1) Whis is ugly, I’d say. Yes, Simon’s proposal contains syntactic sugar for selection, but this sugar might not be available for other record systems, implemented in the language. The situation would be different if we would not only have kind String, but also an automatically defined GADT that we can use to fake dependent types with string parameters: data String :: String -> * -- automatically defined A string literal "abc" would be of type String "abc" then. However, I am not sure at the moment, if this would solve all the above problems. Best wishes, Wolfgang
The problem with this approach is that different labels do not have different representations at the value level.
I think this is an advantage, because it means you don't have to carry this stuff about at runtime.
This allows me to pattern match records, since I can construct record patterns that contain fixed labels:
X :& MyName1 := myValue1 :& MyName2 := myValue2
I cannot see how this could be done using kind String. Do you see a solution for this?
A similar problem arises when you want to define a selector function. You could implement a function get that receives a record and a label as arguments. However, you could not say something like the following then:
get myRecord MyName1
Instead, you would have to write something like this:
get myRecord (Label :: MyName1)
Just define a constant myName1 = Label :: MyName1 for each label you actually use, and you can use it in both get and pattern matching Barney.
Am Montag, den 07.11.2011, 21:41 +0000 schrieb Barney Hilken:
The problem with this approach is that different labels do not have different representations at the value level.
I think this is an advantage, because it means you don't have to carry this stuff about at runtime.
This allows me to pattern match records, since I can construct record patterns that contain fixed labels:
X :& MyName1 := myValue1 :& MyName2 := myValue2
I cannot see how this could be done using kind String. Do you see a solution for this?
A similar problem arises when you want to define a selector function. You could implement a function get that receives a record and a label as arguments. However, you could not say something like the following then:
get myRecord MyName1
Instead, you would have to write something like this:
get myRecord (Label :: MyName1)
Just define a constant
myName1 = Label :: MyName1
for each label you actually use, and you can use it in both get and pattern matching
You cannot use such a constant in a pattern. You need a data constructor if you want to use pattern matching. Best wishes, Wolfgang
On Mon, Nov 07, 2011 at 08:31:04PM +0200, Wolfgang Jeltsch wrote:
The problem with this approach is that different labels do not have different representations at the value level. In my record system, I use label definitions like the following ones:
data MyName1 = MyName1
data MyName2 = MyName2
Instead of class Has (r :: *) (f :: String) (t :: *) where (as on the wiki), would it be possible to have something like class Has (r :: *) (ft :: *) (f :: ft) (t :: *) where (where ft stands for field type)? This could also solve the representation-hiding problem: foo.field would use the string "field" as the field name, as in the proposal on the wiki page. But foo.Field (capital first letter) would use the constructor Field that is in scope. If you don't want to export the field getter then capitalise the first letter and don't export the constructor. Thanks Ian
Ian said....
class Has (r :: *) (ft :: *) (f :: ft) (t :: *) where (where ft stands for field type)?
class Has (r :: *) (f :: ft) (t :: *) where would be my understanding of how it would be phrased under the current polymorphic kind system. This could also solve the representation-hiding problem:
foo.field would use the string "field" as the field name, as in the proposal on the wiki page.
But foo.Field (capital first letter) would use the constructor Field that is in scope. If you don't want to export the field getter then capitalise the first letter and don't export the constructor.
I like it. Between that and using Proxy rather than type application perhaps everyone can be made happy. -Edward
Wolfgang Is there a wiki page giving a specific, concrete design for the proposal you advocate? Something at the level of detail of http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields? I am unsure whether you regard it as an alternative to the above, or something that should be done as well. And if the former, how does it relate to the challenge articulated on http://hackage.haskell.org/trac/ghc/wiki/Records, namely how to make Haskell's existing named-field system work better? Thanks Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Wolfgang Jeltsch | Sent: 07 November 2011 18:31 | To: glasgow-haskell-users@haskell.org | Subject: Re: Records in Haskell | | Am Montag, den 07.11.2011, 17:53 +0000 schrieb Barney Hilken: | > Here is my understanding of the current state of the argument: | > | > Instead of Labels, there will be a new kind String, which is not a | > subkind of *, so its elements are not types. The elements of String | > are strings at the type level, written just like normal strings. If | > you want labels, you can define them yourself, either empty: | > | > data Label (a :: String) | > | > or inhabited | > | > data Label (a :: String) = Label | > | > these definitions give you a family of types of the form Label "name", | > in the first case empty (except for undefined), in the second case | > inhabited by a single element (Label :: Label "name") | > | > There are several similar proposals for extensible records defined | > using labels, all of which (as far as I can see) could be defined just | > as easily using the kind String. | | The problem with this approach is that different labels do not have | different representations at the value level. In my record system, I use | label definitions like the following ones: | | data MyName1 = MyName1 | | data MyName2 = MyName2 | | This allows me to pattern match records, since I can construct record | patterns that contain fixed labels: | | X :& MyName1 := myValue1 :& MyName2 := myValue2 | | I cannot see how this could be done using kind String. Do you see a | solution for this? | | A similar problem arises when you want to define a selector function. | You could implement a function get that receives a record and a label as | arguments. However, you could not say something like the following then: | | get myRecord MyName1 | | Instead, you would have to write something like this: | | get myRecord (Label :: MyName1) | | Whis is ugly, I’d say. | | Yes, Simon’s proposal contains syntactic sugar for selection, but this | sugar might not be available for other record systems, implemented in | the language. | | The situation would be different if we would not only have kind String, | but also an automatically defined GADT that we can use to fake dependent | types with string parameters: | | data String :: String -> * -- automatically defined | | A string literal "abc" would be of type String "abc" then. However, I am | not sure at the moment, if this would solve all the above problems. | | Best wishes, | Wolfgang | | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Am Montag, den 07.11.2011, 23:30 +0000 schrieb Simon Peyton-Jones:
Wolfgang
Is there a wiki page giving a specific, concrete design for the proposal you advocate? Something at the level of detail of http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields?
Well, I don’t propose a new record system as a language feature. Instead, I’ve implemented a record system as a library. The paper at http://www.informatik.tu-cottbus.de/~jeltsch/research/ppdp-2010-paper.pdf describes this in detail, and the records package at http://hackage.haskell.org/package/records is the actual library. My stance is that it is possibly better if we do not try to include a one-size-fits-it-all record system into the language, but if the language provided support for basic things that almost all record system *libraries* would need. In my opinion, there is at least one such thing that should get language support: field labels. There is already the proposal at http://hackage.haskell.org/trac/haskell-prime/wiki/FirstClassLabels for first-class field labels.
I am unsure whether you regard it as an alternative to the above, or something that should be done as well. And if the former, how does it relate to the challenge articulated on http://hackage.haskell.org/trac/ghc/wiki/Records, namely how to make Haskell's existing named-field system work better?
I don’t think that everyone should use my record system. I see it as one member of a family of reasonable record systems. My intention, when developing my record system, was not to make the existing system better, since I needed quite a lot of advanced features that anything near Haskell’s existing record system couldn’t give me. So I started something completely new.
Thanks
Simon
Best wishes, Wolfgang
My stance is that it is possibly better if we do not try to include a one-size-fits-it-all record system into the language, but if the language provided support for basic things that almost all record system *libraries* would need.
Agreed. To the extent that such libraries could be improved by sugar, a general solution for such library-specific sugar might be sought. But the record libraries tended to be quite useful, modulo (of the top of my head, probably incomplete): - first-class labels I wonder whether the recent lifting of values into the type-level (towards typed types) offers sufficient convenience? Do they address the sharing issue? Haven't had the time to read yet; - soundness All the type-class based libraries work in the grey area of things that GHC allows for pragmatic reasons and that Hugs disallowed for soundness reasons; the success of GHC shows that Hugs was too careful, but I'd prefer if GHC either acquired safe features that could replace the current interplay of FDs and Overlapping Instances, or if someone proved the set of features in use safe; - optimization there is no reason why record libraries need to be slow to run, and the compilation time increases needed to make it so might be optimized away, too; but someone needs to do the work, or record field selection will -naively and in overloaded style- involve linear lookup; If these were to be addressed, record libraries would be more widely acceptable than they are today (though I recommend playing with the ones that exist, and reporting on their strengths and weaknesses in practice); initially, everyone would use their favorite, but I am hopeful that a common API would emerge eventually, from use. We haven't had any luck agreeing on a common API before use, and none of the many good proposals have managed to sway everyone, which is why I agree on not settling on a single design just yet - just pave the road for wider adoption of record libraries). Back to the side-line for me;-) Claus
participants (6)
-
Barney Hilken -
Claus Reinke -
Edward Kmett -
Ian Lynagh -
Simon Peyton-Jones -
Wolfgang Jeltsch