[Prev][Next][Index][Thread]
Re: failures
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
half hit.
Olivier Ridoux
--
Docendo discimus