A follow-up on Skolem constants

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:

Xavier Leroy. A syntactic theory of type generativity and sharing.  JFP 1996.

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.

This entry was posted in Compilers, Typing Tidbits and tagged . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s