1. 8

  2. 3

    I have no idea what “spooky errors at a distance” Chris is talking about.

    h : α → β
    g : β → γ
    f : γ -> δ
    let v = h foo 
    let v' = g v
    let v'' = 

    Suppose the type of h changes to α → ε. If the type ε is not compatible with β, h foo will fail to typecheck. Coming up with a type that is compatible with everything except γ is hardly easy.

    1. 4

      I think your example is different from what Chris had in mind, but I agree with your point. It’s hard to say that type inference would be problematic without knowing both what the inference algorithm is, and what the code in question is.

      I use OCaml a lot and I can’t say I often run into this kind of “spooky errors at a distance”. In practice, even if you don’t use type annotations in the code, it’s good practice to write module interfaces with explicit types. So a change in types in one place will give pretty obvious errors about where to fix it. If you’re not writing interfaces, you’re probably dealing with localized, coupled code, where making the type changes aren’t a big deal and the issues Chris describes aren’t so important.

      1. 1

        The situation I was thinking of goes something like this. Go has inside a function type inference for return types, so you can write newvar := afunc() and the type of newvar is inferred from afunc()’s return type. Now suppose you extend this to inferring the return type of a function through some syntax (either returning newvar or simply doing return afunc()). This allows you to create a chain of functions with inferred return types; you call afunc() and use its type as your inferred return type, then someone calls you and uses your return type (inferred from afunc()) as their return type, and so on. Then eventually someone at the top of the call chain actually uses a return value in a way that requires it to have a specific type, which is compatible with afunc()’s current return type.

        Then afunc() changes its return type. Your function is still type correct, just with a different inferred return type, and so is your caller, and so is your caller’s caller, and so on all the way up to the person who actually uses a return value in a way that is now incompatible with afunc()’s new return type. That person gets a type error.

        (To make this easier to happen, you can actually do a lot of generic things with values in Go; for example, as long as a value is some sort of pointer, you can always compare it with nil, and if a type is some sort of a number you can compare it with zero or another constant. This covers a lot of ground in much practical code, right up to the point where someone wants a particular sort of pointer or number for various reasons.)

        1. 1

          I haven’t used Go but this sounds very similar to languages with “more” type inference (Haskell, for instance) which force you to add type annotations to top-level forms so these errors cannot propagate outside the source file anyway.

          I see a distinction between type systems with “proper inference” and the ones that only propagate types “downwards”[*] – can Go infer the type of a variable by its usage later on in the function? (Does it ever need to?)

          [*] I think var x = y in C# is an example of this, where it’s “inference” in that it lets you omit declaring the type of x when both you and the compiler know exactly what its type is (it’s the type of y).

          1. 2

            can Go infer the type of a variable by its usage later on in the function?

            No, it can’t. I’ve seen it referred to as “type deduction” instead, although the spec uses no such language (nor does it use the word “inference”): https://golang.org/ref/spec#Variable_declarations

            I think “limited inference,” as used by the OP, is an okay phrase to use to describe this. But there is certainly a distinction between the inference used by Go and the inference used, by, say, Haskell.