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

On Mon, Jun 15, 2009 at 1:10 PM, Stephen Bloch<sbloch at adelphi.edu> wrote:
> I'll have to think about this: "type" as a type still seems so elegant, so
> expressively efficient :-)  My naive first impulse is to suggest a
> consistent but incomplete static type-checker that never misclassifies
> something's type, correctly classifies the types of MOST expressions in
> practice, and when it can't, knows when to give up so it at least
> terminates.  Has somebody already proven that that's unattainable too?

FWIW, I rather like Agda's intuitionistic approach to this via it's
Set type hierarchy. Set is not an element of Set, but that doesn't
stop you from working with higher order constructs. I'm not sure what
a great reference would be, but if you just search for "Set1" (which
does contain Set!) in the link below you can see some examples.

http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf

Anthony