On 10/12/07, Brandon S. Allbery KF8NH
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