[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: the forward method [dynamic vs. static typing]




On Dec 15, 2003, at 1:44 PM, John Clements wrote:

>
> On Dec 9, 2003, at 7:40 PM, Ken Shan wrote:
>
>> Static typing can make programs more concise: I can write
>>
>>     getLine >>= print . (/2) . read
>>
>> or
>>
>>     getLine >>= print . not . read
>>
>> rather than
>>
>>     getLine >>= print . (/2) . readDouble
>>
>> or
>>
>>     getLine >>= print . not . readBool
>
> Jumping rather late; Ken, this doesn't seem like a (generally) good 
> idea.  That is, when the meaning of a function call depends not just 
> on its inputs but also on how its output is used, it could be very 
> hard to reason about a program.
>
> Typically, type systems help you to construct a proof that certain 
> errors cannot arise during evaluation.  When parts of that proof are 
> used to alter the evaluation itself, you suddenly have a class of 
> _runtime_ errors (or rather, "mis-behaviors") that can only be 
> understood by examining the type proof.
>
> I see that read is something of a special case, but even here I can 
> imagine some _really_confusing_ errors:  E.G.: compiled program 
> prompts: "Enter a String:".  User enters a string. Now user gets 
> message:  "read: expected double, given string".  Huh?
>
> I admit that this is somewhat contrived, because in general when the 
> programmer asks for a string, the result of that call will be used in 
> a way that allows the type system to infer that it must be a string.  
> In a test harness, though, I can see this coming up.
>
> So: does Haskell (or some of its implementations) really work this way?
>
> john
>
> p.s.: I've read about ten messages past the one I'm responding to; if 
> this topic has already been hashed out, please ignore it.

In the tradition of others within earshot, I'm going to respond to my 
own message.

Based on my conversation with Philippe Meunier, I'm going to refine my 
argument:  My claim is that you can't write down a deterministic 
operational semantics for Haskell that doesn't involve the result of 
the type proof.  My further claim is that for other languages, you can. 
  Obvious exceptions to this are languages like C that aren't 
deterministic.  And of course, concurrency really scotches my 
determinism as well. "YKWIM".

john