17
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Viola
    May 18, 2023 at 7:13
  • $\begingroup$ @Viola in fact pattern matching can have its own semantics which differs from being a compositional version of 'one variable matching'. $\endgroup$
    – ice1000
    May 18, 2023 at 15:21

1 Answer 1

3
$\begingroup$

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.
$\endgroup$
1
  • 1
    $\begingroup$ 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). $\endgroup$ May 19, 2023 at 21:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .