[Haskell-cafe] Kind product

[Richard Eisenberg]

On Nov 30, 2014, at 5:38 PM, Gautier DI FOLCO <gautier.difolco at gmail.com> wrote:
> 
> Thanks for your answer.
> I don't see why it's closer to dependent typing, can you give me some hints?

One of the steps to dependent typing in Haskell (as my research partners and I see it) is making the type level and the kind level uniform -- that is, to stop distinguishing types from kinds. Thus, since we have type families, we must have kind families as well. The uniformity between the levels makes it easier to promote more data constructors to type constructors.

I agree with the implied opinion that kind families have little to do with types depending on values.

Richard