[Haskell-cafe] Re: Type-level arithmetic

[Philippa Cowderoy]

On Fri, 12 Oct 2007, Steve Schafer wrote:

> On Fri, 12 Oct 2007 21:51:46 +0100 (GMT Daylight Time), you wrote:
> 
> >Which is nevertheless the kind of power you need in order to also be able 
> >to prove precise properties.
> 
> We're not talking about POWER, we're talking about SYNTAX.

Which has no small amount to do with the power to express problems in a 
natural way, no? My point being that we already want this for things that 
are more obviously appropriate uses of a type system.

> To which my rejoinder is, "To what end?" To extend the _syntax_ of the 
> type system in a way that allows such "natural" expression turns it into 
> yet another programming language. So what have we gained?
> 

It's already yet another programming language, whether you like it or not 
- the question is how usable it is. Either you accept the gains made on 
the way or not, but what we have gained is the ability to reason about our 
programs in the language they are written in.

We already have types-of-types in Haskell, they're called kinds. There's 
even a language that'll let you stack this as far as you like - why not? 
Zero, one or infinity, what else is new?

-- 
flippa at flippac.org

Society does not owe people jobs.
Society owes it to itself to find people jobs.