[Haskell-cafe] -XPolyKinds and undefined arguments

[John Meacham]

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
<douglas.mcclean at gmail.com> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>