On Oct 12, 2007, at 19:26 , Tim Chevalier wrote:
On 10/12/07, Brandon S. Allbery KF8NH <[EMAIL PROTECTED]> 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] [EMAIL PROTECTED]
system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED]
electrical and computer engineering, carnegie mellon university KF8NH
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
