Reid Just helped me whack out a solution, it involve something i didn't even know was possible in haskell data Eff :: *-> * where Pure :: Eff s Mut :: s -> Eff s data EVector :: Eff * -> * -> * where PureVector :: S.Vector el -> EVector Pure el MutVector :: SM.MVector s e -> EVector (Mut s) el (the surprising thing was the Eff *, i didn't know we could do that!) this type checks, but it can be made simpler still! data Eff s where Pure :: Eff s Mut :: s -> Eff s data EVector s el where PureVector :: S.Vector el -> EVector Pure el MutVector :: SM.MVector s e -> EVector (Mut s) el :) that said, I do have some more interesting stuff in the works where I hope to make use of kind level gadts, so i look forward to finding out how that shakes out! -Carter On Tue, Feb 25, 2014 at 10:23 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

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