Re: [Haskell-cafe] Re: Type-level arithmetic

On Oct 12, 2007, at 16:25 , Tim Chevalier wrote:

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

You two are talking past each other. You're talking about dependent typing, etc. Steve's complaint is not about dependent typing; he's saying Andrew is looking for something different from that, namely the type system being a metalanguage. I have the same impression, that Andrew isn't interested in dependent typing. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH