<p>As far as I know, there is no "right" or "only" way of associating operations of theorems to mathematical structures. Certainly there is no <strong>canonical</strong> way, and even on paper you often see sentences such as "we write <em>foo</em> instead of <em>foobar</em> when no ambiguity occurs". Even this does not prevent misunderstandings, and often clarification by the author or guesswork by the reader is required.</p>

<p>There has been a lot of work in disambiguating mathematical statements of the kind you describe, especially in mathematical proof assistants like Coq, Isabelle, Mizar, etc., but there are many annoyances in practice, and a lot of compromise to design a disambiguation system which insures:</p>

<ol>
<li>Inferring reasonable statements, i.e. $1+\pi$ should be easy to recognize as a real number</li>
<li>Acceptable performance, i.e. $1+1$ in $\mathbb{N}$ should be recognized nigh-instantaneously, even as part of a much larger expression</li>
<li>Understandable error messages, i.e. $\pi+\mathbb{Z}$ should fail because $\mathbb{Z}$ is not (coercible to) a real number, rather than some crazy failure involving additive structure on quotient sets.</li>
</ol>

<p>I can't understate how important (and difficult) point 3 is: experimentally, it's better to fail predictably than succeed in a bizarre manner, as I'm sure Scala users are aware.</p>

<p>Another issue is that notations like $+$ and $\cdot$ are often used to describe abstract operations like commuative monoids, but also concrete operations on the sets that support them, so if you want to write
$$ \forall\ x\ y\ z,\ (x\cdot y)\cdot z=x \cdot (y\cdot z)$$
for any monoid, you have to imagine instantiating $\cdot$ by addition in the naturals.</p>

<p>In general, the idea of applying an operation to a whole structure rather than just the carrier set is called the <strong>bundled</strong> approach, and it is mostly used in the <a href="http://math-comp.github.io/math-comp/" rel="nofollow">mathematical components</a> library which was used in the recent formalization of the Feit-Thompson theorem in Coq.</p>

<p>One big disadvantage of the bundled approach is that, as you noticed, mathematical sets often carry a great deal of structure, e.g. $\mathbb{R}$ is a group, and a ring and a field (as well as a topological space, and a great many other things) and one wants to exploit the knowledge that the additive group operation of $\mathbb{R}$ is the same as the $+$ operation of the ring, and that the order $\leq$ is compatible with them.</p>

<p>The <strong>unbundled</strong> approach is much more amenable to these kinds of <a href="https://en.wikipedia.org/wiki/Mixin" rel="nofollow">mixins</a>, which are more severe in mathematics than in CS, as <em>properties</em> need to be supported in addition to simply <em>operations</em>.</p>

<p>The Mathematical Components team has written about these issues in the 2009 paper <a href="http://hal.inria.fr/inria-00368403/file/main.pdf" rel="nofollow">Packaging Mathematical Structures</a>, as have we in the context of the <a href="http://leanprover.github.io/about/" rel="nofollow">Lean</a> interactive theorem prover in the paper <a href="http://arxiv.org/abs/1505.04324" rel="nofollow">Elaboration in Dependent Type Theory</a>.</p>

<p>I feel that the question of a reasonable inference mechanism for disambiguation is still a very open question though.</p>

CC BY-SA 3.0
2016-01-25T16:46:23.763Z
2016-01-25T16:46:23.763Z
cody
<p>There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc. </p>

<p>In mathematics however, there are many situations where one set carries the same structure in multiple ways, like the integers being a monoid under both addition and multiplication.  </p>

<p>We normally just give these different names, but potentially one wants to abstract some tougher mathematical function, or a proof done in the type system.  </p>

<p>In principle, one could do this the way mathematicians do it, by applying a type class to a type that associates the operations to the base type, as opposed to just the set itself with a fixed association. </p>

<p>Is that the "right" or "only" way to gain this flexibility?  Or is there something else? </p>

<p>In particular, there are a bunch of languages like Scala that do overloading of overloading rules in a rather dangerously complex ways, well even incoherent instances in Haskell probably.  It'd be interesting if there were clearer "more parametric" way to achieve the ends that motivates those design decisions. </p>

CC BY-SA 3.0
2016-01-23T13:34:16.170Z
Maybe [Isabelle's Haskell-style type classes](https://isabelle.in.tum.de/dist/Isabelle2015/doc/classes.pdf) are of interest?
Martin Berger
CC BY-SA 3.0
2016-01-23T13:36:19.833Z
Oh, and why is scope-based overloading "dangerous"? One perceived disadvantage of Haskell's type classes has been their global nature.
Martin Berger
CC BY-SA 3.0
2016-01-23T16:12:21.897Z
Anything is scope based really, including parametric polymorphic things.  I've edited it to say "dangerously complex" by which I mean using rules humans do not read off easily.
Jeff Burdges
<type-theory><dependent-type><proof-assistants>
Is there a theory of overloading types?
Jeff Burdges
# Is there a theory of overloading types?

(Asked by: username_0 on 2016-01-22)

There is a sound theory of overloading operators and functions realized by type classes in Haskell, and to rougher extent by traits in Rust, etc.

In mathematics however, there are many situations where one set carries the same structure in multiple ways, like the integers being a monoid under both addition and multiplication.

We normally just give these different names, but potentially one wants to abstract some tougher mathematical function, or a proof done in the type system.

In principle, one could do this the way mathematicians do it, by applying a type class to a type that associates the operations to the base type, as opposed to just the set itself with a fixed association.

Is that the "right" or "only" way to gain this flexibility? Or is there something else?

In particular, there are a bunch of languages like Scala that do overloading of overloading rules in a rather dangerously complex ways, well even incoherent instances in Haskell probably. It'd be interesting if there were clearer "more parametric" way to achieve the ends that motivates those design decisions.

**Tags:** type-theory, dependent-type, proof-assistants
> **Comments:**
> **username_1**: Maybe [Isabelle's Haskell-style type classes](https://isabelle.in.tum.de/dist/Isabelle2015/doc/classes.pdf) are of interest?  
> **username_1**: Oh, and why is scope-based overloading "dangerous"? One perceived disadvantage of Haskell's type classes has been their global nature.  
> **username_0**: Anything is scope based really, including parametric polymorphic things.  I've edited it to say "dangerously complex" by which I mean using rules humans do not read off easily.  

---

## 1 answers

### Answer by username_2 on 2016-01-25. Score: 3 | Accepted answer

As far as I know, there is no "right" or "only" way of associating operations of theorems to mathematical structures. Certainly there is no **canonical** way, and even on paper you often see sentences such as "we write *foo* instead of *foobar* when no ambiguity occurs". Even this does not prevent misunderstandings, and often clarification by the author or guesswork by the reader is required.

There has been a lot of work in disambiguating mathematical statements of the kind you describe, especially in mathematical proof assistants like Coq, Isabelle, Mizar, etc., but there are many annoyances in practice, and a lot of compromise to design a disambiguation system which insures:

1. Inferring reasonable statements, i.e. $1+\pi$ should be easy to recognize as a real number
2. Acceptable performance, i.e. $1+1$ in $\mathbb{N}$ should be recognized nigh-instantaneously, even as part of a much larger expression
3. Understandable error messages, i.e. $\pi+\mathbb{Z}$ should fail because $\mathbb{Z}$ is not (coercible to) a real number, rather than some crazy failure involving additive structure on quotient sets.

I can't understate how important (and difficult) point 3 is: experimentally, it's better to fail predictably than succeed in a bizarre manner, as I'm sure Scala users are aware.

Another issue is that notations like $+$ and $\cdot$ are often used to describe abstract operations like commuative monoids, but also concrete operations on the sets that support them, so if you want to write
$$ \forall\ x\ y\ z,\ (x\cdot y)\cdot z=x \cdot (y\cdot z)$$
for any monoid, you have to imagine instantiating $\cdot$ by addition in the naturals.

In general, the idea of applying an operation to a whole structure rather than just the carrier set is called the **bundled** approach, and it is mostly used in the [mathematical components](http://math-comp.github.io/math-comp/) library which was used in the recent formalization of the Feit-Thompson theorem in Coq.

One big disadvantage of the bundled approach is that, as you noticed, mathematical sets often carry a great deal of structure, e.g. $\mathbb{R}$ is a group, and a ring and a field (as well as a topological space, and a great many other things) and one wants to exploit the knowledge that the additive group operation of $\mathbb{R}$ is the same as the $+$ operation of the ring, and that the order $\leq$ is compatible with them.

The **unbundled** approach is much more amenable to these kinds of [mixins](https://en.wikipedia.org/wiki/Mixin), which are more severe in mathematics than in CS, as *properties* need to be supported in addition to simply *operations*.

The Mathematical Components team has written about these issues in the 2009 paper [Packaging Mathematical Structures](http://hal.inria.fr/inria-00368403/file/main.pdf), as have we in the context of the [Lean](http://leanprover.github.io/about/) interactive theorem prover in the paper [Elaboration in Dependent Type Theory](http://arxiv.org/abs/1505.04324).

I feel that the question of a reasonable inference mechanism for disambiguation is still a very open question though.


---

