It means check both ways Gamma |- e => t Given Gamma (the environment) and e, you want to derive the type t (bog standard type inference). The other dire

It means check both ways Gamma |- e => t Given Gamma (the environment) and e, you want to derive the type t (bog standard type inference). The other direction also holds: Gamma |- e <= t Now we want to ensure that e conforms to type t. Consider for example, a function: func foo(a) b and an expression that we know the type of already: e <= a Therefore we can say when we apply `foo` onto `e`, we'll yield something of type `b` In effect, you perform 2 passes: forwards inference, and then backwards inference. p/s: I'm not actually a PL person. This is from my casual reading, so my understanding is highly probably very wrong