[TYPES] Congruence rules vs frames

[Philip Wadler]

Most mechanised formulations of reduction systems, such as those found in
Software Foundations or in Programming Language Foundations in Agda, use
one congruence rule for each evaluation context:

  ξ-·₁ : ∀ {L L′ M}
    → L —→ L′
      -----------------
    → L · M —→ L′ · M

  ξ-·₂ : ∀ {V M M′}
    → Value V
    → M —→ M′
      -----------------
    → V · M —→ V · M′

One might instead define frames that specify evaluation contexts and have a
single congruence rule.

data Frame : Set where
  □·                   : Term → Frame
  ·□                   : (V : Term) → Value V → Frame

_[_] : Frame → Term → Term
(□· M) [ L ]                        =  L · M
(·□ V _) [ M ]                    =  V · M

 ξ : ∀ F {M M′}
    → M —→ M′
      -------------------
    → F [ M ] —→ F [ M′ ]

However, one rapidly gets into problems. For instance, consider the proof
that types are preserved by reduction.

preserve : ∀ {M N A}
  → ∅ ⊢ M ⦂ A
  → M —→ N
    ----------
  → ∅ ⊢ N ⦂ A
...
preserve (⊢L · ⊢M)  (ξ (□· _) L—→L′)  =  (preserve ⊢L L—→L′) · ⊢M
preserve (⊢L · ⊢M)  (ξ (·□ _ _) M—→M′)  =  ⊢L · (preserve ⊢M M—→M′)
...

The first of these two lines gives an error message:

I'm not sure if there should be a case for the constructor ξ,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  F [ M ] ≟ L · M₁
  F [ M′ ] ≟ N
when checking that the pattern ξ (□· _) L—→L′ has type L · M —→ N

And the second provokes a similar error.

This explains why so many formulations use one congruence rule for each
evaluation context. But is there a way to make the approach with a single
congruence rule work? Any citations to such approaches in the literature?

Thank you for your help. Go well, -- P



.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. https://urldefense.com/v3/__http://homepages.inf.ed.ac.uk/wadler/__;!!IBzWLUs!EIYnAk7pSQVJFwJaONabTO_JqymiXUpQnVqKBbbpFSiJ_flduU6cOIjOgNtqMC_UDbn50dUukp4$ 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20211009/40248446/attachment-0001.ksh>