On 10/05/2012 03:04 PM, Invisible wrote:

> Basically, the FUNCTION may be polymorphic, but every CALL to the
> function involves fixed types. If the calling function is itself
> polymorphic, then you can trace that out to the next step. In summary,
> if you take any valid Haskell program and analyse the entire program
> text, you can always statically compute the exact type of everything in
> the program.
>
> In a sense, this is pretty damned similar to C++ templates. All the
> polymorphism is at compile-time.

On closer inspection, this isn't *quite* true...

The counter-example I was shown is this:

   wrap :: Show x => Int -> x -> String
   wrap 0 x = show x
   wrap n x = wrap (n-1) [x]

This is "polymorphic recursion". The function recursively calls itself 
with a different type. Basically, it takes some data and wraps it in N 
layers of lists. And since N can only be known at run-time, you can't 
statically say how many times you need.

Actually, if you're paying attention, you'll notice that if N is 
*negative*, this yields an infinite loop, requiring infinity different 
type instanciations.

(And if you're *really* paying attention, you'll notice that Int has a 
finite number of bits in it...)

This example is fairly stupid of course - why would you want to wrap a 
value in a list of lists of lists? But it demonstrates an interesting 
edge case.

Notice that since the final type of X is determined by N, the function 
cannot *return* X, since there would be no way to write a sensible type 
signature for that. It can only apply a polymorphic function to X and 
return the result from that. (In this case, the "show" function, which 
works for any degree of wrapping.)

IMHO, all of this is probably of theoretical interest only. I can't 
imagine there being much practical use for it...

Post a reply to this message