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