Re: dynamic vs. static typing

[Neelakantan Krishnaswami <address@hidden>]

Peter van Rooijen writes:
> From: "Joe Marshall" <jrm@ccs.neu.edu>
> > I was just pointing out that lists of unknown objects are
> > interesting in and of themselves.
> 
> It seems to me that they are as interesting as natural numbers.
> 
> After all, that's what they are, right?

Not quite: you can reverse a list without knowing its contents.

Reynold's abstraction theorem says that parametrically polymorphic
functions do not perform any operations on the values at polymorphic
type. Phillip Wadler wrote a paper on how you can turn this around and
use it to deduce specific theorems about functions without actually
having to do a proof. For example, because reverse has the type

  reverse: List a -> List a

we know that it can't modify the values of the list. It can only
delete, copy, or permute the cons cells, all without looking at the
inside of its contents.

See: <http://citeseer.nj.nec.com/wadler89theorems.html>


-- 
Neel Krishnaswami
neelk@cs.cmu.edu