[Haskell-cafe] Optimization with Strings ?

[Neil Davies]

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 <semanticphilosopher at 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
>
>
> -- 
> Colin Adams
> Preston,
> Lancashire,
> ENGLAND