[plt-scheme] The perfect teaching language--Is this too much to ask for?

>
> See, I think that the problems that students have with design are
> because they don't pay enough attention to the types.

Yes, if you know what a type is, right? Imagine a world where you have
no idea what a type is and an instructor starts talking to you about
types. Formalizing the declaration of types, it seems to me, gets in
the way of beginners experimenting with their design. If nothing runs
until the type checker says it is OK and you are not even sure about
what a type is nor how to design code, you find yourself stuck unable
to test anything. My claim is that types are a hindrance at the
beginning. Later in life, students will appreciate and understand the
support a type checker provides.

To be honest, I have had a similar discussion with European colleagues
that are all for types from the beginning (needless to say they are
type gurus). They are unwilling to budge from the position that types
should be taught from day 1. I believe that the approach in HtDP/C
provides a gentle path into programming with types.

> The example I
> cited of returning "" instead of empty is quite common. Part of
> getting the design right is figuring out how the pieces *have* to fit
> together because of the types that they have. I think this is why
> writing the contract is the first step in the design recipe. If you
> don't know what kinds of things your function is supposed to consume
> and produce, you have no hope of getting the function right. And if
> you get the types wrong and program to the contract, you're guaranteed
> to get a function that won't work.
>

Yes, but does getting a type error provide you with the insight to
know how to fix the problem? If you are experienced.....probably. On
the other hand, using your example, a beginning student that returns
"" instead of empty in their code is unlikely to suddenly get it
because the type checker signals an error. The error does not suddenly
make more sense. It is different with an experienced programmer that
will recognize his/her silly mistake.

>
> This is a valid point, but I much more often see students who have
> test cases that don't match contracts and refuse to change the test
> cases that work.
>

Yes, yes, yes. :-) Students do write functions and test cases that
don't match the contract. I personally believe there is a great deal
of value in having students reason through their code to find where
the problem is. A type checker would deprive them of the opportunity
of engaging in this process of discovery. After all, the type checker
will point exactly where the problem is (right? ;-).


>> If the above is not convincing, how about getting beginning students
>> to write typed programs for abstract functions that manipulate
>> compound data structures? How about getting the types right for
>> programs that use encapsulation? All of the sudden, types get in the
>> way of undertsanding fundamental concepts. Be careful for what you
>> wish for!
>
> I disagree completely with this. When we get to abstract list
> functions, I think it's the types that keep students sane.

Please, send me your students! :-) If they can reason through the
contracts (not to say types) of abstract functions in general, I will
be more than delighted to have them in my class.

> To use
> build-list, map, filter, and the folds correctly, I think students
> *have* to consciously think about the types. Now, whether they have to
> get the fully abstracted types with type variables correct is
> something I'm not too insistent about

OK, but that is where things start getting hard for beginners. In
fact, how do they get a grasp of this "thinking consciously about the
types?" My conjecture is that they do not go off and write down a type
proof. Instead, they experiment by running their code and see how the
results match up with their understanding and with what they wrote.
It's this process of refinement that prepares them for programming in
a language with types. Even experts are surprised by the process of
refinement from time to time as witnessed on this thread. :-) Just
keeping things light!

I guess my point is rather simple. Types yes, but not at the
beginning. Let students wrestle with their designs (and type errors)
and we try to keep them from getting too frustrated.

-- 

Cheers,

Marco