[Haskell-cafe] Re: Type-level arithmetic
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Fri Oct 12 19:37:07 EDT 2007
On Oct 12, 2007, at 19:26 , Tim Chevalier wrote:
> On 10/12/07, Brandon S. Allbery KF8NH <allbery at ece.cmu.edu> 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 at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university KF8NH
More information about the Haskell-Cafe