Records in Haskell

[Iavor Diatchki]

Hello,

On Mon, Jan 2, 2012 at 4:38 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
>
> ·        I don’t know exactly what you have in mean by “the ability to
> reflect the type-level string at the value level”.
>

This can be done using singleton types in exactly the same way that it
is done on the type-nats branch.  It is useful if we want to allow
users to define interesting polymorphic functions for values of types
with type-level string literals (e.g., in the context of records, this
would allow a user to define a custom showing function that can
display the record labels).  Here is what the type-nat singletons
approach might look like for string literals:

newtype StringS (s :: String) = StringS String      -- Abstract type
for singletons (constructor not exported)

fromStringS :: StringS s -> String
fromStringS (StringS s) = s

class StringI s where
  stringS :: StringS s    -- "smart" constructor for StringS values.

Users cannot define instances for class "StingI", they are built into
GHC.  When GHC sees a constraint of the from "StringI X", for a
concrete string "X", it discharges it by making  a string evidence
value containing "X".  So, for example, the following would happen on
the GHCi prompt:

> fromStringS (stringS :: StringS "Hello")
"Hello"

The common pattern for using types in this way is something like this:

data CustomType (s :: String) = ...

tyParamString :: StringI s => CustomType s -> StringS s
tyParamString _ = stringS

showCustomType :: StringI s => CustomType s -> String
showCustomType x = "the type param is " ++ fromStringS (tyParamString
x) ++ moreStuff x

I hope this helps,
-Iavor