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 <semanticphilosop...@googlemail.com>:
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
