Records in Haskell

[Wolfgang Jeltsch]

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