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

On Oct 12, 2007, at 19:26 , Tim Chevalier wrote:

On 10/12/07, Brandon S. Allbery KF8NH wrote:

...

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.

Well, the type system *is* a metalanguage, so presumably Andrew's looking for something more specific than that...

My impression is he's looking for something more *general* than that. He wants to write entire programs in the type system, something like the crazies who write programs in C++ templates such that template expansion does all the work at compile time and the runtime code just prints the constant result. Certainly this covers dependent typing, but it goes well beyond it. -- 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