would support for kind equalities enable the following example?

[Carter Schonwald]

also Ive not been able to find any tickets on Trac for "heres some
motiviating example for higher kinded data kinds", happy to great a feature
request ticket motivated by this code if there sin't one :)


On Mon, 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/63ea519b/attachment.html>