I agree. If only they wrote down the typechecking/evaluation semantics, even if it’s in the traditional form of a page’s worth of cryptic deduction rules.
I think [1] is a good summary of the types and [2] to be a good explanation of their philosophy, but I had some experience with lattice theory and typed feature structure grammars which helped a lot. There are a couple of papers cited in [2] that would help a lot in providing background.
Not quite a one-pager! Maybe it would make a good blog post...
