[plt-scheme] macro question

From: hendrik at topoi.pooq.com (hendrik at topoi.pooq.com)
Date: Tue Jun 10 11:40:17 EDT 2008

On Sun, Jun 08, 2008 at 04:01:02PM -0400, Matthias Felleisen wrote:

> Pedagogically: Types in TS play the role of contracts in HtDP. All  
> programs could be assigned types, and the type checker should 'bless'  
> them all. In the long run, I am considering using Typed Scheme for  
> the introduction of types into the HtD curriculum. Some unnamed  
> schools switch to ML for this purpose, but I think type inference  
> gets in the way of understanding the power of a rich type language.

Type inference gets in the way of understanding programs in the 
language.  I need to see the types when I'm reading the program, so I 
know what it all means.  It's not enough to know that there exists a 
way of attaching types to the code.

> (Having said that, TS supports 'local' type inference and we may  
> develop tools based on past soft typing work (inference via HM or  
> SBA) to help programmers port untyped modules into the typed world.)

There are a few type inferences that do not seem to harm the 
readability of a program.  Type information can flow:

(a) from the declaration of an identifier to its use

(b) from the leaves of a parse tree towards its root (the usual 
direction of expressino evaluation)

(c) from the root of a parse tree towards the leaves (called coercion in 
Algol 68; a mechanism whereby the context of an expression affects its 
meaning.  Used for determining the types of initializers in C.

I haven't yet seen anything else that didn't become obscure.

-- hendrik

Posted on the users mailing list.