Re: [Haskell-cafe] Limits of deduction

Christopher L Conway wrote:

On 5/14/07, Roberto Zunino wrote:

...

Also, using only rank-1:

polyf :: Int -> a -> Int polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z->z) else polyf (x-2) 3

Here passing both 3 and (\z->z) as y confuses the type inference.

Actually, I tried this in ghci... Should this work?

polyf.hs: polyf x y = if x==0 then 0 else if x==1 then polyf (x-1) (\z->z) else polyf (x-2) 3

NOTE: no type signature

I forgot to mention a *use* of that as in test = polyf 1 2 Then: No instance for (Num (t -> t)) (see also below) Also, we can avoid type classes and _still_ have inference problems: using (3 :: Int) in polyf yields: Couldn't match expected type `Int' against inferred type `t -> t' which is actually the type mismatch error I had in mind. So, even in Haskell - type classes, we need signatures in some cases.

Prelude> :l polyf [1 of 1] Compiling Main ( polyf.hs, interpreted ) Ok, modules loaded: Main. *Main> :t polyf polyf :: forall a t1 t. (Num (t1 -> t1), Num a, Num t) => a -> (t1 -> t1) -> t

The inference assigns y the type (t1 -> t1) even though it is assigned the value 3?

Yes, because Haskell natural literals are overloaded: 3 :: forall a. Num a => a So 3 :: (t1 -> t1) is "fine" provided you supply a Num instance for that. Alas, only trivial instances exists (0=1=2=..=id). Zun.