On Jan 2, 2012, at 8:05 PM, Iavor Diatchki wrote:

Hello,

On Mon, Jan 2, 2012 at 4:38 AM, Simon Peyton-Jones
<simonpj@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.

Thanks for the clear exposition! This is nearly exactly what I had in mind, and describes precisely one of the use cases I'd imagine.

The other tool I could imagine using, although for less common purposes, would be:

newtype StringC a = StringC (forall (s :: String). StringS s -> a)

runStringC :: String -> StringC a -> a
runStringC = compiler magic

With type level nats and the like, it's easy enough to write this by hand, and not terribly inefficient. But with type level strings, I'd imagine that it would be nicer to push the work to the compiler.

Cheers,
Gershom