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@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@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@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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



--
Alp Mestanogullari