<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>On Jan 2, 2012, at 8:05 PM, Iavor Diatchki wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>Hello,<br><br>On Mon, Jan 2, 2012 at 4:38 AM, Simon Peyton-Jones<br><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br><blockquote type="cite"><br></blockquote><blockquote type="cite">· I don’t know exactly what you have in mean by “the ability to<br></blockquote><blockquote type="cite">reflect the type-level string at the value level”.<br></blockquote><font class="Apple-style-span" color="#006312"><br></font>This can be done using singleton types in exactly the same way that it<br>is done on the type-nats branch. It is useful if we want to allow<br>users to define interesting polymorphic functions for values of types<br>with type-level string literals (e.g., in the context of records, this<br>would allow a user to define a custom showing function that can<br>display the record labels). Here is what the type-nat singletons<br>approach might look like for string literals:<br><br>newtype StringS (s :: String) = StringS String -- Abstract type<br>for singletons (constructor not exported)<br><br>fromStringS :: StringS s -> String<br>fromStringS (StringS s) = s<br><br>class StringI s where<br> stringS :: StringS s -- "smart" constructor for StringS values.<br></div></blockquote></div><br><div>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.</div><div><br></div><div>The other tool I could imagine using, although for less common purposes, would be:</div><div><br></div><div>newtype StringC a = StringC (forall (s :: String). StringS s -> a)</div><div><br></div><div>runStringC :: String -> StringC a -> a</div><div>runStringC = compiler magic</div><div><br></div><div>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.</div><div><br></div><div>Cheers,</div><div>Gershom</div></body></html>