would support for kind equalities enable the following example?

[Carter Schonwald]

IN this case i *DO* want the GADT. (but i can't express it)

The reason is simple: one type parameter makes for a less complex API to
educate others about than 2 type parameters. And likewise for 3 vs 4. Etc
etc. Its a human factors thing :)

I do agree in this case that my "defunctionalized" type is equivalent in
type safety, and i'm happy to use it for now.




On Tue, Feb 25, 2014 at 6:50 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> My question is: why do you want Eff to be a GADT? It's true that GADTs do
> not promote (currently), which is why your first example doesn't work.
> (It's not to do with kinds, exactly, but GADTs.) But, I don't quite see a
> reason for having a GADT there -- generally, when a GADT is really useful,
> no amount of defunctionalization will be a substitute.
>
> GHC ticket #7961 is a place to make noise about this. My (with co-authors
> Stephanie Weirich and Justin Hsu) ICFP paper from last year ("System FC
> with Explicit Kind Equality") is part of the solution, and I was planning
> on submitting the other part of the solution (type inference!) for ICFP
> this year. Alas, that won't happen, but I believe I should be able to pull
> it together for the POPL deadline (July). So, there's somewhat slow but
> somewhat steady work in this direction, and I'm confident something will
> make its way into GHC before too long.
>
> Richard
>
> On Feb 24, 2014, at 11:28 PM, Carter Schonwald <carter.schonwald at gmail.com>
> wrote:
>
> > Hey all,
> >
> > I've a use case in my code where It looks like it might be an example of
> something that won't compile until we have type level GADTs
> >
> > I'm essentially writing a vector api that
> > allows certain args to be mutable, pure or "dont care". (dont care =
> that they're treated as being immutable). I'm using GADTs to model this.
> (using GADTs rather than type classes partly because I want to make sure
> type inference works out nicely, and partly to see how far i can go while
> not adding any new type classes)
> >
> > data Eff :: * -> * where
> >     Pure :: Eff ()
> >     Mut :: s -> Eff s
> >
> > data EVector  :: * -> * -> * where
> >     PureVector :: S.Vector el  -> EVector Pure el
> >     MutVector :: SM.MVector s el -> EVector (Mut s) el
> >
> > the above doesn't work because DataKinds only works at kind * currently,
> > however i can defunctionalize it to the following (while making it a tad
> less pretty)
> > and it then works
> >
> > data Eff = Pure | Mut
> >
> > data EVector  :: Eff -> * -> * -> * where
> >     PureVector :: S.Vector el  -> EVector Pure () el
> >     MutVector :: SM.MVector s el -> EVector Mut s  el
> >
> >
> > am i correct in thinking that the first example *should* be possible
> once we have fancier kind machinery (kind equalities and type level
> GADTs?)? I suspect I'll be hitting *A LOT* more examples like the above,
> and if theres any ways I can help push this along on the research or
> engineering side, I please tell me :)
> >
> > thanks!
> > -Carter
> >
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140225/db33bc29/attachment-0001.html>