# Unification and pattern matching

**URL:** <https://discuss.ocaml.org/t/unification-and-pattern-matching/14196>\
**Category:** Learning\
**Tags:** type-system, compilation\
**Created:** [February 27, 2024, 11:24am UTC](https://discuss.ocaml.org/t/unification-and-pattern-matching/14196 "2024-02-27T11:24:57Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![Gholad](https://avatars.discourse-cdn.com/v4/letter/g/839c29/32.png) [@Gholad](https://discuss.ocaml.org/u/Gholad)\
**Post date:** [February 27, 2024, 11:24am UTC](https://discuss.ocaml.org/t/unification-and-pattern-matching/14196/1 "2024-02-27T11:24:57Z")

</div>

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]](https://en.wikipedia.org/wiki/Unification_(computer_science)#cite_note-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 ?

---

<div class="post-metadata">

**Author:** ![nojb](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/nojb/32/519_2.png) [@nojb](https://discuss.ocaml.org/u/nojb)\
**Post date:** [February 27, 2024, 12:17pm UTC](https://discuss.ocaml.org/t/unification-and-pattern-matching/14196/2 "2024-02-27T12:17:29Z")

</div>

> [@Gholad](#):
>
> And i’m not sure to understand the link between unification and pattern matching

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

> **[xleroy-zinc.pdf](https://caml.inria.fr/pub/papers/xleroy-zinc.pdf)**
>
> 901.93 KB

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

Cheers,  
Nicolas

---

<div class="post-metadata">

**Author:** ![dinosaure](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/dinosaure/32/16_2.png) [@dinosaure](https://discuss.ocaml.org/u/dinosaure)\
**Post date:** [February 27, 2024, 12:32pm UTC](https://discuss.ocaml.org/t/unification-and-pattern-matching/14196/3 "2024-02-27T12:32:59Z")

</div>

This [paper](http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf) is also good to understand the pattern-matching compilation.