[Agda] Converting intrinsically typed terms

[Aaron Stump]

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/5ce45f8e/attachment.html>