[Haskell-cafe] Re: Type-level arithmetic
Brandon S. Allbery KF8NH
allbery at ece.cmu.edu
Fri Oct 12 19:22:41 EDT 2007
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
>> to do the things that a sane person would use "ordinary"
>> programming to
> 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
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