Unification and pattern matching

Learning
,
1

I’m trying to understand how pattern matching works “under the hood”, and while i was reading the wikipedia page of “unification” i saw this :

If a solution is required to make both sides of each equation literally equal, the process is called syntactic or free unification, otherwise semantic or equational unification, or E-unification, or unification modulo theory.

If the right side of each equation is closed (no free variables), the problem is called (pattern) matching. The left side (with variables) of each equation is called the pattern.[1]

And i’m not sure to understand the link between unification and pattern matching actually, when it talk about “the right side of each equation”, the equation is : pattern = value as match value with pattern ->... in ocaml ?

2

As far as compilation is concerned, pattern matching and unification are not related. The compilation of pattern matching works by decomposing complex pattern matchings (with nested patterns) into a nested pattern matchings where each node performs only “simple” pattern matchings (ie matches on the head constructor).

For a clear explanation of how this is done in a simplified version of the OCaml compiler, I recommend taking a look at section 5.2.4 of

(the actual thing is more complex, but the basic idea is the same).

Cheers,
Nicolas

1 Like
3

This paper is also good to understand the pattern-matching compilation.

2 Likes