[Haskell-cafe] Re: Type-level arithmetic
catamorphism at gmail.com
Fri Oct 12 19:26:49 EDT 2007
On 10/12/07, Brandon S. Allbery KF8NH <allbery at ece.cmu.edu> 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
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.
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
More information about the Haskell-Cafe