[Haskell-cafe] -XPolyKinds and undefined arguments

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120207/b345699f/attachment.htm>