Dear Ignat, In the paper you linked to one should state more clearly that the two graph operations overlay and connect use an implicit equivalence relation between vertices of the two graphs involved. So these operations can be thought of as a traditional algebraic operation followed by a quotient. You might want to learn about domain semantics in general and domain environments in particular. Big names are Dana Scott and Gordon Plotkin, to name just two. Domain theory is the science of assigning (via a functor) an object of a category of partially ordered sets to each type of a (typed) lambda calculus and to each term of the calculus an arrow of that category. It turns out that algebraic domains are suitable for representing programs on algebraic data types. And if the category is just right and the lambda calculus is rich enough, then one can go the other way: Then you can prove that for each arrow in the category of domains there is a program that has that arrow as semantics. Algebraic domains match very nicely the way we build up complex data types via tuples, sums, function types and type recursion and how we build up functions via pattern matching and recursion. And every finite algebraic domain is a directed cycle-free graph. The little (free online) book by Thomas Streicher [1] might be a good start on domain semantics. A comprehensive mathematical theory of domains (not only algebraic ones) can be found in [2] but that book is expensive and hard to obtain. Sadly, with vanilla type systems such as Haskell's you can specify only algebraic domains. Anything beyond that is via "soft" definitions, meaning it can not be expressed in the type system, as you already observed. And domain theory provides mathematical proofs for this fact. Representing types like the prime numbers is possible with dependently- typed languages, but as far as I know these languages can also not go beyond algebraic domains, anyone please correct me if I'm wrong. Of course people have thought about representing other structures that are not algebraic domains. There are at least two ways I can think of: (1) What you call a sub-type: A subset of an algebraic domain. If the sub-type in question somehow sits "at the top" of the domain, then the surrounding algebraic domain is called a domain environment of the type in question. For example, the infinite binary tree is a domain environment of the type of infinite binary sequences. The important question to ask youself here is whether the sub-type is a computable one or not [*]. So if A is an algebraic data type, can you write a program that, given x :: A decides whether x is a member of the sub- type? For example, the sub-type of total functions A -> B is not a computable sub-type of the type of all functions A -> B for general A and B. (2) Quotients of algebraic domains. That means each element of your target type has several (maybe infinitely many) representations in an algebraic domain. This is fairly common. The Double data type has two representations for zero, because each Double value has a sign bit. If you want a set functor, take any container like [] or Seq and disregard multiplicities, so [x,y] and [x,y,y] represent the same set {x,y}. The art is then to write functions f that respect these quotients. Meaning if the values x and y both represent the same element in the quotient, then f(x) and f(y) represent the same element again. See section 4.2 in your linked paper on the problem of whether equivalence classes are computable. A stronger notion is a retract, that is a quotient map q :: A -> D together with a function e :: D -> A that embeds the type D back into the algebraic domain A such that q.e = id and q and e are adjoints. It is known that the retracts of algebraic domains are precisely the so- called continuous domains, a wide class that encompasses for example a real numbers object. Now you may also want to combine (1) and (2) and represent your data type as a quotient of a sub-set of an algebraic domain. As I see it your paper describes just that. It is still an open question whether certain continuous domains can be represented via expanding systems of finite domains, as is the case with algebraic domains [**]. My gut feeling is that such a description involves a description of quotients, but on another level: Since any quotient of a finite domain is algebraic, limits of such quotients will not take you beyond algebraic domains. Instead, one must describe what the quotient q :: A -> D does to the finite parts of A. Regards, Olaf [1] https://b-ok.org/book/768876/241ddb [2] Continuous lattices and domains, ISBN 0-521-80338-1 [*] One can prove that while there are uncountably many subsets of natural numbers, there are only countably many computable subsets in the sense that there exists a program that decides membership. [**] Give me any Haskell type and I show you the system of retractions of finite types whose limit is this type.