Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined by the shallow pattern matching

rec x f 0 = x
rec x f (S n) = f n (rec x f n)

A non-shallow pattern would be something like

even 0 = true
even (S 0) = false
even (S S n) = even n

because it stacks the constructor in the third clause.

One gets the idea that we can translate patterns back to eliminators. (Exercise: write down even using rec.) However, the question how precisely this can be done is not trivial, especially in type theories without Axiom K. As it turns out, for Agda the answer is positive, see Pattern matching without K by Cockx, Devriese and Piessens.

Eliminators are more convenient from a semantic point of view, as they correspond more closely to how universal properties of constructions are described in practice. For example, the simple recursor for natural numbers is the direct translation of the fact that $\mathbb{N}$ is the initial algebra for $X \mapsto 1 + X$.

As Neel points out in the comments, patterns are generally preferred in proof-theoretic analysis, because the normal forms need many fewer commuting conversions.

For the best of both worlds, we would like to describe new constructions in terms of eliminators, as they are easier to specify, but then to use them with pattern matching. (And this answers your question: eliminators are useful in practice because it is easy for a user to explain what an elimnator is, but it's a lot harder for the user to extend pattern matching.)

It would be nice to have a proof assistant that could automate the passage from an eliminator to (non-shallow) patterns. I believe Epigram 2 was going in that direction?

Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined by the shallow pattern matching

rec x f 0 = x
rec x f (S n) = f n (rec x f n)

A non-shallow pattern would be something like

even 0 = true
even (S 0) = false
even (S S n) = even n

because it stacks the constructor in the third clause.

One gets the idea that we can translate patterns back to eliminators. (Exercise: write down even using rec.) However, the question how precisely this can be done is not trivial, especially in type theories without Axiom K. As it turns out, for Agda the answer is positive, see Pattern matching without K by Cockx, Devriese and Piessens.

Eliminators are more convenient from a semantic point of view, as they correspond more closely to universal properties of semantic constructions. For example, the simple recursor for natural numbers is the direct translation of the fact that $\mathbb{N}$ is the initial algebra for $X \mapsto 1 + X$.

As Neel points out in the comments, patterns are generally preferred in proof-theoretic analysis, because the normal forms need many fewer commuting conversions.

For the best of both worlds, we would like to describe new constructions in terms of eliminators, as they are easier to specify, but then to use them with pattern matching. (And this answers your question: eliminators are useful in practice because it is easy for a user to explain what an elimnator is, but it's a lot harder for the user to extend pattern matching.)

It would be nice to have a proof assistant that could automate the passage from an eliminator to (non-shallow) patterns. I believe Epigram 2 was going in that direction?

Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined by the shallow pattern matching

rec x f 0 = x
rec x f (S n) = f n (rec x f n)

A non-shallow pattern would be something like

even 0 = true
even (S 0) = false
even (S S n) = even n

because it stacks the constructor in the third clause.

One gets the idea that we can translate patterns back to eliminators. (Exercise: write down even using rec.) However, the question how precisely this can be done is not trivial, especially in type theories without Axiom K. As it turns out, for Agda the answer is positive, see Pattern matching without K by Cockx, Devriese and Piessens.

Eliminators are more convenient from a theoretical point of view, as it is more straightforward to describe their semantic meaning. They correspond more closely to how universal properties of constructions are described in practice. For example, the simple recursor for natural numbers is the direct translation of the fact that $\mathbb{N}$ is the initial algebra for $X \mapsto 1 + X$.

For the best of both worlds, we would like to describe new constructions in terms of eliminators, as they are easier to specify, but then to use them with pattern matching. (And this answers your question: eliminators are useful in practice because it is easy for a user to explain what an elimnator is, but it's a lot harder for the user to extend pattern matching.)

It would be nice to have a proof assistant that could automate the passage from an eliminator to (non-shallow) patterns. I believe Epigram 2 was going in that direction?

Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined by the shallow pattern matching

rec x f 0 = x
rec x f (S n) = f n (rec x f n)

A non-shallow pattern would be something like

even 0 = true
even (S 0) = false
even (S S n) = even n

because it stacks the constructor in the third clause.

One gets the idea that we can translate patterns back to eliminators. (Exercise: write down even using rec.) However, the question how precisely this can be done is not trivial, especially in type theories without Axiom K. As it turns out, for Agda the answer is positive, see Pattern matching without K by Cockx, Devriese and Piessens.

Eliminators are more convenient from a semantic point of view, as they correspond more closely to how universal properties of constructions are described in practice. For example, the simple recursor for natural numbers is the direct translation of the fact that $\mathbb{N}$ is the initial algebra for $X \mapsto 1 + X$.

As Neel points out in the comments, patterns are generally preferred in proof-theoretic analysis, because the normal forms need many fewer commuting conversions.

For the best of both worlds, we would like to describe new constructions in terms of eliminators, as they are easier to specify, but then to use them with pattern matching. (And this answers your question: eliminators are useful in practice because it is easy for a user to explain what an elimnator is, but it's a lot harder for the user to extend pattern matching.)

It would be nice to have a proof assistant that could automate the passage from an eliminator to (non-shallow) patterns. I believe Epigram 2 was going in that direction?