When type checking, unified universe level, and ensure it's a total order. We can buil

Based on HoTT's idea <div class="highlight highlight-source-racket notranslate pos

universe polymorphism about k HOT 2 CLOSED

dannypsnl commented on August 26, 2024

universe polymorphism

from k.

Comments (2)

dannypsnl commented on August 26, 2024

Another approach is McBride universe, which is introducing a lift operator ^. When we need a corresponding type level, use ^ to get a proper inference.

(def (map {i @ Level}
          {A B : Type i}
          [l : (List A)]
          [f : A -> B])
  : (List B)
  [nil nil]
  [(cons head l) (cons (f head) (map l f))])

Here, I use @ to notate Level since Level is not a type. When we are using map with i and i+1 expressions, use ^map to handle i+1 expression.

from k.

dannypsnl commented on August 26, 2024

Based on HoTT's idea

(def (is-prop {i @ Level} [A : Type i])
  : Type i
  (x y : A) -> x = y)
(def (×-is-prop {i j @ Level}
                {A : Type i}
                {B : Type j}
                [PA : is-prop A]
                [PB : is-prop B])
  : is-prop (A × B)
  ...)
(def (∧ {i j @ Level}
         [A : Type i]
         [B : Type j])
  : Type (lmax i j)
  A × B)

from k.

Recommend Projects