A few weeks ago, I ran into a type checking issue that I had never been warned about before that called for Skolem constants.
The biggest issue, for me anyway, was that it sort of came out of nowhere. I felt like I should have heard something about this before running into it face first while trying to implement a type checker for a really simple language.
While commenters on the last post found several references to explaining Skolem constants and their use, I hadn’t yet really tracked down the origin of their use in type checkers. Completely by accident this week, I stumbled upon some candidates.
I was bored, so I started reading through the “notes” sections of each chapter of Design Concepts in Programming Languages. Chapter 14 (on Abstract Types) just so happens to mention nonce types, which are essentially the same thing, and listed some references to something called type generativity in SML.
One of them was to the Definition of Standard ML, which I had noted last time that I hadn’t had a chance to check yet. (I really need to find a copy of this. Am I blind, or are there no links to this document from smlnj.org? I guess there’s always the library…) The other:
These seem to only discuss the issue of holding a type abstract in the context of module systems, but it’s essentially the same idea. The only thing I’m really missing is an obvious source explicitly noting that this sort of thing is required to type check bog-standard Haskell type annotations.