[Haskell-cafe] Re: Type-level arithmetic

[Brandon S. Allbery KF8NH]

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

> On 10/12/07, Steve Schafer <steve at fenestra.com> 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 at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH