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

On Sat, Jun 13, 2009 at 6:00 PM, Shriram Krishnamurthi<sk at cs.brown.edu> wrote:
>> 2. Types in the Language
>
> These are not types.  These are simply inspectors on the run-time
> tags.  Your own example illustrates the point:
>
>>>>> type(isinstance)
>> <type 'builtin_function_or_method'>
>
> The *type* of isinstance would be something like
>
>  isinstance :: value x type -> boolean
>
> [Never mind that type should not be a type.]  In contrast, the
> run-time tag is "some kind of applicable object", and that's what
> Python gives you.

You're absolutely correct, and that's the confusion I was suffering
from. I *do* want run-time type annotations/tags that ride along with
values, so that students can make assertions and ask questions about
them.

You're exactly right that the type of isinstance should be more
specific, and I'd want something like

> (type is-of-type)
Any Type -> Boolean

in the Scheme version (where Type is the top of the hierarchy of
run-time tags that describe types).

>> OK, the last line is not particularly useful, but every Python value
>> knows what it is, these types are real objects in the language, and
>> programs can manipulate and ask questions about them.
>
> 1. I see no pedagogic value in this.

Have you never had a student try to return a number instead of a posn?
Or (much more common and much more painful) in the chapters on binary
trees and family trees, students get confused about the kinds of
structures they're building and bury a mistake so deep in a structure
that by the time they get the error message it's not clear where they
painted themselves into a corner. These are the problems that they
spend ten or fifteen minutes staring at, and when I get there, I know
it's a type problem, but there are three or four functions, all with
working test cases that could have triggered the problem, and I have
to spend 5 minutes unwinding everything with them.

Outside of Scheme programming, I think there's a great deal of
pedagogic value in getting them to think about types. All of my
students get to AP Calculus AB or BC by their senior year and many of
them don't understand the relationship between the sets of numbers
they work with--naturals, integers, reals, rationals, irrationals, and
complex. It's not their fault--the curriculum I went through at the
same high school made that abundantly clear. Sometime in the 90's, we
went to something that was less theoretically rigorous and
concentrated more on applications. I'd like to drill them on type
judgments and the best way to do that is to have them be able to check
their judgments with a program that gives the right answer.

> 2. Scheme doesn't like to build in a bunch of crud.  You can choose
> whatever representation you want for run-time tags and construct
> essentially the same in Scheme using the built-in predicates.  If you
> think this is so useful for teaching, write a Teachpack that exports
> and standard interface for this.  I leave it as an exercise because
> it's not a very hard one.

I think that's what I'd like to do. Unfortunately, I'm running into my
ignorance of Scheme beyond HtDP. If you think it's pretty easy, I'd
like to give it a go, but I'm at a bit of a loss as to where to start.
Should I implement the run-time tags as objects because of the natural
sub-classing/sub-typing relationships, should a tag be a struct,
should I just have a bunch of symbols? Can you constrain the exercise
a bit?

>> I want types to impact students' programming,
>> because a huge proportion of the mistakes my students make have to do
>> with muddy thinking about types, and I think the programming
>> environment should make them be explicit about what they think is
>> going on and help them when they're wrong.
>
> If you want this, and you want dynamic enforcement (which you seem
> to), use the PLT contract system (not to be confused with "contracts
> as comments" a la HtDP), which is about as sophisticated as you will
> find in any language.

Exactly! I got so excited when I found the contract system, except it
only works across module boundaries and I want students' functions
checked within the file where they're defined. Is there any way to (a)
allow students to declare a contract in a fairly easy to understand
way, and (b) check the contract against all of the other uses in the
same module?


>> 3. Static Typing
>> Yea for Python--I can play with types in the language.
>
> No you can't.  You can play with run-time tags, as you can in lots of
> other languages.
>

Exactly. Is it safe to say that, for each type in the language, I want
a run-time-accessible value that corresponds with that type that can
be manipulated by the language--including some specific functions like
unify types, check if a value is of a type, etc.--or am I still not
correctly verbalizing/understanding what I'm asking for?

> Shriram

Thanks for correcting my misapprehensions!

Todd