4 ms·
This must be why kinds (types of types) in Haskell are a separate and less powerful thing than ordinary types?
by TazeTSchnitzel 11mo ago
This must be why kinds (types of types) in Haskell are a separate and less powerful thing than ordinary types?
- amelius 11mo agoI suspect not, because in that case Type is not a Type itself, but a Kind.
- alcidesfonseca 11mo agoI believe it to be historically true, but Dependent Haskell might change this (https://ghc.serokell.io/dh https://ghc.serokell.io/dh see unification of types and kinds). In Lean (and I believe Rocq as well), the Type of Int is Type 0, the type of Type 0 is Type 1, and so on (called universes). They all come from this restriction.
- aureianimus 11mo agoWith respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.