[Haskell-cafe] Re: Type-level arithmetic

Steve Schafer steve at fenestra.com
Fri Oct 12 16:20:43 EDT 2007

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.

More information about the Haskell-Cafe mailing list