Intrinsic or Extrinsic Typing for PL Metatheory?

Stream: Program verification

[Ian Sweet]

I’m wondering if there is prevailing wisdom as to whether or not one should represent typed terms in Lean4 intrinsically (terms are well-typed by construction) or extrinsically?

The prevailing wisdom is to use extrinsic typing in Roq (Coq) and intrinsic typing in Agda. As far as I know, the preference comes down to the ergonomics of performing dependent pattern matching.

Thoughts?

[Mario Carneiro]

The prevailing wisdom which I tend to dispense is in favor of extrinsic typing, although you can get away with intrinsic typing for sufficiently simple type systems

[Mario Carneiro]

IME extrinsic typing scales better to the complicated cases

[Chris Henson]

Mario Carneiro said:

The prevailing wisdom which I tend to dispense is in favor of extrinsic typing, although you can get away with intrinsic typing for sufficiently simple type systems

@Mario Carneiro Do you have examples you could share, especially of anything with some form of dependent types?

[Mario Carneiro]

Lean4lean is maybe a bit of an extreme example, but I think it is basically impossible to represent this typing judgment in intrinsic typing style

[Mario Carneiro]

with dependent types you have computation inside the indices of the inductive type, I can't imagine this working out unless you have induction-recursion

[Ian Sweet]

Thanks @Mario Carneiro , that matches my intuition as well. I appreciate the response!

[Jason Gross]

Extrinsic typing is also the way to go if you care about performance, unless you have very simple types; otherwise you will duplicate the type parameters at every node of the AST and end up with ~quadratic or worse performance in the size of your types.

[Alex Keizer]

Jason Gross said:

Extrinsic typing is also the way to go if you care about performance, unless you have very simple types; otherwise you will duplicate the type parameters at every node of the AST and end up with ~quadratic or worse performance in the size of your types.

This is something you can work around by playing tricks like Erased to ensure the type parameters are erased at runtime, at the cost of even more complexity.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am assuming the bad complexity is in kernel-typechecking the term rather than in evaluating any code, in which case Erased wouldn't help, no?