would support for kind equalities enable the following example?

[Carter Schonwald]

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 at 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 <eir at cis.upenn.edu>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 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/63655d2c/attachment.html>