Polymorphic typechecking doesn't work

[UnkindPartition]

It looks like hask always trusts type signatures and doesn't check them.

E.g.

from hask import *

@sig(H/ "a" >> "b" >> "c")
def const1(x, y):
    return x+1
print(const1(1,2))

runs successfully.

If my understanding is correct, perhaps you should highlight this fact in the readme and not claim "Full Hindley-Milner type system that will typecheck any function decorated with a Hask type signature".

[billpmurphy]

So, just to make sure we are on the same page: The bug shown in your example is that the output is of type int, not polymorphic. As I see it, the real problem here is that the type signature a -> b -> c doesn't really make sense in practice, since the only return value that can inhabit it is something like undefined or bottom, which we don't really have in Hask. What Hask should do in this case is simply not allow that kind of type signature.

I hope I did not give the impression in the README that Hask is doing type inference on the function body--that is essentially impossible in Python. Nor does it really make sense to do this--in your example, for some a and b, a + b can be any type depending on the definition of a.__add__. If I gave this impression in the README, then I need to change the wording.

For example, there is really no way that Hask can or should detect this behavior at function-creation-time, even though it causes a runtime error:

@sig(H/ "a" >> "b" >> "a")
def const1(x, y):
    return x + 1

const1("b", 1)

What Hask is doing is inferring types within the type signature and when functions are composed, and checking the types when arguments are supplied and when the function is evaluated.

[UnkindPartition]

Indeed, the example shows not one, but two bugs. (I first meant to post two examples -- hence 1 in const1 -- but then merged them into one.)

If what you're doing is separately unifying a with the type of the first argument, b with the type of the second argument, and c with the type of the result, then I'd suggest not mentioning Hindley-Milner, as this is nothing like it.

[billpmurphy]

If you look under the hood at hindley_milner.py, it does have a real implementation of HM (i.e., if you create expressions in the internal type language, which is basically just lambda calculus, it will infer the most general type; there are some examples of this in tests.py). But as you pointed out, Hask does try to unify arguments as soon as it receives them, and does not use inference on the body of functions, which is not HM.