I don’t fully understand it myself, but this seems like a good introduction: https://people.mpi-sws.org/~joshua/bitype.pdf https://people.mpi-sws.org/~joshua/b

I don’t fully understand it myself, but this seems like a good introduction: https://people.mpi-sws.org/~joshua/bitype.pdf https://people.mpi-sws.org/~joshua/bitype.pdf edit: but it’s incomplete: it never gets around to discussing subtyping and thus helping justify its existence. I think the main point is that due to subtyping and other complexities, we may not be able to synthesize the type of an expression just by looking at it, but if its type has been determined by other constraints, we can still check that that type is valid for the expression.