I'm interested in type-level strings myself. I'm using an
approximation in order to enrich the instant-generics-style reflection
of data type declarations with a sensitivity to constructor names. For
example, this lets me automatically convert between many the
similarly-named constructors of related data types (e.g. pipeline of
ASTs in a compiler).
Is there any existing developments regarding type-level strings? I
have (arbitrarily) taken the approach of promoting the cereal library
to the type-level, encoding strings that way, and working from there
(ultimately inspired by Kiselyov and Chan's implicit configurations
paper). It's certainly not perfect, but it's all I need for the
functionality I've been chasing so far.
In regard to Labels versus Atom, etc., in my use case of converting
between similar datatypes, it would be very reasonable to eventually
add/remove prefixes/suffixes from these type-level reifications of
constructor names. If type-level strings are not implemented as lists
of characters, I would still like access to a comparable API. Perhaps
an isomorphism?
Thanks for your time,Nick
PS — I suspect the "reflect to value-level" idea was something along
the lines of automatically providing a function @stringVal :: forall
(a :: Label). a -> String@.
On Mon, Jan 2, 2012 at 6:38 AM, Simon Peyton-Jones
It seems to me that there's only one essential missing language feature, which is appropriately-kinded type-level strings (and, ideally, the ability to reflect these strings back down to the value level). Given that, template haskell, and the HList bag of tricks, I'm confident that a fair number of elegant records packages can be crafted. Based on that experience, we can then decide what syntactic sugar would be useful to elide the TH layer altogether.
I think we can do this part without much trouble, once the dust has settled on -XPolyKinds. It certainly fits with all the work we’ve been doing recently on the kind system. I agree that it’s a fairly basic requirement; for example, it’s also assumed by http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields
Specifically
· Allow String as a new kind
· Now you can define classes or types with kinds like
MyCls :: String -> a -> Constraint
T :: String -> *
· Provide type-level string literals, so that “foo” :: String
Open questions:
· Is String (at the kind level) a synonym for [Char]? I’m inclined *not* to do this initially, because it would require us to have promoted character literals too -- and the implementation of record labels as strings of type-level cons-cells is not going to be efficient.
· If String is not a kind level synonym for [Char], maybe it should have a different name. For example, “foo” :: Label? Or Atom? After all, if it doesn’t behave like a Haskell string it probably should not have the same name.
· Are there any operations over Labels?
· I don’t know exactly what you have in mean by “the ability to reflect the type-level string at the value level”.
Simon
From: Gershom Bazerman [mailto:gershomb@gmail.com] Sent: 31 December 2011 19:12 To: Simon Peyton-Jones Cc: Greg Weber; glasgow-haskell-users@haskell.org
Subject: Re: Records in Haskell
On Dec 31, 2011, at 1:28 PM, Simon Peyton-Jones wrote:
The trouble is that I just don't have the bandwidth (or, if I'm honest, the motivation) to drive this through to a conclusion. And if no one else does either, perhaps it isn't *that* important to anyone. That said, it clearly is *somewhat* important to a lot of people, so doing nothing isn't very satisfactory either.
Usually I feel I know how to move forward, but here I don't.
Simon
It seems to me that there's only one essential missing language feature, which is appropriately-kinded type-level strings (and, ideally, the ability to reflect these strings back down to the value level). Given that, template haskell, and the HList bag of tricks, I'm confident that a fair number of elegant records packages can be crafted. Based on that experience, we can then decide what syntactic sugar would be useful to elide the TH layer altogether.
Beyond that, it would really help namespacing in general to appropriately extend the module system to allow multiple modules to be declared within a single file -- or, better yet, "submodules". I know that this introduces a few corner cases that need to be thought through -- what happens with overlapping declarations, for example. But I tend to think the path here is relatively straightforward and obvious, and the added expressive power should make namespacing issues much more tractable. Like the type-level strings proposal, this isn't about implementing records as such -- rather, it's about generally extending the expressive power of the language so that record systems--among other things--are easier to write.
Cheers,
Gershom
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users