Vrftsjtryk

Nomenclature

The term expressive in the question shall bear the same meaning as in the following sentence:

A Turing Machine is as expressive as Lambda Calculus.

Introduction

While learning Haskell, I had noticed that there are 2 ways to achieve the same effect, namely Pattern Matching and Case Expression. For example,

-- Pattern Matching

not True  = False

not False = True



-- Case Expression

not x = case x of True  -> False

                  False -> True

I am also fully aware that Pattern Matching is actually a form of syntax sugar that will be compiled into Case Expression.

Therefore, we can be very sure that every Pattern Matching expression can be converted to Case Expression.

Question

So, this is my question: Is the following statement true?

Every Case Expression can be re-written using Pattern Matching.

Regardless of the truthiness of the statement above, I would be glad if you could provide a formal proof to support your answer.

P/S

The motivation that drove me to seek answer for this question is because I'm currently designing my own language, which I wish to have as less feature as possible, but not too minimal like Lambda Calculus which only have 3 features.

The expression

case e of

  p1 -> e1

  p2 -> e2

  ...

can be rewritten as

let k p1 = e1

    k p2 = e2

    ...

 in k e

where k is a fresh identifier.

This translation assumes that the language has some way to define a local function by pattern matching (e.g. let).

If local functions can not be defined, there's always the possibility of lifting the definition to the top level. Indeed, any local definition

let f x1 ... xk = e in e'

having free variables v1 .. vn can be rewritten written as

(f -> e') (globalF v1 ... vn)

provided that we also define a global function

globalF v1 ... vn x1 ... xk = e

Note that globalF has no free variables, by construction. I believe it is sometimes called a "supercombinator".

This naturally extends to the case where x1 ... xk are patterns, and we have multiple defining equations for f / globalF.

For example,

case x of True  -> False

          False -> True

cab be rewritten as

let f True  = False

    f False = True

 in f x