[Agda] Embedded universe polymorphic programming.

[Vladimir Voevodsky]

This is about a system with explicit functions between universes where I also arrived 
at the conclusion that it is much more efficient to keep terms and types separate:

https://github.com/vladimirias/Universe_Polymorphic_Type_System

V.




On Oct 6, 2014, at 7:58 AM, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:

> Hi.
> 
> The following paper may be of interest:
> 
> https://who.rocq.inria.fr/Ali.Assaf/research/coc-explicit-subtyping.pdf
> 
> Best regards,
> 
> Frédéric Blanqui.
> 
> Le 04/10/2014 12:45, flicky frans a écrit :
>> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
Url : http://lists.chalmers.se/pipermail/agda/attachments/20141006/0ceb1716/signature.bin