notes-computer-programming-programmingLanguageDesign-prosAndCons-returnTypeOnlyPolymorphism

in Haskell this is confusing: http://stackoverflow.com/questions/3467279/how-to-create-a-polyvariadic-haskell-function

• you are using the type system's type inference combined with polymorphism to decide something which feels syntactic
• in unpacking this, you switch from reading things from left-to-right and right-to-left three times
  • when you first see 'sumOf 5 8 22 :: Integer', you read it left to right. And indeed, that's how it parses: (((sumOf 5) 8) 22) :: Integer
  • but now, you see that you need to determine the type of 'sumOf 5' in order to compute the first term. You know it takes an Int as integer. But you don't know what type it yields as output.
  • So you look further to the right. 8 is an Int, but you still don't know what you need. So you look further to the right. 22 is an Int and you gotta have an Int at the end. So the type of ((sumOf 5) 8) 22 must be Int -> Int.
  • And now you have to switch and go right to left. Since ((sumOf 5) 8) 22 must be Int -> Int, ((sumOf 5) 8) must be Int -> Int -> Int, and sumOf 5 must be Int -> Int -> Int -> Int.
  • Now you start substituting the fn defn. Int -> Int -> Int -> Int matches (Int -> (*)) so (sumOf 5) is replaced by (sumOf . (5 +) . toInteger).
  • But now you have to go right again. (((sumOf . (5 +) . toInteger) 8) 22). And now you have to go leftwards from the 8 (not sure if i got this step right, i forgot how . work w/ grouping): ((sumOf . (5 +) . (toInteger 8)) 22) -> ((sumOf . (5 +) 8) 22) -> ((sumOf (5 + 8)) 22).
  • Now you have to go right to left again (or just remember your earlier going-left work); ((sumOf (5 + 8)) 22) :: Int so (sumOf (5 + 8)) :: Int -> Int so sumOf :: Int -> Int -> Int. Then go left to right again to expand: (sumOf (5 + 8)) 22 -> (sumOf . ((5 + 8) +) . toInteger) 22. Then go right to left again to apply: (sumOf . ((5 + 8) +) . toInteger) 22 -> (sumOf . ((5 + 8) +)) 22 -> sumOf . ((5 + 8 + 22))
• the types of parts of the expression are unexpected and context-dependent and seemingly inconsistent with each other. You wouldn't expect the type of 'sumOf 5' to be 'Int -> Int -> Int', you'd expect it to be 'Int', because if you said (sumOf 5) + 3 you'd get 8. It's only 'Int -> Int -> Int -> Int' in this particular context. Indeed, right in this derivation, we see that (sumOf 5) is of type Int -> Int -> Int -> Int, but (sumOf (5+8)) is of type Int -> Int, and (sumOf (5+8+22)) is of type Int->Int->Int.

i'm not sure exactly what i want here. i consider this abuse of the type system but by what criteria?

One could say: if there is an expression containing subexpressions which are equivalent to the same function given the same type of input, then they should be the same type. But this would pretty much rule polymorphism only on the return type, because you could have a long program as one expression with different uses of the same function in very different places. Not sure if that is a big sacrifice or not: see http://programmers.stackexchange.com/questions/105662/is-return-type-only-polymorphism-in-haskell-a-good-thing

In there, my interpretation of what Philip JF points out is that if you have values that are union types, then that's not too different from 0-ary functions which return different types, since in Haskell 0-ary functions aren't distinct from their return values. So it would seem inconsistent to disallow non-0-ary functions from doing that while allowing 0-ary functions to.

Some potential responses that i can think of:

• (a) be inconsistent, disallow non-0-ary functions from having multiple potential return types
• (b) make our objection more specific to focus on ad-hoc polymorphism. We are not irked merely by functions whose return type may be multiple things even after fixing the input types; rather, we are irked by the conjunction of that with ad-hoc polymorphism.
• (c) make our objection more specific to focus on kinds. We are not irked merely by functions whose return type may be multiple things even after fixing the input types; rather, we are irked by functions whose return type may be multiple KINDS (see http://en.wikipedia.org/wiki/Kind_%28type_theory%29#Kinds_in_Haskell ) even after fixing the input types. However, http://en.wikipedia.org/wiki/Kind_%28type_theory%29#Kinds_in_Haskell says that Haskell doesn't allow polymorphic kinds already., so how is "class SumRes? r where sumOf :: Integer -> r; instance SumRes? Integer where sumOf = id; instance (Integral a, SumRes? r) => SumRes? (a -> r) where sumOf x = sumOf . (x +) . toInteger;" even valid? It's because haskell is happy to think r is of kind *, that is any kind. Haskell by default infers the most general kind, whereas here we would like it to infer the most specific kind. But this seems to fall to the same objection as before; e.g. the empty list might be a list of integers, or functions, or functions of functions, right?
• (d) take the intersection of the last two bullet points; the only thing we object to is when there is ad-hoc polymorphism which dispatches based on return-only differences in kind.
• (e) take the intersection of (b) and automatic type inference; allow things like that, but force a type annotation immediately after the return-type-only-polymorphic function.
• (f) or, the same as (e), but intersected with (c) as well, e.g. if there is a return-type-only-kind-polymorphic function, then its return type will not be inferred but must be type annotated. E.g. ((((sumOf :: Int -> Int -> Int -> Int) 5 :: Int -> Int -> Int) 8 :: Int -> Int) 22) :: Int.

however, http://programmers.stackexchange.com/questions/105662/is-return-type-only-polymorphism-in-haskell-a-good-thing suggests that this is related to Haskell's monomorphism restriction ( http://www.haskell.org/haskellwiki/Monomorphism_restriction , http://www.haskell.org/onlinereport/decls.html#monomorphism). Perhaps while fixing this we want to remove enough power to make the monomorphism restriction irrelevant. I'm not sure that http://programmers.stackexchange.com/questions/105662/is-return-type-only-polymorphism-in-haskell-a-good-thing is correct about it being tied to polymorphic-return-only types, though.

actually, some of these responses won't work; consider a fn sumOf2 which has a polymorphic form which takes pairs of inputs (a,b).

Now do

sumOf2 x = sumOf (x,b) sumOf2 5 8 22 b 5 8 22 :: int

i'm not sure if that that is quite right but i bet you can fix it somehow. The point is, to make the backwards type system inference produce a value b whose type contains the forbidden information from the future that we dont want sumOf to polymorph on, and then to feed that b to sumOf as an input, so that it uses input polymorphism, not return polymorphism, to utilize the forbidden information.

another idea is to limit polymorphism as follows: the function signature for all of the polymorphic forms must be a (single) template. You can still get ad-hoc in the implementation.

umm, no dude, that isn't good enough, the offending example already meets this:

class SumRes? r where sumOf :: Integer -> r

instance SumRes? Integer where sumOf = id

instance (Integral a, SumRes? r) => SumRes? (a -> r) where sumOf x = sumOf . (x +) . toInteger

hmm.. the problem seems to be that one of the instances demands a higher kind and the other doesnt. But if you forbade this, could someone get around it by just wrapping the higher kind in an opaque wrapper type like IsAFunction??

hmm.. no, the offending example doesnt quite meet this; should require that in each function in the class, no type parameters appear that didnt appear in the inputs to that function.

but, as noted above, you could get around this by giving a dummy argument to the fun (e.g. sumOf(dummy)) so that the compiler can infer 'dummy' to be the desired return type

see jasperType.txt for current best guess