would support for kind equalities enable the following example?

[Richard Eisenberg]

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
> 
>