Re: [Haskell-cafe] Optimization with Strings ?

Ah but the type system is the proof - it doesn't permit you to construct things that are 'unsafe' - the whole way the language (and its implementation) is constructed is to do that for you. The issue is that, very occasionally, you the programmer (usually for reasons of performance - runtime or code lines) want something slightly out of the ordinary. This is the escape mechanism. To quote the late, great DNA - it is all about rigidly defined areas of doubt and uncertainty - one of the arts of programming is to push all the nasty doubt and uncertainty into a small corner where you can beat it to death with a large dose of logic, proof and (occasional) handwaving... Now before you start talking about 'surely the type system should be complete' - I refer you to http://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theorem Take comfort in that, I do, it means that us humans still have a role....... Neil On 4 Dec 2009, at 09:16, Colin Adams wrote:

But the type system doesn't insist on such a proof - so is it not a hole?

2009/12/4 Neil Davies :

...

Or maybe it should be renamed

proofObligationsOnUseNeedToBeSupliedBySuitablyQualifiedIndividualPerformIO

which is what it really is - unsafe in the wrong hands

Nei

On 4 Dec 2009, at 08:57, Colin Adams wrote:

...

...

Please help me understand the holes in Haskell's type system.

Not really wanting to support the troll, but ...

unsafePerformIO?

Can't it be removed? -- Colin Adams Preston, Lancashire, ENGLAND _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Colin Adams Preston, Lancashire, ENGLAND