On Oct 12, 2007, at 16:25 , Tim Chevalier wrote:
On 10/12/07, Steve Schafer <[EMAIL PROTECTED]> 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] [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
