[Haskell-cafe] Promoting associated data types

Alp Mestanogullari alpmestan at gmail.com
Fri Jun 26 23:09:31 UTC 2015


This all looks very interesting, thanks for the summary!
Le 26 juin 2015 17:31, "Richard Eisenberg" <eir at cis.upenn.edu> a écrit :

> A wiki page is desperately needed about this. One which I'll have to
> create after the POPL deadline (July 10).
>
> In the meantime, I'll summarize:
>
> The plan is to merge GHC's type language with its kind language. That is,
> there will be no difference, at all, between types and kinds. So any type
> family is now also a kind family, you can have unsaturated kinds, etc.
> Having merged types and kinds, it is also convenient to have (* :: *). That
> is, the type of * will be *. Other languages (Idris/Coq/Agda) avoid this
> simplification (preferring something *0 :: *1 :: *2 :: *3 :: ...) because
> they require logical consistency in order to be type-safe. Haskell doesn't
> (for reasons that are beyond the scope of this email) so our type system
> can be simpler, at least in this regard.
>
> The user-facing effects of this change should all be positive. All
> existing programs will continue to work (of course!), and I am being very
> careful not to degrade error messages. In particular, error messages will
> continue to mention types and kinds as separate entities, because this
> distinction is helpful to users. Kind parameters will remain invisible
> (implicit) in all code that compiles today.
>
> But, new, wonderful things are allowed. Like these:
>
> data Proxy k (a :: k) = Proxy    -- note the visible (explicit) kind
> parameter k!
>
> data (a :: k1) :~~: (b :: k2) where   -- heterogeneous equality
>   HRefl :: a :~~: a
>
> data G a where
>   MkG :: G Bool
> data H a (g :: G a) where
>   MkH :: a -> H a g
> foo :: H Bool 'MkG
> foo = MkH True
>
> type family KindOf (a :: k) :: *
> type instance KindOf (a :: k) = k
>
> ... and other fun stuff.
>
> Richard
>
> On Jun 26, 2015, at 4:24 AM, Alp Mestanogullari <alpmestan at gmail.com>
> wrote:
>
> Hello,
>
> Sorry to chime in, but Richard: could you expand a little bit on what your
> ongoing work there consists in and what will be possible that wasn't
> before? You got me quite curious here.
>
> Thanks!
>
> On Thu, Jun 25, 2015 at 2:31 PM, Richard Eisenberg <eir at cis.upenn.edu>
> wrote:
>
>> Hi Косырев,
>>
>> Promoting type/data families isn't a matter of safety, exactly, but a
>> matter of drastically altering the internal type system of GHC to support
>> such things. Happily, my research is all about doing so. You can expect
>> your first example `class C1 a (b :: D I)` to work in GHC 7.12. If you're
>> overly interested, my work is happening at github.com/goldfirere/ghc on
>> the `nokinds` branch. But there won't be much (any?) action there for a
>> little while as I'm working on anther project for the next few weeks.
>>
>> Your second example, though, is ill-formed: you can't have a type
>> variable of kind `D`, as `D`, by itself, isn't a kind. You could say this,
>> if you wanted, though:
>>
>> > class C1 a (b :: D a)
>>
>> Do you have an use case for this? I'm always curious to see how
>> Haskellers want to use these advanced features!
>>
>> Thanks,
>> Richard
>>
>> On Jun 25, 2015, at 2:44 AM, Kosyrev Serge <_deepfire at feelingofgreen.ru>
>> wrote:
>>
>> > Good day!
>> >
>> > DataKinds doesn't allow promotion of type/data families.
>> >
>> > However, in the specific case of associated data families -- aren't
>> > they constrained more, and sufficiently so that the following, for
>> example,
>> > could be made to work without stepping into dangerous territories:
>> >
>> > --
>> > {-# LANGUAGE DataKinds #-}
>> > {-# LANGUAGE KindSignatures #-}
>> > {-# LANGUAGE TypeFamilies #-}
>> > {-# LANGUAGE UnicodeSyntax #-}
>> >
>> > module M where
>> >
>> > class C a where
>> >    data D a ∷ *
>> >
>> > data I
>> >
>> > instance C I where
>> >    data D I
>> >
>> > class C1 a (b ∷ D I) where
>> >
>> > -- ..or, maybe, perhaps even the following:
>> >
>> > class C1 a (b ∷ D) where
>> >
>> > --
>> > respectfully,
>> > Косырев Серёга
>> > _______________________________________________
>> > Haskell-Cafe mailing list
>> > Haskell-Cafe at haskell.org
>> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> >
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>
>
>
> --
> Alp Mestanogullari
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150627/cbcbf5e0/attachment.html>


More information about the Haskell-Cafe mailing list