<p>In type theoretic presentations of programming languages, we usually define an elimination principle similar to a function for inductive types, and we assume pattern matchings to be <em>elaborated</em> into the eliminators. In practical implementations like in Agda/Haskell, we have pattern matching in the core language. Some languages impose eliminators, and really do the translation under the hood, such as Coq/Lean.</p>
<p>What are the benefits of each of these methods?</p>

<types>
What are the pros and cons of eliminators vs. pattern matching with a termination checker?
CC BY-SA 4.0
2023-05-18T07:13:12.727Z
From what little I understand it's about providing patter matching either as syntactic sugar or as core feature that is explicitly represented in AST?
Viola
CC BY-SA 4.0
2023-05-18T15:21:55.600Z
@Viola in fact pattern matching can have its own semantics which differs from being a compositional version of 'one variable matching'.
ice1000
<blockquote>
<p>Eliminators</p>
</blockquote>
<p>Here are some pros:</p>
<ol>
<li>Readability. They explicitly separate cases for each  constructor of a inductive type.</li>
<li>More features. They allow you to have dependent types or more complex functions.</li>
</ol>
<p>Here are some cons:</p>
<ol>
<li>Complexity. Adding it makes the language more complex and make it harder to learn.</li>
<li>Performance. They can produce a significant amount of indirection which can affect your performance. Pattern matching does much less of this.</li>
</ol>
<blockquote>
<p>Pattern matching</p>
</blockquote>
<p>Here are some pros:</p>
<ol>
<li>Simplicity. Unlike eliminators, they are straightforward and intuitive.</li>
<li>Readability. Multiple cases can be taken care of in one construct, making the code more readable. Eliminators tend to make the syntax considerably more verbose.</li>
</ol>
<p>Here are some cons:</p>
<ol>
<li>Runtime errors. Pattern matching often leads to a lot of runtime errors that need to fixed. It also requires the creator to be extremely thorough and put in a significant amount of effort into the language. This is much less in eliminators.</li>
<li>Not useful for all code. For some higher level code, the limited functionality compared to language with eliminators can mean that very advanced or specialized things simply can't be done.</li>
</ol>

CC BY-SA 4.0
2023-05-19T10:12:38.620Z
2023-05-19T10:14:38.310Z
2023-05-19T10:14:38.310Z
Starship
CC BY-SA 4.0
2023-05-19T21:09:25.653Z
The pros of *both* of them include "readability?" Also, what is the difference between simplicity and readability here? And can you provide a reference for the performance difference between the two? I am skeptical of that one. It also seems like you're implying that pattern matching cannot work for dependent types, which is not true (for instance, see [Coq's `match ... as ... in ... return ... with ... end` construct](https://coq.inria.fr/refman/language/extensions/match.html#dependent-pattern-matching)).
David Young
# What are the pros and cons of eliminators vs. pattern matching with a termination checker?
Posted by: username_0 on 2023-05-16
In type theoretic presentations of programming languages, we usually define an elimination principle similar to a function for inductive types, and we assume pattern matchings to be *elaborated* into the eliminators. In practical implementations like in Agda/Haskell, we have pattern matching in the core language. Some languages impose eliminators, and really do the translation under the hood, such as Coq/Lean.

What are the benefits of each of these methods?
**Tags:** types
> **Comments:**
> **username_1**: From what little I understand it's about providing patter matching either as syntactic sugar or as core feature that is explicitly represented in AST?  
> **username_0**: @Viola in fact pattern matching can have its own semantics which differs from being a compositional version of 'one variable matching'.  
---
## 1 answers
### Answer by username_2 on 2023-05-19. Score: 3
> Eliminators

Here are some pros:

1. Readability. They explicitly separate cases for each constructor of a inductive type.
2. More features. They allow you to have dependent types or more complex functions.

Here are some cons:

1. Complexity. Adding it makes the language more complex and make it harder to learn.
2. Performance. They can produce a significant amount of indirection which can affect your performance. Pattern matching does much less of this.

> Pattern matching

Here are some pros:

1. Simplicity. Unlike eliminators, they are straightforward and intuitive.
2. Readability. Multiple cases can be taken care of in one construct, making the code more readable. Eliminators tend to make the syntax considerably more verbose.

Here are some cons:

1. Runtime errors. Pattern matching often leads to a lot of runtime errors that need to fixed. It also requires the creator to be extremely thorough and put in a significant amount of effort into the language. This is much less in eliminators.
2. Not useful for all code. For some higher level code, the limited functionality compared to language with eliminators can mean that very advanced or specialized things simply can't be done.
> **Comments:**
> **username_3** (2023-05-19): The pros of *both* of them include "readability?" Also, what is the difference between simplicity and readability here? And can you provide a reference for the performance difference between the two? I am skeptical of that one. It also seems like you're implying that pattern matching cannot work for dependent types, which is not true (for instance, see [Coq's `match ... as ... in ... return ... with ... end` construct](https://coq.inria.fr/refman/language/extensions/match.html#dependent-pattern-matching)).  
---
