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

This all looks very interesting, thanks for the summary! Le 26 juin 2015 17:31, "Richard Eisenberg" 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 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 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

Richard Eisenberg writes:

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!

You are probably going to be disappointed -- I'm actually trying to model some kind of stereotypical OO type hierarchy. Basically, I have a known finite set of Categories (in a non-mathematical sense) of data, that I insist on modeling as a type class [1]. Each Category has a number of highly-custom Layouts capable of representing its data. Due to my irrational stubbornness, I insist on modeling them as type classes as well. I'm also trying to preserve as much user-extensibility, as I can -- through type class instancing. (Which seemingly inevitably leads to existential wrappers -- which is widely discouraged, but, for now, let's forget about this.) So, two type classes for Categories and Layouts -- this gives rise to two indices, a total of four types. For indexing the Category type class I can use a regular promoted ADT:

data CatName = Graph | Dag | Set deriving (Eq)

class Category (a ∷ CatName) where data CatX a ∷ *

..which suddenly allows to do something I couldn't figure out how to do without XDataKinds -- a simple decision procedure over a list of existentials:

data CatEntry where CatEntry ∷ Category a ⇒ (a, (CatX a)) → CatEntry

data CatAssoc where CatAssoc ∷ [CatEntry] → CatAssoc

prefer ∷ Category c ⇒ c → CatEntry → CatX c → CatX c prefer cat (CatAssoc xs) defx = case find (\(CatEntry (icat, _)) → cat == icat) xs of Just (CatEntry (icat, x)) → x Nothing → defx

Basically, DataKinds allows constraining the type class index, so that its members become directly comparable. ..however. There seems to be a need to go further, and to extend the same trick to Layouts -- remember that I need to index them as well -- so let me revisit the definition of Category (and elucidate the nature of CatX along the way):

class Category (a ∷ CatName) where data LayoutName a ∷ *

class Category cat ⇒ Layout cat (lay ∷ LayoutName cat) | lay → cat where

..which suddenly explains the meaning of 'prefer' -- a choice function for layouts:

data CatEntry where CatEntry ∷ Category a ⇒ (a, (LayoutName a)) → CatEntry

prefer ∷ Category c ⇒ c → CatEntry → LayoutName c → LayoutName c prefer cat (CatAssoc xs) deflayout = case find (\(CatEntry (icat, _)) → cat == icat) xs of Just (CatEntry (icat, lay)) → lay Nothing → deflayout

..but, of course, that can't be done yet : -) So, in the end, I'm trading off extensibility for ability to quantify over the type index. I'm not sure if I will need the quantification part in the end, but I sure as hell would like to have the choice : -) -- respectfully, Косырев Серёга -- 1. The why of type class choice is a separate question, and my reasoning is likely highly debatable. Let's assume it's aesthetics/usability, for now.

Kosyrev Serge <_deepfire@feelingofgreen.ru> writes:

So, two type classes for Categories and Layouts -- this gives rise to two indices, a total of four types.

For indexing the Category type class I can use a regular promoted ADT:

...

data CatName = Graph | Dag | Set deriving (Eq)

class Category (a ∷ CatName) where data CatX a ∷ *

..which suddenly allows to do something I couldn't figure out how to do without XDataKinds -- a simple decision procedure over a list of existentials:

...

data CatEntry where CatEntry ∷ Category a ⇒ (a, (CatX a)) → CatEntry

data CatAssoc where CatAssoc ∷ [CatEntry] → CatAssoc

prefer ∷ Category c ⇒ c → CatEntry → CatX c → CatX c prefer cat (CatAssoc xs) defx = case find (\(CatEntry (icat, _)) → cat == icat) xs of Just (CatEntry (icat, x)) → x Nothing → defx

Basically, DataKinds allows constraining the type class index, so that its members become directly comparable.

Sadly, even this doesn't fly, because:

The first argument of a tuple should have kind '*', but 'a' has kind 'CatName'.

..which doesn't really change even if I replace the tuple with a product type within the CatEntry itself. Basically GHC refuses to constrain the kind of constructor argument types beyond the granularity provided by '*'. And so I wonder if this is one restriction among those that you aim to remove.. : -) -- respectfully, Косырев Серёга

Richard Eisenberg writes:

On Jun 28, 2015, at 7:11 PM, Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:

...

Sadly, even this doesn't fly, because:

...

The first argument of a tuple should have kind '*', but 'a' has kind 'CatName'.

..which doesn't really change even if I replace the tuple with a product type within the CatEntry itself.

Basically GHC refuses to constrain the kind of constructor argument types beyond the granularity provided by '*'.

And so I wonder if this is one restriction among those that you aim to remove.. : -)

No -- this restriction leads to the best definition for tuples, in my opinion. Instead, you probably want a promoted tuple: put a ' before the open-parenthesis, and see if that works for you.

data CatEntry where CatEntry ∷ Category a ⇒ '(a, CatX a) → CatEntry

yields:

Expected a type, but ‘'(a, CatX a)’ has kind ‘(,) CatName *’ In the type ‘'(a, CatX a)’

whereas:

data CatEntry where CatEntry ∷ Category a ⇒ a → CatX a → CatEntry

yields:

Expected a type, but ‘a’ has kind ‘CatName’ In the type ‘a’

-- respectfully, Косырев Серёга