[Haskell-cafe] Re: Type-level arithmetic

[Tim Chevalier]

On 10/12/07, Steve Schafer <steve at fenestra.com> 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