I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that everybody defines sum types in the same way, and they way the language is extended to accommodate this new type includes the following typing rules:

  • if $\sigma$ and $\tau$ are types, then $\sigma+\tau$ is a type
  • if $M$ is of type $\sigma$, then $\operatorname{inl} M$ is of type $\sigma+\tau$
  • symmetrically for $\operatorname{inr}$, if $M$ is of type $\tau$, then $\operatorname{inr} M$ is of type $\sigma+\tau$.

However, suppose I have two sum types, $\sigma+\tau$ and $\sigma+\phi$, and also that $M$ is of type $\sigma$. Then it is not clear what the type of $\operatorname{inl} M$ is.

Is there something I missed, or is this really how sum types work? Because it would be quite easy to actually "fix" the definition to allow one to immediately infer the type of $\operatorname{inl} M$ in the example above -- just include the sum type in the annotation:

$\operatorname{inl_{\sigma+\tau}} M$ is, of course, of type $\sigma+\tau$.

But this is not what is usually done. Why? (Or is it actually done, implicitly?)

  • 2
    $\begingroup$ I think the 'Sums and Uniqueness of Types' section (p. 134) in the book contains several answers to this question. $\endgroup$ Apr 17 '16 at 17:35
  • $\begingroup$ @Anton Trunov: I see, I ha dread several course notes and then started Pierce-s section on sums, but hadn't gotten that far. It's clear not that it is indeed ambiguous, and that there are ways to remove ambiguity. Thank you! $\endgroup$
    – josh
    Apr 17 '16 at 17:55

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\sigma + \tau$ for any $\tau$. The names of type variables don't matter, what matters is where else are you using the same type variable.

  • 2
    $\begingroup$ This is a good observation, though it does mean you have to give up the notion that every term has one specific type. Most programming languages that deal with this parameterize inl in some way, effectively making separate inls for the different resulting sum types, though Scala does in fact do exactly what you suggest via variance. $\endgroup$
    – Owen
    Apr 18 '16 at 2:36

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.