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