[Haskell-cafe] Re: Type-level arithmetic

[Philippa Cowderoy]

On Fri, 12 Oct 2007, Steve Schafer wrote:

> On Fri, 12 Oct 2007 13:25:28 -0700, you wrote:
> 
> >I'm not sure what sanity has to do with it. Presumably we all agree
> >that it's a good idea for the compiler to know, at compile-time, that
> >head is only applied to lists. Why not also have the compiler check
> >that head is only applied to non-empty lists?
> 
> Again, that sort of practical application of type systems is not (as far
> as I know) what this discussion is about. This discussion was spawned by
> talk of using the type system to do truly bizarre things, such as solve
> the Instant Insanity puzzle. A while back, Dan Piponi posed the question
> of using the type system to solve one of the liar/truthteller logic
> problems. And so on.
> 

Which is nevertheless the kind of power you need in order to also be able 
to prove precise properties. How are you going to prove that an entire 
class of problems is solveable (and the safety or termination of a piece 
of code may depend on this) if you can't prove that an individual one is?

-- 
flippa at flippac.org

A problem that's all in your head is still a problem.
Brain damage is but one form of mind damage.