Comment by tomp | Hacker News Reader

Comment by tomp | Hacker News Reader

Parent Full thread

(Disclaimer: I have yet to read the paper.) It's interesting because it's both important and hard.

It's important because it allows you to infer types in the presence of parametric polymorphism ("generics") and subtyping ("OOP"). For example, consider this function:

  twice(f, x) = f(f(x))
  twice : forall a. (a -> a) -> a -> a             // OCaml type (no subtyping)
  twice : forall a, b <: a. (a -> b) -> a -> b     // "ugly" type with subtyping
  twice : forall a, b. (a -> a & b) -> a -> b      // equivalent to the above, but maybe nicer to see and reason about

In OCaml, the type of this function would be too narrow, so you wouldn't be able to call `twice` with arguments such as `round : float -> int` (assuming `int <: float`). Stephen's previous work [1] infers the third type (`&` means intersection type).

It's hard because subtypes are hard to reason about. Type inference usually works by solving equations; if you have 3 type variables 'a, 'b and 'c, and you know that

  'a == list[int]
  'b == list['c]
  'a == 'b

then you can infer that `'c == int`. This breaks down in presence of subtyping; for example, you cannot use

  'a & 'b == 'c & 'b

to infer that `'a == 'c` (a possible solution is `'a == int`, `'b == int`, `'c == float`).

Type inference in the presence of subtyping is so hard that no programming language does it currently. There are many tricks and approximations - e.g. Scala does type propagation (if it knows the types of function parameters, it can infer the types of most other variables), and bidirectional type inference (it can figure out the types of anonymous function arguments), but AFAIK there is no existing implementation of it. Hopefully this paper changes that. Of course, there is an argument to be made that writing types in code makes it more readable, and therefore types should be written - in general, I agree with this argument, but type inference can still be very helpful (e.g. you write a function with complicated types and ask the compiler to fill in the type; or you write a number of tiny helper functions with obvious types).

[1] MLsub https://www.cl.cam.ac.uk/~sd601/mlsub/

> It's hard because subtypes are hard to reason about.

I think it's more correct to say that a language with both subtyping and parametric polymorphism is hard. Subtyping on its own or polymorphism on its own are pretty straightforward.

Though note that an even better type would probably be

    twice : forall a,b,c. ((a->b)&(b->c)) -> a -> c

(e.g. in MLSub, the type for

    twice (fun x -> x::[]) 1

is the unsatisfying

    (rec a = (a list | int) list)

rather than the expected

    (int list) list

)

You're right, interesting example! Although I'd prefer to "fix" this by incorporating first-class polymorphism [1] with MLsub - I guess non-polymorphic functions satisfying the constraint `(a -> b) & (b -> c)` are quite rare (although I'm sure that you can think of an example).

[1] https://github.com/tomprimozic/type-systems/tree/master/firs...

Edit: although on second thought, just first-class polymorphism isn't enough to fix this... any type system where the function `twice` has the same type as the function `three_times` will exhibit the same problem!

Non-polymorphic functions of the type `a->a` trivially satisfy it, of course. Also, I think polymorphic functions are the most interesting case where you can't use twice as desired in an ML-like language, so it's too bad that despite the fancier type they don't work too well in MLsub. Here's another example that fails when I'd hope for it to succeed:

  let one = twice (fun o -> o.x) { x = { x = 1 } }

It seems that if you try to ascribe the type you wrote to twice you do get (a -> (a & b)) -> a -> b. I suspect this is a direct result of the "extensional" principles used to design the subtyping relation (so that it forms a lattice with nice properties) and I'm not sure whether it would be at all easy to get around. But I could be wrong, I'm still digesting the paper.

(Actually, I think it conceivably might just be a bug in the current typechecker; ascription isn't working for records AFAICT which makes me think they might not be fully baked).

> It's interesting because it's both important and hard.

Is it true that the problem (of type inference) is hard only in the presence of operations or expressions with types? In other words, if a language does not provide operations or expressions with types then it is more or less obvious how to infer types?

It makes some things easier, but you give up principality: without things like intersection types, you end up with programs for which there isn't a "best" type to ascribe them. You can see this in the parent's example: without subtyping constraints or intersection types, there's no way to usefully express the subtyping that is possible in this example. It's generally considered a bad thing if your language infers a type which is incompatible with another type you could have manually written, e.g., (float -> int) -> float -> int, that is also a valid type for the expression. We like there to be a best choice for type inference to pick, but if the type language isn't expressive enough, there won't be one!

It was worth trying:

    class Effable t where
      f :: forall d. Effable d
        => t -> d

    instance intsAreEffable :: Effable Int where
      f x = ???

(This is PureScript, though. Excuse the bad pun.)

Thanks, this is the comment I wanted to "win" the thread. I'm still figuring it out.

>Type inference in the presence of subtyping is so hard that no programming language does it currently.

Hack does some cute stuff in this area. E.g. the type checker postpones inferring the type of empty arrays.

Reply on news.ycombinator.com