Can't you do something like have the kind be unlifted? for instance
data Proxy (a :: #)
data Type1 :: #
data Type2 :: #
John
On Tue, Feb 7, 2012 at 12:19 PM, Douglas McClean
There are all sorts of useful functions that would otherwise require explicit type applications which we work around by passing undefined and ignoring its value. (See http://www.haskell.org/pipermail/libraries/2010-October/014742.html for a prior discussion of why this is, how the use of undefined for something that is perfectly well defined smells, and various suggestions about one day changing it.)
Examples: Data.Typeable.typeOf, Foreign.Storable.sizeOf, etc.
It seems to me that the new -XPolyKinds extension might provide a good long-term solution to statically insuring that arguments like this are always undefined and are never inspected.
If we had a library definition:
-- a kind-indexed family of empty types, Proxy :: AnyK -> * data Proxy a
then we could write things that resemble type applications such as "sizeOf @Int64". Unlike the current approach, we'd be assured that nobody tries to use the value of such a proxy in any meaningful way, since you can't pattern match it or pass a "Proxy t" in a context expecting a "t". We'd have formal documentation of which parameters are in this value-is-unused-and-only-type-matters category (which might help us erase more often?).
This is essentially the same Proxy type as in section 2.5 of the "Giving Haskell a Promotion" paper, except that by making it empty instead of isomorphic to () we end up with a type that only has one value (bottom) instead of two (Proxy and bottom), which should be a desirable property if we are trying to erase uses and forbid pattern matches and such, I think.
Adding a syntax extension (or even some TH?) to make something like "@Int64" desugar to "undefined :: Proxy Int64" would eliminate the clutter/smell from the undefineds.
Poly kinds allow us to use the same mechanism where the "undefined" parameter is a phantom type at a kind other than *. It seems to work nicely, and it cleaned up some of my code by unifying various proxy types I had made specialized at kinds like Bool.
How would you compare this to some of the proposals in the 2010 thread? Would people still prefer their fantasy-Haskell-of-the-future to include full-blown support for explicit type applications instead?
-Doug
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe