[Haskell-cafe] Re: Type-level arithmetic

[Tim Chevalier]

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
> 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