[plt-scheme] macro question

On Jun 8, 2008, at 6:01 PM, Prabhakar Ragde wrote:

> Matthias Felleisen wrote:
>
>>> How do contracts fit into this view?
>> I am giving two answers because I am not sure what the question  
>> aims at:
>
> Thanks, Matthias. My question was aiming on the technical side, but  
> the pedagogical side is also intriguing. Understanding the error  
> messages that result when HM-style type inference fails (at least  
> in my limited experience with SML and GHC) seems to me to be the  
> largest barrier to moving freshmen or sophomores from HtDP into a  
> statically-typed environment with a sensible type system.


The XML work (Harper/Mitchell) and Cardelli's tech rpts from around  
the same time makes one thing pretty clear: type inference is a tool,  
types are what matters. In this spirit, your statement is wrong  
because we can easily avoid type inference in Typed Scheme _and_ move  
freshmen to a fairly sophisticated type system in the first year.  
Indeed, Typed Scheme's type system is somewhat more sophisticated  
than ML's, with (for example) first-class polymorphic functions,  
which ML doesn't have.

So what's the real problem with type systems? A type system is a  
theorem checker. When type systems get complicated (allow the  
statement of complex thoughts about programs), they tend to include  
some fair amount of local (not HM) inference so that programmers  
don't have to spell out every single detail of thee complex claims.  
BUT, when then the theorem checker becomes a theorem prover, and  we  
don't understand to this day, how to inform people why theorem  
provers failed and how to restate the theorem and its lemmas in order  
to get the proof through. However, I consider this problem secondary  
in the context of Typed Scheme because we can always state types and  
get the checker to report reasonable precise failure messages.

I would never ever use HM type inference (with SML's mechanism) on  
freshmen. That's torture. -- Matthias