<div dir="ltr">IN this case i *DO* want the GADT. (but i can't express it)<br><br><div>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 :) <br>

<br>I do agree in this case that my "defunctionalized" type is equivalent in type safety, and i'm happy to use it for now. <br></div>
<div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 25, 2014 at 6:50 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>


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


<span class="HOEnZb"><font color="#888888"><br>
Richard<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Feb 24, 2014, at 11:28 PM, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com">carter.schonwald@gmail.com</a>> wrote:<br>
<br>
> Hey all,<br>
><br>
> 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<br>
><br>
> I'm essentially writing a vector api that<br>
> 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)<br>


><br>
> data Eff :: * -> * where<br>
>     Pure :: Eff ()<br>
>     Mut :: s -> Eff s<br>
><br>
> data EVector  :: * -> * -> * where<br>
>     PureVector :: S.Vector el  -> EVector Pure el<br>
>     MutVector :: SM.MVector s el -> EVector (Mut s) el<br>
><br>
> the above doesn't work because DataKinds only works at kind * currently,<br>
> however i can defunctionalize it to the following (while making it a tad less pretty)<br>
> and it then works<br>
><br>
> data Eff = Pure | Mut<br>
><br>
> data EVector  :: Eff -> * -> * -> * where<br>
>     PureVector :: S.Vector el  -> EVector Pure () el<br>
>     MutVector :: SM.MVector s el -> EVector Mut s  el<br>
><br>
><br>
> 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 :)<br>


><br>
> thanks!<br>
> -Carter<br>
><br>
><br>
<br>
</div></div></blockquote></div><br></div>