Useful techniques for sharing the ideas about type system implementation.

[xieyuheng]

Recently reading the book "Design Patterns" by Erich Gamma, Richard Helm, Ralph Johnson and John Vlissides.
And thinking about your teaching of NbE in davidchristiansen.dk/tutorials/nbe.
I found that in their terms, the following ideas about type system implementation,
can be called "application specific design pattern" (where our "specific application domain" is type system):

• Closure (for lexical scope)
• Bidirectional type checking (reading inference rule as type checking algorithm)
• Normalization by evaluation
• Elaboration during type checking (clear separation of roles)
• And many others...

And beside this mere "calling", their also provide a very systemic way for sharing these ideas
(which is better acquired by reading the book).

Maybe we can borrow some of their techniques to sharing those very very valuable ideas about type system implementation.

[xieyuheng]

"Design Patterns" is defined as the following:

Each pattern describes a problem which occurs over and over again in our environment,
and then describes the core of the solution to that problem, in such a way that
you can use this solution a million times over, without ever doing it the same way twice.
-- Christopher Alexander

[david-christiansen]

This might be a useful way to talk about it, but I don't think it's a bug in the Pie implementation! In any case, I'd call all those things "techniques" rather than "design patterns" - I don't see what we gain from the design pattern terminology in this specific case.