Re: dynamic vs. static typing

[Matt Hellige <address@hidden>]

[Neelakantan Krishnaswami <neelk@gs3106.sp.cs.cmu.edu>]
> 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>
> 

This is both true and useful. But what's the point of permuting the
elements of a list if no other part of the program can or will ever
inspect the values? In fact, how could one even determine that such a
permutation had been done?

Matt

-- 
Matt Hellige                  matt@immute.net
http://matt.immute.net