[Haskell-cafe] Re: Type-level arithmetic

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

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

Steve Schafer
Fenestra Technologies Corp.
http://www.fenestra.com/