<p>It is trivial to model <a href="https://en.wikipedia.org/wiki/Tagged_union" rel="noreferrer">sum types</a> using only <a href="https://en.wikipedia.org/wiki/Union_type" rel="noreferrer">union types</a> and <a href="https://en.wikipedia.org/wiki/Product_type" rel="noreferrer">product types</a>: simply add a discriminant. $A + B \cong (0 \times A) \cup (1 \times B)$.</p>

<p>What I am wondering is whether or not there is a concise, practical representation for union types using sum types and product types.</p>

CC BY-SA 3.0
2016-12-25T12:25:12.677Z
I don't think this question is sufficiently precise to be a research-level question, because it's important to define what exactly you mean by a "representation" (let alone a "concise, practical" one). I suspect you might be looking for an implementation along the lines of Joshua Dunfield's "Elaborating Intersection and Union Types" (http://www.cs.cmu.edu/~joshuad/papers/intcomp/).
Noam Zeilberger
CC BY-SA 3.0
2016-12-25T12:27:07.477Z
On the other hand, there is also a simple counterpart to your equation, which basically says that a union is the "image of a sum along the codiagonal map". You could have a look at some notes I wrote (http://noamz.org/oplss16/refinements-notes.pdf) which discuss such equations (see p.70, Equations 3.10 and 3.13) and explains how to interpret them in a very general categorical setting.
Noam Zeilberger
CC BY-SA 3.0
2016-12-26T20:52:48.257Z
I was rather thinking the OP should define what he means by union. Types are not sets, so there's no such thing as union of types, at least not until someone defines it. In fact, the question is ill-posed since it's usng set-theoretic terminology but it speaks about types. That just doesn't make a lot of sense. I am downvoting until this gets fixed.
Andrej Bauer
CC BY-SA 3.0
2016-12-26T22:54:17.533Z
Andrej: saying that "there's no such thing as union of types" is dogmatic and inappropriate, because there is a substantial literature on union types (e.g., check out the bibliography in the Dunfield paper I linked). Don't be mislead by the set-theoretic terminology (which is standard though): the proper way of thinking about intersection and union types is in fibrational terms ("union type" is essentially just another name for "fibered coproduct").
Noam Zeilberger
CC BY-SA 3.0
2016-12-26T22:58:06.373Z
I stand corrected. Alas, I can't change my vote unless the question is edited. Perhaps the question could get rid of the set theory and instead replace it with an appropriate link to union types?
Andrej Bauer
CC BY-SA 3.0
2016-12-26T23:11:47.493Z
I agree that the question is underspecified in multiple ways.
Noam Zeilberger
CC BY-SA 3.0
2016-12-27T16:19:50.500Z
I've updated the question to include links and to use more standard syntax.

I agree that my use "representation" is underspecified, but I'm not sure what other word to use. Apologies for the insufficient formality, I'm still finding my way around PLT.
Carl Patenaude Poulin
CC BY-SA 3.0
2016-12-27T17:27:25.670Z
@NoamZeilberger It's a fairly contentious statement to say that "the proper way of thinking about intersection and union types is in fibrational terms". The problem with a categorical understanding of types is that it rarely generalises well from functional to interactive forms of computation. I'd replace "the proper" by "an interesting".
Martin Berger
CC BY-SA 3.0
2016-12-27T18:42:17.923Z
@CarlPatenaudePoulin Be careful, your new notation is still open to misunderstandings! By "0" and "1", I understand that you mean the values 0 and 1 as "singleton types" refining the integers/booleans, but that should be made explicit because it is an essential element of this encoding. I am still not exactly sure what you mean by a "representation", but do either of the references I mentioned get at what you were looking for?
Noam Zeilberger
CC BY-SA 3.0
2016-12-27T18:49:26.633Z
@MartinBerger you might be right that it's contentious, but I think it is important to demystify these things. The fibrational point of view is very general, and in my experience it captures what people mean when they talk about intersection and union types.
Noam Zeilberger
CC BY-SA 3.0
2016-12-27T21:25:37.793Z
"Untagged union as fibered coproduct" is a great answer to the question I was trying to ask, though at a slightly higher level of abstraction than I hoped for. I think Joshua Dunfield's paper might elucidate this for me, though I need to re-read it to make sure.

One thing I'm not sure how to fix is the use of $0$ and $1$ to represent distinct singleton terms. I understand the potential confusion between $0$ and the empty type, but is there a standard notation for distinct singleton types?
Carl Patenaude Poulin
CC BY-SA 3.0
2016-12-27T21:25:46.593Z
Thank you so much Noam for deconstructing this question, just your out-loud interpretation is helping me figure out exactly what I'm looking for.
Carl Patenaude Poulin
CC BY-SA 3.0
2016-12-27T21:29:17.800Z
Addendum: is there a connection between fibered coproducts and topological fibrations?
Carl Patenaude Poulin
CC BY-SA 3.0
2016-12-28T09:21:32.537Z
There isn't a standard notation for singleton types, and you'll even find some disagreement about what exactly singleton types *are* (just as there is some disagreement about what exactly are union types). For navigating these topics, it is extremely helpful (again, IMO) to keep in mind the distinction between a "type" and "type refinement". All of these constructs (unions, singletons, etc.) really fall under the "type refinement" rubric. Another ref that you might find useful here is Rowan Davies' thesis, "Practical Refinement-Type Checking" (https://www.cs.cmu.edu/~rwh/theses/davies.pdf).
Noam Zeilberger
CC BY-SA 3.0
2016-12-28T09:28:36.957Z
Re: fibrations, the fibrational view of typing I alluded to is related to the concept of a "categorical fibration", which is indeed a generalization of the concept of fibration from topology. This view is explained in more detail in Chapter 3 of the OPLSS notes I linked to (as well as in the references mentioned there).
Noam Zeilberger
CC BY-SA 3.0
2016-12-28T13:16:46.523Z
@NoamZeilberger  Can you sketch how the fibrational POV is general enough (or rather, has "the right generality") to give convincing accounts of union and intersection types for interaction (e.g. as given by session types, or Kobayashi et al linear types, or Honda et al "uniform type structure" types)?
Martin Berger
CC BY-SA 3.0
2016-12-28T14:15:50.263Z
@MartinBerger I don't know enough about session types to answer that, but when I have more time I'll try to think about it and send you an email.
Noam Zeilberger
<type-theory><model-theory>
Modeling union types using sum types
Carl Patenaude Poulin
# Modeling union types using sum types

(Asked by: username_0 on 2016-12-25)

It is trivial to model [sum types](https://en.wikipedia.org/wiki/Tagged_union) using only [union types](https://en.wikipedia.org/wiki/Union_type) and [product types](https://en.wikipedia.org/wiki/Product_type): simply add a discriminant. $A + B \cong (0 \times A) \cup (1 \times B)$.

What I am wondering is whether or not there is a concise, practical representation for union types using sum types and product types.

**Tags:** type-theory, model-theory

> **Comments:**
> **username_1**: I don't think this question is sufficiently precise to be a research-level question, because it's important to define what exactly you mean by a "representation" (let alone a "concise, practical" one). I suspect you might be looking for an implementation along the lines of Joshua Dunfield's "Elaborating Intersection and Union Types" (http://www.cs.cmu.edu/~joshuad/papers/intcomp/).  
> **username_1**: On the other hand, there is also a simple counterpart to your equation, which basically says that a union is the "image of a sum along the codiagonal map". You could have a look at some notes I wrote (http://noamz.org/oplss16/refinements-notes.pdf) which discuss such equations (see p.70, Equations 3.10 and 3.13) and explains how to interpret them in a very general categorical setting.  
> **username_2**: I was rather thinking the OP should define what he means by union. Types are not sets, so there's no such thing as union of types, at least not until someone defines it. In fact, the question is ill-posed since it's usng set-theoretic terminology but it speaks about types. That just doesn't make a lot of sense. I am downvoting until this gets fixed.  
> **username_1**: Andrej: saying that "there's no such thing as union of types" is dogmatic and inappropriate, because there is a substantial literature on union types (e.g., check out the bibliography in the Dunfield paper I linked). Don't be mislead by the set-theoretic terminology (which is standard though): the proper way of thinking about intersection and union types is in fibrational terms ("union type" is essentially just another name for "fibered coproduct").  
> **username_2**: I stand corrected. Alas, I can't change my vote unless the question is edited. Perhaps the question could get rid of the set theory and instead replace it with an appropriate link to union types?  
> **username_1**: I agree that the question is underspecified in multiple ways.  
> **username_0**: I've updated the question to include links and to use more standard syntax.  I agree that my use "representation" is underspecified, but I'm not sure what other word to use. Apologies for the insufficient formality, I'm still finding my way around PLT.  
> **username_3**: @NoamZeilberger It's a fairly contentious statement to say that "the proper way of thinking about intersection and union types is in fibrational terms". The problem with a categorical understanding of types is that it rarely generalises well from functional to interactive forms of computation. I'd replace "the proper" by "an interesting".  
> **username_1**: @CarlPatenaudePoulin Be careful, your new notation is still open to misunderstandings! By "0" and "1", I understand that you mean the values 0 and 1 as "singleton types" refining the integers/booleans, but that should be made explicit because it is an essential element of this encoding. I am still not exactly sure what you mean by a "representation", but do either of the references I mentioned get at what you were looking for?  
> **username_1**: @MartinBerger you might be right that it's contentious, but I think it is important to demystify these things. The fibrational point of view is very general, and in my experience it captures what people mean when they talk about intersection and union types.  
> **username_0**: "Untagged union as fibered coproduct" is a great answer to the question I was trying to ask, though at a slightly higher level of abstraction than I hoped for. I think Joshua Dunfield's paper might elucidate this for me, though I need to re-read it to make sure.  One thing I'm not sure how to fix is the use of $0$ and $1$ to represent distinct singleton terms. I understand the potential confusion between $0$ and the empty type, but is there a standard notation for distinct singleton types?  
> **username_0**: Thank you so much Noam for deconstructing this question, just your out-loud interpretation is helping me figure out exactly what I'm looking for.  
> **username_0**: Addendum: is there a connection between fibered coproducts and topological fibrations?  
> **username_1**: There isn't a standard notation for singleton types, and you'll even find some disagreement about what exactly singleton types *are* (just as there is some disagreement about what exactly are union types). For navigating these topics, it is extremely helpful (again, IMO) to keep in mind the distinction between a "type" and "type refinement". All of these constructs (unions, singletons, etc.) really fall under the "type refinement" rubric. Another ref that you might find useful here is Rowan Davies' thesis, "Practical Refinement-Type Checking" (https://www.cs.cmu.edu/~rwh/theses/davies.pdf).  
> **username_1**: Re: fibrations, the fibrational view of typing I alluded to is related to the concept of a "categorical fibration", which is indeed a generalization of the concept of fibration from topology. This view is explained in more detail in Chapter 3 of the OPLSS notes I linked to (as well as in the references mentioned there).  
> **username_3**: @NoamZeilberger  Can you sketch how the fibrational POV is general enough (or rather, has "the right generality") to give convincing accounts of union and intersection types for interaction (e.g. as given by session types, or Kobayashi et al linear types, or Honda et al "uniform type structure" types)?  
> **username_1**: @MartinBerger I don't know enough about session types to answer that, but when I have more time I'll try to think about it and send you an email.  

---

## 0 answers

