Records in Haskell

Simon Peyton-Jones simonpj at microsoft.com
Tue Nov 8 00:30:51 CET 2011


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 at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Wolfgang Jeltsch
|  Sent: 07 November 2011 18:31
|  To: glasgow-haskell-users at 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 at haskell.org
|  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


More information about the Glasgow-haskell-users mailing list