Types versus sets in math and programming languages
This strikes me as a quite language-specific treatise, and may indicate a shortcoming or particularity of the syntax or semantics of the described programming language (i.e., Disco) rather than an essential conceptual difference.<p>For comparison, in Prolog, a <i>type</i> is indeed a <i>set</i> of terms! For example, the type &quot;integer&quot; truly denotes the set of integers, and if an argument has the type &quot;integer&quot;, then we know that the predicate can only hold if that argument is an element of this type.<p>Quoting from the Prolog ISO standard:<p><pre><code>    7.1 Types

    The type of any term is determined by its abstract syntax
    (6.1.2).

    Every term has one of the following mutually-exclusive
    types: V (variables), I (integers), F (floating point values),
    A (atoms), CT (compound terms).

    A term with type I, F, or A is an atomic term.
</code></pre>
and further:<p><pre><code>    7.1.2 Integer

    An integer is a member of a set I (see 6.1.2 c) where I
    is a subset of ℤ characterized by one or three parameters.
</code></pre>
Prolog also has <i>type errors</i>: <i>&quot;There shall be a Type Error when the type of an argument or one of its components is incorrect, but not a variable.&quot;</i> For example, in Scryer Prolog, we get:<p><pre><code>   ?- length(Ls, a).
   caught: error(type_error(integer,a),length&#x2F;2)
</code></pre>
This is because the second argument of length&#x2F;2 must be an element of the set <i>I</i> of <i>integers</i>. Since the atom &#x27;a&#x27; is not an integer, the relation does not hold in this case. Declaratively, a <i>type error</i> is equivalent to <i>silent failure</i>: It means that the relation cannot hold for this type of argument, and so every specialization of the query will also not hold, whereas a generalization or an instantiation with a term of a different type may succeed.<p>This view readily carries over to logic variables. For example, using library(clpz), we get:<p><pre><code>    ?- X #&gt; 3.
       clpz:(X in 4..sup).
</code></pre>
And we get a <i>type error</i> if we try to instantiate the thus constrained variable X to a term that is not an element of ℤ:<p><pre><code>    ?- X #&gt; 3, X = a.
    caught: error(type_error(integer,a),unknown(a)-1)
</code></pre>
So, indeed, <i>types</i> denote <i>sets</i> of terms that are acceptable as arguments.<p>The example in the article, i.e., ℕ, could be regarded as an element of the set of <i>atoms</i> in Prolog, and therefore have the <i>type</i> atom. In indeed, for example Trealla Prolog answers:<p><pre><code>    ?- atom(ℕ).
    true.</code></pre>