4

In Haskell, kinds (types of types) allow for some useful things such as type constructors. My question is, would there be any benefit at all to also having kinds of kinds (types of types of types), or is there nothing they could do that couldn't easily be done with just kinds and types?

LogicChains
  • 4,332
  • 2
  • 18
  • 27
  • Could you give an example of two kinds which would have a different "type³"? I mean, kinds clearly make sense (regardless of whether they're *useful*), since they allow differentiating e.g. `Maybe` from `Maybe Int`. But I can't think of two kinds which can be differentiated by their "type³". –  Mar 08 '14 at 12:52
  • It's possible that I'm misunderstanding kinds and the concept of them having a 'type' is meaningless. If so, I'll accept that as an answer. I was just assuming that, much as one can have higher order functions, one can have higher order types; (types of)^n types. – LogicChains Mar 08 '14 at 12:58
  • I really don't know if it's "meaningless", that's why I asked. Since types of anything types/kinds categorize values/types into sets, it's obvious (to me) that types of kinds should categorize kinds into sets. But I can't think of any non-trivial way to do this, i.e. any scheme that has more sets than "the set of all kinds". –  Mar 08 '14 at 13:11
  • 1
    see also http://stackoverflow.com/questions/14401689/values-types-kinds-as-an-infinite-sequence?rq=1 – Markus1189 Mar 08 '14 at 13:15
  • I don't know either, which is why I posted the question. I figured that just because I can't think of how it would work, doesn't mean it's not possible. – LogicChains Mar 08 '14 at 13:18
  • @Markus1189 Thank you, that link explains a lot. Now I'd just be interested in finding out if there's any actual use for such constructions. – LogicChains Mar 08 '14 at 13:20
  • If you have kind constructors you'd have to have some type system for the kinds to make sure they make sense. – augustss Mar 08 '14 at 13:58
  • The "kind" of a kind is called a "sort". GHC only has one at the moment, `BOX`. – David Young Mar 08 '14 at 19:54

1 Answers1

6

Ωmega has sorts all the way up. Basically, it is claimed that an infinite kind hierarchy together with appropriate GADTs is as powerful as dependent types.

Also, when trying out stuff using DataKinds, PolyKinds and the like, I sometimes feel constrained somewhat by how type constructors are not lifted to kind constructors, or that lifted kinds cannot be constrained (i.e., there are no kind classes). Ωmega seems to solve a lot of these restrictions -- unfortunately, as it is often the case, at the cost of becoming a more academic language. But I still find it easier to read compared to "real" dependently typed languages like Agda and Coq (although at least Agda does have an infinite hierarchy of sorts, too). Maybe that's because Ωmega just fits more to a Haskell mindset.

phipsgabler
  • 20,535
  • 4
  • 40
  • 60
  • Is there any relationship between infinite type hierarchy, and OOP's class inheritance? If each class were a type, then each parent class, is a type of its children? Although it seems that one can do that by creating data constructors that use previous data constructors. – CMCDragonkai Dec 16 '14 at 12:05
  • I wouldn't say so, no. Sorts are _types of types (of types of...)_, which is a different story than subtypes. They're more similar to class reification, IMO. E.g., in Python, each value has a class (= type); each class has a [metaclass](http://stackoverflow.com/q/100003/1346276) (~ kind, but not quite). By default, that metaclass is `type` -- but you can also have your own metaclasses (~ other kinds). Although, that's not a quite exact analogy, I'd say. In general, subtyping systems and the ones in functional languages are quite orthogonal. – phipsgabler Dec 16 '14 at 13:21
  • Sure subtyping and infinite type hierarchy has differences, but the general idea seems the same. Implemention wise classes seems to have specific functionality that happens in the value universe, so I'm not sure how to reconcile that. – CMCDragonkai Dec 16 '14 at 13:36
  • I think I don't exactly get your point, but for me, the difference is the following: Subtyping defines a relation between objects in the same universe, whereas sorts form a hierarchy of universes on different levels. So you can construct a class from aggregating other classes, because they're on the same level -- but you can't (arbitrarily) "combine" things of different sorts (not even on the same level!), since they live in different "conceptual universes". – phipsgabler Dec 16 '14 at 13:57
  • Yea I was thinking about that over the night, and so that makes sense too. I was just trying to think that if you were in a language that didn't support universes, then you could kind of simulate that idea through subtyping. But the restriction of manipulating certain classes of objects would be up to the programmer and not guaranteed by the compiler. So the use of these infinite universes, is that each level up specifies the semantics of the level below it. Just like an integer specifies what it means to do `1+1`, something above integer specifies what the integer itself means right? – CMCDragonkai Dec 17 '14 at 04:22
  • That's probably more coherent to my understanding, yes. Kinds restrict the set of values to choose from in genereral (i.e., `*` and `Nat` in `data Vec :: Nat -> * -> *`, and subtypes define a subset _within_ a kind (e.g. passing `Int` to `Objekt -> Int` is admissible). – phipsgabler Dec 17 '14 at 08:20