List = Set -> Set -- so now you can have List Int, List Bool, etc; in Haskell you can't express that as a type expression, so you end up talking about kinds, * -> *, so at least one can talk about parameterising on some of them, or matching the parameters.
Read literally, this means that given a type (Set), List produces a type (Set). But is it possible to have a List List? (Hence paradox akin to Russel)
The solution is to have towers of types. In Agda, Set implies Set 1. So List = Set 1 -> Set 1. But the type (Set 1 -> Set 1) is itself a Set 2 - next level universe of types. Although List is in a different universe, List Int is in the same universe as Int. Then at type level it is impossible to have List List, because List accepts an argument of type from universe 1 (Set 1), not universe 2 (Set 2, such as List).
It is possible to generalize List, though, by capturing the universe from which the argument is: List = Set a -> Set a. Now it is possible to express something like List List, but the two Lists are from two different universes.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2018-12-14 07:14 pm (UTC)Like,
List = Set -> Set -- so now you can have List Int, List Bool, etc; in Haskell you can't express that as a type expression, so you end up talking about kinds, * -> *, so at least one can talk about parameterising on some of them, or matching the parameters.
Read literally, this means that given a type (Set), List produces a type (Set). But is it possible to have a List List? (Hence paradox akin to Russel)
The solution is to have towers of types. In Agda, Set implies Set 1. So List = Set 1 -> Set 1. But the type (Set 1 -> Set 1) is itself a Set 2 - next level universe of types. Although List is in a different universe, List Int is in the same universe as Int. Then at type level it is impossible to have List List, because List accepts an argument of type from universe 1 (Set 1), not universe 2 (Set 2, such as List).
It is possible to generalize List, though, by capturing the universe from which the argument is: List = Set a -> Set a. Now it is possible to express something like List List, but the two Lists are from two different universes.