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

On Sat, Jun 13, 2009 at 06:33:41PM -0400, Todd O'Bryan wrote:
> 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. :-)

I have.  The problem is, in generality, infeasible, but it is possible 
to make useful approximations to it based on various heuristics.

You can go further if you allow the programmer to provide sufficient 
proof hints, you can actually do this in much generality, but it becomes 
impractical to program.

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

Except for the paametric types, that looks like the type system in Algol 
68 (dated 1968).  Within a year or two it was generalized to allow 
parametric types, provided that values of these parametric types were 
always pointed to by references (something true of prett well everythig 
in Scheme.)

> 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
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme