For several years I have been designing and implementing a functional teaching language especially for use in the context of a Discrete Mathematics course. The idea is for students to be exposed to some functional and staticallytyped programming early in their computer science education, and to give them a fun and concrete way to see the connections between the concepts they learn in a Discrete Math course and computation. I am not the first to think of combining FP + Discrete Math, but I think there is an opportunity to do it really well with a language designed expressly for the purpose. (And, who am I kidding, designing and implementing a language is just plain fun.)
Of course the language has an expressive static type system, with base types like natural numbers, rationals, Booleans, and Unicode characters, as well as sum and product types, lists, strings, and the ability to define arbitrary recursive types. It also has builtin types and syntax for finite sets. For example,
A : Set ℕ
A = {1, 3, 6}
(Incidentally, I will be using Unicode syntax since it looks nice, but there are also ASCII equivalents for everything.) Sets support the usual operations like union, intersection, and difference, as well as set comprehension notation. The intention is that this will provide a rich playground for students to play around with the basic set theory that is typically taught in a discrete math class.
But wait…
Hopefully the above all seems pretty normal if you are used to programming in a statically typed language. Unfortunately, there is something here that I suspect is going to be deeply confusing to students. I am so used to it that it took me a long time to realize what was wrong; maybe you have not realized it either. (Well, perhaps I gave it away with the title of the blog post…)
In a math class, we typically tell students that is a set. But in Disco, ℕ
is a type and something like {1,2,3}
is a set. If you have been told that is a set, the distinction is going to seem very weird and artificial to you. For example, right now in Disco, you can ask whether {1,2}
is a subset of {1,2,3}
:
Disco> {1,2} ⊆ {1,2,3}
true
But if you try to ask whether {1,2}
is a subset of ℕ
, you get a syntax error:
Disco> {1,2} ⊆ ℕ
1:10:

1  {1,2} ⊆ ℕ
 ^
keyword "ℕ" cannot be used as an identifier
Now, we could try various things to improve this particular example—at the very least, make it fail more gracefully. But the fundamental question remains: what is the distinction between types and sets, and why is it important? If it’s not important, we should get rid of it; if it is important, then I need to be able to explain it to students!
We could try to completely get rid of the distinction, but this seems like it would lead directly to a dependent type system and refinement types. Refinement types are super cool but I really don’t think I want to go there (Disco’s type system is already complicated enough).
However, I think there actually is an important distinction; this blog post is my first attempt at crystallizing my thoughts on the distinction and how I plan to explain it to students.
Types vs sets
So what is the difference between sets and types? The slogan is that types are intensional, whereas sets are extensional. (I won’t actually use those words with my students.) That is:
 Sets are characterized by the relation: we can ask which items are elements of a set and which are not.
 Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.
This seems kind of symmetric, but it is not. You can’t ask whether a thing is an element of a set if you don’t know how to even make or talk about any things in the first place. So types are prior to sets: types provide a universe of values, constructed in orderly ways, that we can work with; only then can we start picking out certain values to place them in a set.
Of course, this all presupposes some kind of type theory as foundational. Of course I am aware that one can instead take axiomatic set theory as a foundation and build everything up from the empty set. But I’m building a typed functional programming language, so of course I’m taking type theory as foundational! More importantly, however, it’s what almost every working mathematician does in practice. No one actually works or thinks in terms of axiomatic set theory (besides set theorists). Even in a typical math class, some sets are special. Before we can talk about the set , we have to introduce the special set so we know what , , and are. Before we can talk about the set we have to introduce the special Cartesian product operation on sets so we know what tuples are. And so on. We can think of types as a language for describing this prior class of special sets.
Explaining things to students
So what will I actually say to my students? First of all, when introducing the language, I will tell them about various builtin primitive types like naturals, rationals, booleans, and characters. I won’t make a big deal about it, and I don’t think I will need to: for the most part they will have already seen a language like Python or Java with types for primitive values.
When we get to talking about sets, however (usually the second unit, after starting with propositional logic), we will define sets as collections of values, and I will explicitly point out the similarity to types. I will tell them that types are special builtin sets with rules for building their elements. We will go on to talk about disjoint union and Cartesian product, and practice building elements of sum and product types. (When we later get to recursion, they will therefore have the tools they need to start building recursive types such as lists and trees.)
The other thing to mention will be the way that when we write the type of a set, as in, Set ℕ
, we have to write down the type of the elements—in other words, the universe, or ambient set from which the elements are chosen. When introducing set theory, traditionally one mentions universe sets only when talking about the set complement operation; but the fact is that mathematicians always have some universe set in mind when describing a given set.
Now, coming back to the example of {1,2} ⊆ ℕ
, it would still be confusing for students if this is a syntax error, and I have some ideas about how to make it work. Briefly, the idea is to allow types to be used in expressions (but not the other way around!), with T : Set T
. If I tell them that types are special sets, then logically they will expect to be able to use them as such! However, this is an extremely nontrivial change: it means that Disco would now be able to represent infinite sets, requiring sets to be internally represented via a deep embedding, rather than simply storing their elements (as is currently the case). For example, 2 ∈ (ℕ \ {3,5})
should evaluate to true
, but we obviously can’t just enumerate all the elements of ℕ \ {3,5}
since there are infinitely many. More on this in a future post, perhaps!
Hi! I very much agree that this is an important and natural distinction to make. You mentioned potentially “getting rid of the distinction” via dependent types and refinement types, though I actually like to think of type refinement systems in the broad sense as based on this very distinction, i.e., starting from a layer of “intrinsic” types, and then building a layer of “extrinsic” types on top of that. I wrote a paper with PaulAndré Melliès where we tried to explain how to map this perspective onto a very simple categorical model that perhaps you would find evocative (we certainly used some similar language to what you are using).
Otherwise, I think teaching discrete math this way via programming is a great idea! Out of curiosity, have you ever interacted with Michael Greenberg? A couple years ago I heard him give a talk about teaching discrete mathematics to early undergraduates using Coq, and I see that now he even has some parts of a book online.
Hi Noam, thanks very much for the comment and for the link to your paper! I will definitely give it a read.
I know Michael well, we did our PhDs together at U Penn. We were both TAs for CIS 500, Software Foundations, and contributed to https://softwarefoundations.cis.upenn.edu/ , which had a strong influence on both of our ideas about the intersection of math, CS, and pedagogy (although we have obviously gone different directions with it!). I really like what Michael has done using Coq to teach formal and informal proof. A longterm goal for Disco is to be able to use it as a basis for doing formal proofs as well — perhaps by exporting to Lean or something like that.
What do you want from Disco? I see two main options that are pretty strongly opposed to each other.
The first alternative is that you want Disco to be a programming language and expressions like `{1, 2} ⊆ x` to be things that your interpreter can evaluate to true or false. In this case, I would 1) rename Set to FinSet, 2) probably describe FinSet as the free commutative idempotent monoid (maybe not in those words depending on your audience) which naturally fits in with Bag (free commutative monoid) and List (free monoid), 3) I would go out of my way to continually emphasize that types and the FinSet type (constructor) are not (ZFC) sets, and that FinSet does NOT correspond to finite (ZFC) sets. With this your problematic example is not problematic but rather a learning opportunity. (It’s doubly not problematic because ℕ isn’t a finite (ZFC) set.)
The second alternative is that you want DIsco to be a language for describing and proving things about combinatorial objects. That is, you want the experience of working with Disco to be like doing Discrete Math homework. An expression like `{1, 2} ⊆ x` would now be something you need to prove rather than something that can be evaluated. In this case, Disco would just be a specification language, basically an “applied” FOL, with a theorem prover attached. This approach does allow identifying `Set X` with the (ZFC) set of subsets of X and experience that’s essentially the same as proving things about sets in mathematics.
My impression is that you want the first approach (or at least the current form of Disco corresponds to the first approach) with, down the line, an additional theorem proving layer on top. This theorem proving layer would be proving things about Disco programs which is different from and a different experience from proving things about ZFC sets. Either way it wouldn’t change what the semantics of the the Disco programming language were, i.e. `Set X` would still not have much to do with (finite) (ZFC) sets.
What bothers me is that, despite understanding these distinctions, you seem to want to obscure them as much as possible, even going so far as to significantly twist Disco just to make the conflation more plausible. Why this bothers me is that this conflation creates and/or compounds various common confusions about the nature of (ZFC) sets. It falsely reinforces the idea that finite (ZFC) sets can have their elements enumerated, and can be computed with, and *are* a “collection” of elements.
Thanks so much for your comment, this is hugely helpful!
I definitely want the first option: a real programming language that computes stuff. You’re right that the things I’m calling sets are free commutative idempotent monoids, and indeed, the language has bags and lists too, with some machinery for going back and forth between them (i.e. adjunctions). However, I’m not sure I understand why you say they have to be finite. The free commutative idempotent monoid on an infinite carrier set can have infinite elements, can’t it?
To be clear, my audience is beginning undergraduates. They have absolutely no idea what ZFC set theory is, nor would they care if I told them. And I don’t care about ZFC set theory either: I want to teach them naive set theory as it is used in basic computer science and mathematics. If the thing I teach them is subtly incompatible with ZFC set theory, but gives them a good sense for how to use ideas about sets in practice, that is perfectly fine with me.
“despite understanding these distinctions”: I think you overestimate my level of understanding. I have taken a graduatelevel course in axiomatic set theory, but I have honestly never given too much thought to its computational content (or lack thereof).
Supposing that we take “sets” in Disco to be elements of (finite) idempotent commutative monoids; can you say more about what goes wrong if you try to prove things about them? I.e. why can’t Disco both have computational content AND be a specification language? Where is the mismatch? Sorry if it is obvious but I’ve really never thought about it before.
The free commutative idempotent monoid doesn’t have to be finite, but the “finite sets” are, as you say, the *elements* of the free commutative monoid. Those will be finite regardless of the cardinality of the generating set. That is, the *type* FinSet X is *the* free commutative idempotent monoid generated from X, and it’s values are the “finite sets with elements in X”.
The question is what you mean by “use ideas about sets in practice”. If you are thinking of using sets like a programmer would, e.g. a la using Haskell’s Data.Set, then the question is: why do you need try to identify types with sets even partially? On the other hand, if by “use ideas about sets in practice” you mean “how mathematician’s manipulate and prove things sets and use them to model things”, then the “data structure” view of sets not only doesn’t correspond with mathematical sets, they also aren’t used in the same way. For actual, mathematical “working with” (mathematical) sets, we are generally working with the property that defines that set. Roughly speaking[1], we identify the set S with the class P(x) x ∈ S. In practice, elements of S will be identified by some formula, i.e. we’ll have x ∈ S ϕ(x) where ϕ is some firstorder formula. In this context, proving S ⊆ T is about proving through logical manipulation that ϕ => ψ where ψ characterizes elements of T. This “propertybased” view doesn’t suggest that you can enumerate the elements of S or that S is “made up” of its elements. The Data.Set view of sets does imply these things which are true for the Data.Set notion of set.
As you did a good job articulating, types and mathematical sets are distinct. I’m confident you would readily agree that types and computational sets are distinct. Mathematical sets and computational sets are also distinct. If you are solely interested in the programming style of usage of (computational) sets, then mathematical sets are irrelevant. Floating or suggesting the idea that “types are sets” is then strange and confusing because 1) it’s false, and 2) the closer fit (and presumably the intent) would be “types are mathematical sets” but these mathematical sets are different from the computational sets your language includes. If you are interested in the mathematical sets, then types and computational sets are irrelevant except that it is probably worthwhile to explicitly contrast them, because I feel that many introductions to mathematical sets are like “you know those finite (computational) sets you’ve probably seen earlier in your education, well set theory sets are just those but we allow infinite elements” which, in my opinion, leads to a lot of confusion at both the philosophical and practical levels.
Given that mathematical sets, computational sets, and types are all distinct, in my mind, it makes the most pedagogical sense to avoid doing anything that would hide that difference. In my mind, apparent similarities should only be brought up to show why they break down. Types are not “collections of values”, let alone computational sets of values. This already starts to become apparent with a type like ℕ which has an unbounded number of values, and becomes more clear with function types, and eventually becomes decisive with types that are not hsets in HoTT. Obviously, I don’t think you should talk about HoTT. The simplest solution is to say nothing: don’t talk about the distinctions but also don’t suggest that there might be a connection. I think this is fine. Purely personally, I would talk about some or all of these distinctions to try (probably futilely) to nip these conflations in the bud, because I have little faith that they won’t be intentionally or unintentionally introduced by future educators or texts.
There is no problem with proving things about Disco programs. You could write a program like `subsetUnion x y = x ⊆ x ∪ y` and then prove that it returns true on all inputs given a semantics for Disco. This would likely be (significantly) more difficult than proving the analogous formula of ZFC as you would be proving something about the evaluation of Disco programs, not a fact about finite sets. Trying to make Disco simultaneously be a programming language and a specification language is likely to result in way too weak of a specification language, or you will have something you can’t compute with. For example, while `subsetUnion A B` could be reduced to a boolean where A and B are explicit terms, the formula `forall x y. x ⊆ x ∪ y` can’t with a straightforward implementation of sets. Your deep embedding idea would get you further, basically passing that formula to an SMT solver, say, at runtime. I don’t think this will get you where you want and you will likely quickly leave the decidable theories an SMT solver can handle. It might still be an interesting thing to explore for its own sake.
Or, you’ll do something like dependent types which would still lead to a “programming language”/”specification language” split roughly along the lines of terms versus types. Maybe you could use some (logical) reflection techniques to connect these more, i.e. to connect the outcome of evaluating some expressions to propositionsastypes, but I don’t know how well that would work out and I don’t imagine the experience of proving things in this style would match what you want.
Possibly, if you constrain Disco enough (e.g. making it total) and/or don’t care about soundness, you could give it a denotational semantics that interprets things in the “obvious” way. You could then (conceptually) do an extension by definitions to ZFC (or better in Mizar) defining the named values of the program as their denotations. You could then run the programs as usual, but also “prove” things about the program as well. This would probably be pretty hard to do in a sound way, especially if Disco supports higherorder functions. Maybe you could have an unsound denotation that was “good enough” for the examples you cared about.
[1]: Of course, this propertybased view of sets is still not the axiomatic view in which sets are the unidentified things ZFC is talking about and more like atomic nodes in a (settheoretic) directed graph than “compound” objects.
Thanks so much for this detailed reply. I will definitely have to chew on this for a while.
One thing I will mention is that it is already possible to write things like `forall x y. x ⊆ x ∪ y` in Disco, as an expression of type `Prop`. Computationally, it will do a QuickCheckstyle test where it will report that it failed to find a counterexample in some number of random tests, but obviously it cannot definitively compute to True or False. I’m definitely not interested in proving things about the evaluation of this expression as a Disco program, i.e. proving that it will always evaluate to True for any inputs. My thinking has been along the other lines you suggest, i.e. reflecting it to the obviously corresponding statement of firstorder logic and trying to prove that with some external proof assistant. Of course, ideally we would want some kind of soundness property which says something like “if the logical translation of S is provable, then S does not compute to False”. I am curious what the soundness difficulties would be given that Disco does indeed support higherorder functions.
Can you do things like `if (forall x y. x ⊆ x ∪ y) then 1 else 0` or is there a separate Bool type?
As for some of the potential issues with soundness, if we (have Disco be total… and) interpret a function type like ℕ > ℕ as the set of functions ℕ > ℕ, then the issue we have is that “most” of those functions don’t have a corresponding Disco program. That’s fine for interpreting a Disco program into that set. It becomes problema tic if (ℕ > ℕ) > ℕ is interpreted naively because then (the interpretation of) our Disco program needs to be able to handle arbitrary set theoretic functions as inputs. As a simple example, a statement like `exists f: ℕ > Bool. P(f)` then `P(f)` could hold only for uncomputable functions, and thus the statement is true in the interpretation but would be false for Disco programs. To be clear, this is the notion of soundness that applies to denotational semantics (not the logical one) and so is relating to an operational semantics. I’m not really sure what your operational semantics would be. To (try to) be clear, the problem is if `exists f.P(f)` is part of the language then we need to provide a denotation for it, and the naive settheoretic denotation of this expression is unlikely to match the operational semantics. There is no issue by itself with “extra” elements (e.g. uncomputable functions) being in our semantic domain. For example, there is no issue at all with interpreting a (total but applied) simply typed lambda calculus in a “naive” set theoretic way, even though there’s no way of writing uncomputable functions in the STLC. It’s fine because there is no STLC term that could “detect” them.
Again, if these formulas are somewhat separated from the “computing parts” of Disco, then this isn’t a problem (though, you’ll probably still struggle to get a “simple” semantics for a relatively rich, full Turingcomplete language).
(This is really a reply to Derek’s last comment, it seems WordPress won’t allow more nesting.)
Can you do things like `if (forall x y. x ⊆ x ∪ y) then 1 else 0` or is there a separate Bool type? No, that would be a type error, there is a separate Bool type.
OK, yes, I understand the issue now. I don’t *think* it’s a problem for the way I have things set up. But you’ve helped immensely in crystallizing all these ideas for me, and I’ll definitely need to spend more time thinking things over.
It may be worth pointing out some things for the students:
– Finite sets are usually what we care about computationally. ℕ is not a finite set, so it doesn’t make sense to ask whether {1, 2, 3} is a (finite set) subset of ℕ.
– Infinite sets are interesting mathematically too, allowing you to talk about “the set of all numbers”, and mathematicians sometimes (perhaps confusingly) refer to that (infinite) set as ℕ.
– How could you represent an infinite set computationally? One approach is via membership functions, where InfSet ℕ is actually just the arrow type ℕ > Bool. Then you can define the set of all numbers (“ℕ”) as being the function that returns true for every input. Interesting assignment questions might arise around defining various operations like union and intersection for infinite sets represented this way.
– Countable and uncountable infinities can then be described in terms of isomorphisms?
Thanks for the comments! All great ideas.