It is trivial to model sum types using only union types and product types: 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.

  • 2
    $\begingroup$ 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" (cs.cmu.edu/~joshuad/papers/intcomp). $\endgroup$ – Noam Zeilberger Dec 25 '16 at 12:25
  • 1
    $\begingroup$ 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 (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. $\endgroup$ – Noam Zeilberger Dec 25 '16 at 12:27
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Dec 26 '16 at 20:52
  • 1
    $\begingroup$ 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"). $\endgroup$ – Noam Zeilberger Dec 26 '16 at 22:54
  • 2
    $\begingroup$ @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. $\endgroup$ – Noam Zeilberger Dec 28 '16 at 14:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.