Great question Mike!

Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently, I think the 'right' (mathematical!) way to understand these 'let-bindings' (which I think is not the right way to see them, at least on a first cut) is via context morphisms, together with a suitable notion, for pattern matching, of when a collection of context morphisms 'covers' another (in the Grothendieck topology/crible sense).

From this point of view, the contexts in which each RHS of the evolving case tree are distinct (they just look as though they 'share' bindings), but they are all suitably correlated by the morphisms between them which furnish the 'let'-like instantiations. The 'evolving' nature of the pattern analysis also fits well with contexts-and-morphisms as a mathematically satisfactory account of 'stages of knowledge' along more traditional Brouwerian/sheaf-theoretic lines.

Whether or not any of our implementations actually realises this conceptual analysis is another matter.

Great question Mike!

Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently, I think the 'right' (mathematical!) way to understand these 'let-bindings' (which I think is not the right way to see them, at least on a first cut) is via context morphisms, together with a suitable notion, for pattern matching, of when a collection of context morphisms 'covers' another context (in the Grothendieck topology/crible sense).

From this point of view, the contexts in which each RHS of the evolving case tree are well typed are distinct (they just look as though they 'share' bindings), but they are all suitably correlated by the morphisms between them which furnish the 'let'-like instantiations. The 'evolving' nature of the pattern analysis also fits well with contexts-and-morphisms as a mathematically satisfactory account of 'stages of knowledge' along more traditional Brouwerian/sheaf-theoretic lines.

Whether or not any of our implementations actually realises this conceptual analysis is another matter.

Great question Mike!

Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently, I think the 'right' (mathematical!) way to understand these 'let-bindings' (which I think is not the right way to see them, at least on a first cut) is via context morphisms, together with a suitable notion, for pattern matching, of when a collection of context morphisms 'covers' another (in the Grothendieck topology/crible sense).

From this point of view, the contexts in which each RHS of the evolving case tree are distinct (they just look as though they 'share' bindings), but they are all suitably correlated by the morphisms between them which furnish the 'let'-like instantiations.

Whether or not any of our implementations actually realises this conceptual analysis is another matter.

Great question Mike!

Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently, I think the 'right' (mathematical!) way to understand these 'let-bindings' (which I think is not the right way to see them, at least on a first cut) is via context morphisms, together with a suitable notion, for pattern matching, of when a collection of context morphisms 'covers' another (in the Grothendieck topology/crible sense).

From this point of view, the contexts in which each RHS of the evolving case tree are distinct (they just look as though they 'share' bindings), but they are all suitably correlated by the morphisms between them which furnish the 'let'-like instantiations. The 'evolving' nature of the pattern analysis also fits well with contexts-and-morphisms as a mathematically satisfactory account of 'stages of knowledge' along more traditional Brouwerian/sheaf-theoretic lines.

Whether or not any of our implementations actually realises this conceptual analysis is another matter.