# [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