[Agda] Converting intrinsically typed terms

[Harley D. Eades III]

We are all awaiting these details. :-)

Harley

On Fri, Nov 6, 2020 at 7:21 PM William Harrison <
william.lawrence.harrison at gmail.com> wrote:

> Who am I kidding? I want to hear the details, too.
>
> Sent from my iPad
>
> On Nov 6, 2020, at 7:15 PM, Conal Elliott <conal at conal.net> wrote:
>
> 
> I'd love to hear more as well.
>
> On Fri, Nov 6, 2020 at 3:24 PM Aaron Stump <aaron-stump at uiowa.edu> wrote:
>
>>
>> On Fri, Nov 6, 2020 at 5:53 AM Thorsten Altenkirch <
>> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>
>>> I don’t agree that one should use CCCs because CCCs introduce the
>>> misleading identification of contexts and types. It is preferable to use a
>>> contextual version of CCCs, basically Categories with Families for simple
>>> types. I can provide more details if there is interest.
>>>
>>
>> Yes, please!
>>
>> Aaron
>>
>>
>>
>>>
>>> Thorsten
>>>
>>>
>>>
>>> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Conal
>>> Elliott <conal at conal.net>
>>> *Date: *Wednesday, 4 November 2020 at 16:52
>>> *To: *"rozowski w.k. (wkr1u18)" <wkr1u18 at soton.ac.uk>
>>> *Cc: *Agda users <agda at lists.chalmers.se>
>>> *Subject: *Re: [Agda] Converting intrinsically typed terms
>>>
>>>
>>>
>>> Hi Wojciech. Since you are starting with the STLC, you might find it
>>> helpful to factor compilation through cartesian closed categories (CCCs).
>>> Then you can use a standard translation for the first part (STLC→CCCs) and
>>> define the rest as familiar algebraic operations: identity, sequential
>>> composition, projections, parallel composition, etc, all with standard laws
>>> they must satisfy (associativity of composition etc). I’ve described such
>>> an approach in a paper draft
>>> <http://conal.net/papers/calculating-compilers-categorically/>, and
>>> there’s a corresponding Agda implementation
>>> <https://github.com/conal/calculating-compilers-agda>. Best of luck! -
>>> Conal
>>>
>>>
>>>
>>> On Mon, Nov 2, 2020 at 2:56 AM rozowski w.k. (wkr1u18) <
>>> wkr1u18 at soton.ac.uk> wrote:
>>>
>>> Hello everyone!
>>>
>>>
>>>
>>> I'm relatively new to Agda (recently just went through first two Parts
>>> of PLFA), so I'm sorry if my question is obvious or don't appropriate for
>>> this forum.
>>>
>>> I am writing to ask for any advice how to formalise type correct
>>> transformations between intrinsically typed terms.
>>>
>>>
>>>
>>> Currently, while doing my BSc thesis, I am working on formalizing a
>>> paper about framework for specifying abstract machines, as a series of
>>> transforms between STLC and intermediate languages including combinators
>>> (eg. pushₛ to push on stack, ƛₛ to pop from stack and bind to variable,
>>> _∘_ to perform sequencing). Each intermediate language adds a pair of
>>> push and lambda combinators to work with different parts of machine - eg.
>>> environments, continuations. Each of the intermediate languages is a subset
>>> of the following ones.
>>>
>>>
>>>
>>> The type rules (and way of building terms - because intrinsic typing)
>>> for those combinators, are:
>>>
>>>   pushₛ_ : ∀ {Γ A}
>>>
>>>     → Γ ⊢ A
>>>
>>>       -----
>>>
>>>     → Γ ⊢ Rₛ A
>>>
>>>
>>>
>>>   ƛₛ_  : ∀ {Γ A B}
>>>
>>>     → Γ , A ⊢ B
>>>
>>>       ---------
>>>
>>>     → Γ ⊢ A ⇒ₛ B
>>>
>>>
>>>
>>>   _∘_ : ∀ {Γ A B}
>>>
>>>     → Γ ⊢ Rₛ A
>>>
>>>     → Γ ⊢ A ⇒ₛ B
>>>
>>>       ---------
>>>
>>>     → Γ ⊢ B
>>>
>>>
>>>
>>> (Rs A is just annotated type for something of type A being stored on
>>> stack)
>>>
>>>
>>>
>>> I managed to use the PLFA formalism and add typing rules for lambda
>>> calculus extended with pair of combinators for the stack and sequencing
>>> operators. The extended semantics now include:
>>>
>>>
>>>
>>>   ξ-∘ₛ₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ₛ B} {M : Γ ⊢ Rₛ A}
>>>
>>>     → L —→ L′
>>>
>>>       ---------------
>>>
>>>     → M ∘ L —→ M ∘ L′
>>>
>>>
>>>
>>>   ξ-∘ₛ₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ₛ B} {M M′ : Γ ⊢ Rₛ A}
>>>
>>>     → Value V
>>>
>>>     → M —→ M′
>>>
>>>       ---------------
>>>
>>>     → M ∘ V —→ M′ ∘ V
>>>
>>>
>>>
>>>   β-∘ₛ :  ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
>>>
>>>       -------------------
>>>
>>>     →  (pushₛ W) ∘ (ƛₛ N) —→ N [ W ]
>>>
>>>
>>>
>>> The part I am having trouble with is formalising a transform between
>>> terms from STLC to this intermediate language. One of the transforms
>>> introduced by this paper is:
>>>
>>>
>>>
>>> Va : Λ→Λs
>>>
>>>
>>>
>>> Va [[x]] = pushs x
>>>
>>> Va [[λx.E]] = pushs (λsx.Va [[E]] )
>>>
>>> Va [[E1 E2]] = Va [[E2]] o Va [[E1]] o app with app = λsf.f
>>>
>>>
>>>
>>>  As the STLC is the subset of the first combinator language, I just
>>> defined transform from the language to itself: I defined map between types,
>>> contexts and variables lookup
>>>
>>>
>>>
>>> Va-type : Type → Type
>>>
>>> Va-type (x ⇒ x₁) = Rₛ ( (Va-type x) ⇒ₛ (Va-type x₁) )
>>>
>>> Va-type `ℕ  = Rₛ `ℕ
>>>
>>> Va-type (Rₛ x)  = Rₛ (Va-type x)
>>>
>>> Va-type (x ⇒ₛ x₁)  = (Va-type x) ⇒ₛ (Va-type x₁)
>>>
>>>
>>>
>>> Va-context : Context → Context
>>>
>>> Va-context ∅ = ∅
>>>
>>> Va-context (x , x₁) =  ( Va-context x , Va-type x₁ )
>>>
>>>
>>>
>>> Va-var : ∀ {Γ A} → Γ ∋ A → ((Va-context Γ) ∋ (Va-type A))
>>>
>>> Va-var Z = Z
>>>
>>> Va-var (S x) = S Va-var x
>>>
>>>
>>>
>>> And the problematic part is declaring the transform between terms:
>>>
>>>
>>>
>>> Va : ∀ {Γ A} → Γ ⊢ A → (Va-context Γ) ⊢ (Va-type A)
>>>
>>> Va (` x) = ` Va-var x
>>>
>>> Va (ƛ x) =  pushₛ (ƛₛ Va x)
>>>
>>>
>>>
>>> -- Here is the hole I cannot come up with filling it
>>>
>>> Va {Γ} (x · x₁) = (pushₛ (Va x₁)) ∘ ((pushₛ (Va x)) ∘ (ƛₛ {!!} ))
>>>
>>> Va `zero = pushₛ `zero
>>>
>>> Va (`suc x) = pushₛ (`zero) -- paper doesn't provide any notion for
>>> dealing with sucessors of Nats - currently left like this to pass the
>>> typecheck
>>>
>>>
>>>
>>> -- Combinators from intermediate language are mapped to itself
>>>
>>> Va (pushₛ x) = pushₛ Va x
>>>
>>> Va (ƛₛ x) = ƛₛ Va x
>>>
>>> Va (x ∘ x₁) = Va x ∘ Va x₁
>>>
>>>
>>>
>>> The only bit, I am not able to formalise is the "app" combinator, as
>>> standard lookup using #_ doesnt work when mapping between terms.
>>>
>>> Do you happen to have any advice for me, how to tackle such
>>> transformations? Is there anything I am missing in my way of formalising?
>>> Did any of you worked with type correct transformations of terms in de
>>> Brujin typed terms and have any tips for me?
>>>
>>>
>>>
>>> I would be most grateful if I could hear back from you!
>>>
>>>
>>>
>>> Best,
>>>
>>> Wojciech
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>> This message and any attachment are intended solely for the addressee
>>> and may contain confidential information. If you have received this
>>> message in error, please contact the sender and delete the email and
>>> attachment.
>>>
>>> Any views or opinions expressed by the author of this email do not
>>> necessarily reflect the views of the University of Nottingham. Email
>>> communications with the University of Nottingham may be monitored
>>> where permitted by law.
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201201/65e6eb6f/attachment.html>