[Prev][Next][Index][Thread]

Re: failures


Matthias Felleisen <matthias@ccs.neu.edu> writes:

>   The canonical example is to combine polymorphic let without
>   restrictions with naive generalizations for references, exceptions,
>   continuations, and channels.
> 
> For what else have we needed *any* form of semantics to dispute naive
> generalizations? 
> 
To dispute a generalization, a counter-example suffices. Generally a
naive understanding of the evaluation of a program is good enough to
realize that the counter-example is really one. So you don't even need
semantics to explain the problem of polymorphic let without
restrictions in the presence of references.

I think semantics comes into play if one wants to convince oneself
that a solution is really what it claims to be. Restricted polymorphic
let is such a case.

> Any other examples than the one above? One is a random hit, two is 
> a coincidence, three makes a pattern. 

Here are two others:

- Covariant vs contravariant overriding in object-oriented languages
  (more generally known as the binary method problem).  Eiffel got that
  one wrong. I need semnatics to convince myself that (for instance) mytype and
  matching is a solution.

- Abstract types as members of objects (also known as ``virtual
  types'' and similar to first-class modules). Beta's solution is
  not statically safe. The gbeta design is thought to fix the
  problems, but how can we be sure? 

To answer the last point, we have recently worked out a semantics for
objects with type members to establish soundness of ``beta-like''
language designs. A paper on this will appear in the next FOOL
workshop and can also be obtained at:

  http://lampwww.epfl.ch/~odersky/papers/fool10.html

Cheers

 -- Martin