-XPolyKinds and undefined arguments
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
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
participants (2)
-
Douglas McClean -
John Meacham