On 10/12/07, Brandon S. Allbery KF8NH <[EMAIL PROTECTED]> 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... > I have the same impression, that Andrew isn't interested in dependent > typing. I'm not sure what he was really asking in his OP either, but when he said that he was looking for a language where you can write type signatures that encode list length, that certainly points to dependent types as one instance of that, even if there are other possibilities. Cheers, Tim -- Tim Chevalier * catamorphism.org * Often in error, never in doubt "The way NT mounts filesystems is something I'd expect to find in a barnyard or on a stock-breeding farm."--Mike Andrews _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe