The word "type" is very overloaded. In the language of type theory, Prolog (and many other languages, usually dynamic) consider a universal type of all terms,

The word "type" is very overloaded. In the language of type theory, Prolog (and many other languages, usually dynamic) consider a universal type of all terms, and then a "type" is a set on the universal type. This is a fine way to go (though you can get contradictions in the form of infinite loops in typechecking if "types" are terms themselves). In type theory, at least for the ones many theoreticians seem to be interested in, the has_type/2 predicate (using Prolog terminology) is a function, which is to say has_type(x, y) has a single value for y for any given term x. Things are set up so that the way in which x is represented (i.e., constructed) determines y. This is useful computationally because if you know something's type, you then know how to deconstruct it into components. For example, types drive the expected cases of a match expression. My main point with this comment is to bring up the fact that the article is talking about type theories as academics who study functional programming languages see them, so in context it's not specific to Disco. (I should mention that has_type is only a function given a symbolic representation of a construction for x. Theoretically, things of different types can have the same internal representation, like with Java generics or C structs, but I think you can always arrange things so that has_type is a function by tagging values with their type. Even in more delicate dependent type systems.) (I guess I should mention that my understanding of types after some years of confusion is that in the end they essentially provide an API for values. The program code sort of constitutes a proof that a value has a specific type, and then you can interact with it as such. It's explicitly not part of the API for a type to be able to tell whether something has that type -- in many type theories, values can have multiple types! Sets on the other hand are a type where part of their API is that values can determine whether or not a value is an element. It's certainly possible to fuse the concepts so that types are required to be sets, but I think this is avoided because there's not always an algorithm for the set interface.)