How do clausal definitions work?

Question

I'm most familiar with the metatheory of calculi based around expressions.

But systems like Agda use separate clauses for definitions.

ifte : { A : Set } -> bool -> A -> A -> A
ifte true x y = x
ifte false x y = y

Copatterns are a similar construct.

I'm mostly interested because I was interested in whether this sort of thing could simplify use of positive types.

For the STLC this sort of scheme suggests an almost ANFish sort of approach?

$$ \frac{x \colon \tau \in \Gamma}{\Gamma \vdash x \colon \tau}$$

$$\frac{ \begin{split}\Gamma, x\colon \tau_1 \vdash e_1 \colon \tau_2\\ \Gamma, y\colon \tau_1 \to \tau_2 \vdash e_2\colon \tau_3 \end{split}}{\Gamma \vdash \textbf{let} \, y \, x := e_1 \, \textbf{in} \, e_2 \colon \tau_3}$$

$$\frac{ \begin{split}\Gamma \vdash e_1 \colon \tau_1 \to \tau_2\\ \Gamma \vdash e_2 \colon \tau_1 \end{split}}{\Gamma \vdash e_1 e_2 \colon \tau_2}$$

I think for sum types you might have pattern matching like

$$\frac{ \begin{split} \Gamma, x\colon \tau_1 \vdash e_1 \colon \tau_3\\ \Gamma , x\colon \tau_2 \vdash e_2 \colon \tau_3\\ \Gamma , y\colon \tau_1 + \tau_2 \to \tau_3 \vdash e_3 \colon \tau_4 \end{split}}{\Gamma \vdash \textbf{let} \, \begin{split}y \, x := e_1 \\ y \, x := e_2 \end{split} \, \textbf{in} \, e_3 \colon \tau_3}$$

I'm not really sure I'm getting the spirit of clausal definitions or how they might simplify things.

How precisely would you formalize these sort of clausal definitions?

Answer 1

If you are interested in non-dependent languages then it is probably not a proof-assistants related question. Those are quite well-studied in computer science. So I assume you are asking about using clausal definitions in dependently typed languages, as opposed to using eliminators (the expression-based substitute for pattern matching and recursion etc).

You can read about these in a series of papers.

• It began with Eliminating dependent pattern matching. This translates clausal pattern matching into eliminators.
• Then it is improved to without using axiom K.
• Then copatterns are added here. And this paper also addresses other problems involving clausal definitions. Its emphasis is less on translating them to eliminators, as languages like Agda don't do the translation anyway.
• Another topic of relevance is termination checking, to which foetus is a good introduction. I'm not familiar with coinductive progress checking.

As for how it simplifies stuff, see if you can define head : Vec (suc n) A -> A that fetches the first element of a nonempty vector using eliminators only. (Hint: it's very long.) More in-depth discussion of this can be found at

• The view from the Left which discusses techniques available with clausal definitions.