[Agda] Embedded universe polymorphic programming.

[Andreas Abel]

Larry Diehl http://www.larrytheliquid.com/
had a paper 'Leveling Up Dependent Types' at DTP 2013, see

   https://dl.dropboxusercontent.com/u/31465260/drafts/leveling-up.pdf

On 04.10.2014 12:45, flicky frans wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/