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

On Sat, Jun 13, 2009 at 6:03 PM, Sam TH<samth at ccs.neu.edu> wrote:
> On Sat, Jun 13, 2009 at 5:45 PM, Todd O'Bryan<toddobryan at gmail.com> wrote:
>
> But if you really want to compute with the types, like this:
>
> (if (equal? (type-of 3) (type-of -3)) 'yes 'no)
>
> then that's more difficult to support,

This is the kind of stuff I would like to do, yes. I guess I'm asking
for run-time type annotations, as Shriram correctly inferred from my
none-too-clear text, with a sufficiently developed semantics to handle
subtypes, unification, etc.

> and if you want to do something
> like this:
>
> (: x (if stuff? Number String))
> (define x ...)
>
> then static checking is suddenly much harder.

This is clearly insane--I have never even considered such an idea. :-)

And it goes to show how naive about this stuff I am. If you limit
yourself to types, unions, parametric types, etc. in type declarations
and don't allow general Scheme code, I gather that the system doesn't
explode. I'm more than willing to do that--thank you for pointing out
how taking my previous statement at face value would have caused a
mess to happen.

> So, I would say, try to come up with specific use cases for
> computation with types, and then your question will be easier to
> answer.

Thanks. I'm trying to work through HtDP the way I wish it worked. I'll
send examples as I come up with them. Maybe Shriram can intuit what I
really want and you can explain how to get at it.

Todd