[plt-scheme] macro question

On Jun 8, 2008, at 11:50 AM, Prabhakar Ragde wrote:

> How do contracts fit into this view?

I am giving two answers because I am not sure what the question aims at:

Technically: Typed Scheme and Scheme modules may export to and import  
from each other. In order to make such interaction safe (type  
soundness), programmers must specify contracts at the boundaries of  
typed modules. These modules must be strong enough to enable the type  
checker to prove the correctness of the specified types.

(In our original theory, we had design an automatic synthesis and we  
may still implement something along those lines.)

We have not yet integrated the type system with the contract system.  
In other words, you cannot supplement typed exports with contracts  
yet. Future work.

;; ---

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.

(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.)


-- Matthias


> Are they an alternative, orthogonal, or do both types and contracts  
> need further development in order to be used effectively in tandem?  
> (My knowledge of type theory is only at about the senior  
> undergraduate level at this point, and I haven't looked seriously  
> at PLT contracts yet.)