On 10/12/07, Steve Schafer
On Fri, 12 Oct 2007 13:03:16 -0700, you wrote:
It's different because the property that (for example) head requires a nonempty list is checked at compile time instead of run time.
No, I understand that. Andrew was talking about using type programming to do the things that a sane person would use "ordinary" programming to do.
I'm not sure what sanity has to do with it. Presumably we all agree that it's a good idea for the compiler to know, at compile-time, that head is only applied to lists. Why not also have the compiler check that head is only applied to non-empty lists? If you think it's sane to want one property checked at compile-time and insane to want the other property checked at compile-time, can you describe your test that can be applied to program properties to determine whether or not it's sane to want them statically checked?
And he wanted to know if there were any efforts to create a type system syntax that better supported that. But it seems to me that when you do that, the language of the type system begins to look like a general-purpose programming language. And that just shoves everything up to the next "meta" level. Pretty soon, you're going to need a meta-type system to meta-type-check your type language, and so on.
This criticism has been made before.
I'm all for enhancing the expressibility of concepts _related to typing_ within the type system, but I don't think that was the original point of this discussion. After all, Andrew's original message mentioned "stuff the type system was never designed to do."
What do you mean by "related to typing"? Haskell's type system allows us to say that head is a function that maps a list of things of type a onto a thing of type a. A more expressive type system might allow us to say that head's domain consists of *non-empty* lists. In this type system, emptiness or non-emptiness is "a concept related to typing", because it's a concept that that type system can express. You seem to be criticizing richer type systems on the sole basis that they are richer than existing ones. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "I always wanted to be commander-in-chief of my own one-woman army" -- Ani DiFranco