Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I believe it to be historically true, but Dependent Haskell might change this (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.



With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: