On 10/12/07, Steve Schafer <[EMAIL PROTECTED]> wrote: > 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
