# Equality Saturation in Haskell, a tutorial

DevFeed: [Equality Saturation in Haskell, a tutorial](<https://devfeed.tech/articles/equality-saturation-in-haskell-a-tutorial-27909.md>)

Original publisher: [Read original article](<http://alt-romes.github.io/posts/2022-08-23-a-first-hegg-tutorial.html>)

Published: 2022-08-23T00:00:00Z

Content type: tutorial

Language: en

Sources: [Romes' Musings](<https://devfeed.tech/sources/romes-musings.md>)

Topics: [Haskell](<https://devfeed.tech/topics/haskell.md>), [Tutorial](<https://devfeed.tech/topics/tutorial.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>)

Tags: [haskell](<https://devfeed.tech/tags/haskell.md>), [mathematics](<https://devfeed.tech/tags/mathematics.md>), [tutorial](<https://devfeed.tech/tags/tutorial.md>), [types](<https://devfeed.tech/tags/types.md>)

## AI overview

A Haskell tutorial introduces equality saturation and e-graphs through hegg, a Haskell-native library based on egg. It develops a simple symbolic mathematics library that simplifies numeric expressions using rewrite rules, covering syntax, language definitions, e-class analysis, cost functions, rewrite rules, and equality saturation.

## Source excerpt

Contents 1 Symbolic Maths in E-graphs 1.1 Syntax 1.2 Language 1.3 Analysis 2 Equality saturation on symbolic expressions 2.1 Cost function 2.2 Rewrite rules 2.3 Equality saturation, finally hegg is a Haskell-native library providing fast e-graphs and equality saturation, based on egg: Fast and Extensible Equality Saturation and Relational E-matching. Suggested material on equality saturation and e-graphs for beginners egg: Fast and Extensible Equality Saturation in a 5m video egg's users guide To get a feel for how we can use hegg and do equality saturation in Haskell, we'll write a simple numeric symbolic manipulation library that can simplify expressions according to a set of rewrite rules by leveraging equality saturation. I hope to eventually write a better exposition that assumes less prior knowledge which introduces first e-graphs-only workflows, and only then equality saturation, from a hegg user's perspective. Until then, this rough tutorial serves as an alternative. 1 Symbolic Maths in E-graphs If you've never heard of symbolic mathematics you might get some intuition from reading Let's Program a Calculus Student first. First, we define our symbolic maths language and enable it to be represented by an e-graph using hegg. 1.1 Syntax We'll start by defining the abstract syntax tree for our simple symbolic expressions: data SymExpr = Const Double | Symbol String | SymExpr :+: SymExpr | SymExpr :*: SymExpr | SymExpr :/: SymExpr infix 6 :+: infix 7 :*:, :/: e1 :: SymExpr e1 = (Symbol "x" :*: Const 2) :/: (Const 2) -- (x*2)/2 You might notice that (x*2)/2 is the same as just x. Our goal is to get equality saturation to do that for us. Our second step is to instance Language for our SymExpr 1.2 Language Language is the required constraint on expressions that are to be represented in e-graph and on which equality saturation can be run: type Language l = (Traversable l, ∀ a. Ord a => Ord (l a)) To declare a Language we must write the "base functor" of SymExpr (i.e.