RE: More on dispatching by function return type

["Kevin S. Millikin" <address@hidden>]

On Wednesday, December 17, 2003 2:35 PM, John Clements 
[SMTP:clements@brinckerhoff.org] wrote:

> Yes, Haskell can... by examining the result of the type proof.  This
> is my point, plain and simple: in order to reason about the program,
> the programmer must be able to compute the result of the type proof.
> This is not the case for other languages (e.g.--I claim--ML).

Simplified implementation of Read typeclass in Standard ML:

- (* class declaration *)
- type 'a reader = string -> 'a;

- (* a couple of instances *)
- val readBool : bool reader = fn _ => true;
- val readInt : int reader = fn _ => 42;

- (* Ken shan's example, simplified *)
- fn r => not o (read r);

Now, does the programmer have to "compute the result of the type proof" 
to reason about this program?