[Haskell-cafe] Re: Type-level arithmetic

[Brandon S. Allbery KF8NH]

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