All geek questions in one place

What are cumulative universes and `*: *`?

In Agda exists Set n. As I understand it, it Set nextends the hierarchy of a type of type Haskell to infinite levels. That is Set 0- this is a universe of normal types, Set 1- this is a universe of normal species, Set 2- this is a universe of normal genera, etc.

On the contrary, Idris has the so-called "cumulative hierarchy of universes." It seems that for a < b, Type a: Type band universe levels are being output. But what does this mean in real-world programs? Can we not determine what works only on some higher, but not lower universe?

By the way, I know this is logically inconsistent, but what is * : *compared to the above agreed decisions?

+4
source share
1 answer

The presence of *: * in Agda corresponds to the set n: set n, and at that moment you probably just reset the levels and just set Set: Set, you can achieve this with the typetyty-type flag.

However, you should not draw a parallel between Set 0, Set 1, Set 2 ... and types, types, varieties; because the views in haskell have the intuition that they are applicable only during type checking, while you can have absolutely reliable run-time data that are of type in set 1.

, Set n Set (n + 1), , Set 0, , Set 1 Set 2. Agda Lift Level - , . .

, , " ", , - , .

, , , : https://github.com/idris-lang/Idris-dev/issues/287

Coq , , , .

+5

Source: https://habr.com/ru/post/1615689/

More articles:


All Articles