Matthias Felleisen wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> Okay, this didn't work out. Let's try again.
> Are examples out there that show how naive reasoning about languages
> (not individual programs) is a major problem?
> The canonical example is to combine polymorphic let without
> restrictions with naive generalizations for references, exceptions,
> continuations, and channels.
> Any other examples than the one above? One is a random hit, two is
> a coincidence, three makes a pattern. -- Matthias
A cousin example is type isomorphism. How far can we go in the idea
that a function of type A->B->C can be a match for a function of type
B->A->C? A semantic notion of type isomorphism helps.
Ok, this is very close to the first example; it may count for only a