[Agda] Converting intrinsically typed terms

[Conal Elliott]

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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201106/9b74f6e1/attachment.html>