Polymorphic functions with set-theoretic types part 1: Syntax, semantics, and evaluation