[Agda] Converting intrinsically typed terms

[William Harrison]

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, and there’s a corresponding Agda implementation. 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201106/b98ad843/attachment.html>