[Agda] Converting intrinsically typed terms

[Thorsten Altenkirch]

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.

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<mailto: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<mailto: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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201106/28581ab2/attachment.html>