[Agda] Converting intrinsically typed terms

[Conal Elliott]

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