form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these