[Agda] Embedded universe polymorphic programming.

[flicky frans]

Hello. I've searched for a papers, that describe how to embed some
hierarchy of universes into a host language so you can write universe
polymorphic functions in an object language, but I haven't found
anything about this theme. So I tried to do it myself.
Instead of having only one datatype `Term', I found it useful to have
two: `Type' and `Term'. `Type' is defined like this:

mutual
  data Type : Maybe Level -> Set where
    ‵Level : Type (just zero)
    ‵Type : ∀ α -> Type (just (suc α))
    _‵ℓΠ‵_ : ∀ {mα} (A : Type mα) {k : ‵⟦ A ⟧ -> Maybe Level}
           -> (∀ x -> Type (k x)) -> Type nothing
    _‵Π‵_ : ∀ {mα mβ} -> (A : Type mα) -> (B : ‵⟦ A ⟧ -> Type mβ) ->
Type (_⊔_ <$> mα ⊛ mβ)

  ‵⟦_⟧ : ∀ {α} -> Type α -> Set
  ‵⟦ ‵Level   ⟧ = Level
  ‵⟦ ‵Type α  ⟧ = Type (just α)
  ‵⟦ A ‵ℓΠ‵ B ⟧ = (x : ‵⟦ A ⟧) -> ‵⟦ B x ⟧
  ‵⟦ A ‵Π‵ B  ⟧ = (x : ‵⟦ A ⟧) -> ‵⟦ B x ⟧

_‵ℓΠ‵_ is for functions like (λ α -> Set α), i.e. functions, where
universe dependent on a value. "Type nothing" is essentially Setω.
_‵Π‵_ captures this Setω possibility (if (A : Setω) or (B : A -> Setω)
then ((x : A) -> B x) : Setω).

`Term' is defined like this:

record Tag {α β : _} {A : Set α} (B : (x : A) -> Set β) (x : A) : Set
(α Le.⊔ β) where
  constructor tag
  field detag : B x
open Tag

mutual
  data Term : ∀ {α} -> Type α -> Set where
    ↑ : ∀ {α} {A : Type α} -> Tag ‵⟦_⟧ A -> Term A
    ⇵ : ∀ {α} (t : Type (just α)) -> Term (‵Type α)
    ℓ⇧ : ∀ {mα} {A : Type mα} {k : ‵⟦ A ⟧ -> Maybe Level} {B : (x : ‵⟦
A ⟧) -> Type (k x)}
       -> ((t : Tag ‵⟦_⟧ A ) -> Term (B (detag t))) -> Term (A ‵ℓΠ‵ B)
    ⇧ : ∀ {mα mβ} {A : Type mα} {B : ‵⟦ A ⟧ -> Type mβ}
      -> ((t : Tag ‵⟦_⟧ A ) -> Term (B (detag t))) -> Term (A ‵Π‵ B)
    _ℓ·_ : ∀ {mα} {A : Type mα} {k : ‵⟦ A ⟧ -> Maybe Level} {B : (x :
‵⟦ A ⟧) -> Type (k x)}
         -> Term (A ‵ℓΠ‵ B) -> (e : Term A) -> Term (B ⟦ e ⟧)
    _·_ : ∀ {mα mβ} {A : Type mα} {B : ‵⟦ A ⟧ -> Type mβ}
        -> Term (A ‵Π‵ B) -> (e : Term A) -> Term (B ⟦ e ⟧)

  ⟦_⟧ : ∀ {α} {A : Type α} -> Term A -> ‵⟦ A ⟧
  ⟦ ↑ t    ⟧ = detag t
  ⟦ ⇵ A    ⟧ = A
  ⟦ ℓ⇧ f   ⟧ = λ x -> ⟦ f (tag x) ⟧
  ⟦ ⇧ f    ⟧ = λ x -> ⟦ f (tag x) ⟧
  ⟦ f ℓ· x ⟧ = ⟦ f ⟧ ⟦ x ⟧
  ⟦ f · x  ⟧ = ⟦ f ⟧ ⟦ x ⟧

The Tag datatype is used to allow Agda infer more types. It's rather
ugly and makes contexts unreadable, but I haven't found any
appropriate way to achieve this inferring.
`⇧' is the lambda abstraction, _·_ is the application.
`ℓ⇧' is the universe dependent lambda abstraction, _ℓ·_ is the the
universe dependent application
`↑' is for lifting values. It could be used for the variables binded
by `⇧' and `ℓ⇧' and for the plain Agda values.
`⇵' stands, that every type (except "Type nothing", which is Setω)
could be treated as a term and so has its own type. That's how it
could be used:

  t : Term (‵Type (suc zero))
  t = ⇵ (‵Type zero)

So instead of having some lifting operator like

  ‵lift : ∀ {α} -> Type (just α) -> Type (just (suc α))

I have this triad:

  ‵Type : ∀ α -> Type (just (suc α))
  ‵⟦ ‵Type α  ⟧ = Type (just α)
  ⇵ : ∀ {α} -> (t : Type (just α)) -> Term (‵Type α)

I've tested this representation on the function, that from (s (s (s
... z))) computes (Set -> Set₁ -> Set₂ -> ... -> Setn). The plain Agda
version [1] and the version, that uses described encoding (among with
this encoding) [2].

One disadvantage is that `Type' is not strictly-positive. Maybe it's
possible to use the Universe record trick, described in the Leveling
Up Dependent Types paper, but, I think, it would be rather clumsy.
This is because there is a lifting operator in the mentioned paper,
while ‵Type constructs a universe from any level instead of just
lifting the current. So if you parametrize the `Type' datatype with
universe, then you should use `Fin' instead of `Level' to make it sure
you always go down. And `A' and `B' should lie in different universes
to make universe polymorphic programming possible, that would be a
problem too.

I have some questions:
Is this representation good?
Is it described somewhere?
Is there any other described technique for the embedded universe
polymorphic programming?

Thanks for your attention.

[1] http://lpaste.net/112044
[2] http://lpaste.net/112045