Triemaps that match

Technical Report

Simon Peyton Jones

Epic Games

Sebastian Graf

Karlsruhe Institute of Technology

The trie data structure is a good choice for finite maps whose
keys are data structures (trees) rather than atomic values. But what if we want
the keys to be patterns, each of which matches many lookup keys?
Efficient matching of this kind is well studied in the theorem prover
community, but much less so in the context of statically typed functional programming.
Doing so yields an interesting new viewpoint — and a practically useful design
pattern, with good runtime performance.

§ INTRODUCTION

Many functional languages provide finite maps either as a
built-in data type, or as a mature, well-optimised library.  Generally the keys
of such a map will be small: an integer, a string, or perhaps a pair of integers.
But in some applications the key is large: an entire tree structure.  For example,
consider the Haskell expression
[3]let x=a+b in...(let y=a+b in x+y)....[E]
We might hope that the compiler will recognise the repeated sub-expression
and transform to
[3]let x=a+b in...(x+x)....[E]
An easy way to do so is to build a finite map that maps the expression  to .
Then, when encountering the inner , we can look up the right hand side in the map,
and replace  by .  All we need is a finite map keyed by syntax trees.

Traditional finite-map implementations tend to do badly in such applications, because
they are often based on balanced trees, and make the assumption that comparing two keys is
a fast, constant-time operation.  That assumption is false for large, tree-structured keys.

Another time that a compiler may want to look up a tree-structured key is
when rewriting expressions: it wants to see if any rewrite rule matches the
sub-expression in hand, and if so rewrite with the instantiated right-hand
side of the rule.
To do this we need a fast way to see if a target expression matches one of
the patterns in a set of (pattern, rhs) pairs.
If there is a large number of such
(pattern, rhs) entries to check, we would like to do so faster
than checking them one by one. Several parts of GHC, a Haskell compiler, need
matching lookup, and currently use an inefficient linear algorithm to do so.

In principle it is well known how to build a finite map for a deeply-structured
key: use a trie.  The matching task is also well studied but, surprisingly,
only in the automated reasoning community (<Ref>): they use
so-called discrimination trees.
In this paper we apply these
ideas in the context of a statically-typed functional programming language, Haskell.
This shift of context is surprisingly fruitful, and we make the following contributions:

* Following <cit.>, we develop a standard pattern for
a statically-typed triemap for an arbitrary algebraic data type (<Ref>). In
contrast, most of the literature describes untyped tries for a
fixed, generic tree type.
In particular:

* Supported by type classes, we can make good use of polymorphism to build triemaps
for polymorphic data types, such as lists (<Ref>).

* We cover the full range of operations expected for finite maps:
not only ion and , but , , ,  and

* We develop a generic optimisation for singleton maps that
compresses leaf paths. Intriguingly, the resulting triemap
transformer can be easily mixed into arbitrary triemap definitions

* We show how to make our triemaps insensitive to $\alpha$-renamings in
keys that include binding forms (<Ref>).
Accounting for $\alpha$-equivalence is not hard, but it is crucial for
the applications in compilers.

* We extend our triemaps to support matching lookups
(<Ref>).  This is an important step, because the only
readily-available alternative is linear lookup. Our main
contribution is to extend the established idea of tries keyed by
arbitrary data types, so that it can handle matching too.

* We present measurements that compare the performance of our triemaps (ignoring
their matching capability) with traditional finite-map implementations in
Haskell (<Ref>).

We discuss related work in <Ref>.
Our contribution is not so much a clever new idea as an exposition of
some old ideas in a new context.  Nevertheless, we found it
surprisingly tricky to develop the “right” abstractions, such as
the  and  classes, the singleton-and-empty map
data type, and the combinators we use in our instances.
These abstractions have been through many iterations, and we
hope that by laying them out here, as a functional pearl, we may shorten
the path for others.

§ THE PROBLEM WE ADDRESS

[B]type TF v=Maybe v→Maybe v[E]

[B]data Map k v=…[23]

[26]::Map k v[E]

[26]::Ord k[36]
[36]⇒k→v→Map k v→Map k v[E]

[26]::Ord k[36]
[36]⇒k→Map k v→Maybe v[E]

[30]Ord k[37]
[37]⇒TF v→k[E]

[30]→Map k v→Map k v[E]

[26]::(v→r→r)→r→Map k v→r[E]

[26]::(v→w)→Map k v→Map k w[E]

[30]Ord k[37]

[30]→Map k v→Map k v→Map k v[E]

[26]::Map k v→Int[E]

[30]Ord b[37]
[37]⇒Map b c→Map a b→Map a c[E]

[B]infixr 1>=>[23]

[B](>=>)::Monad m[19]
[19]⇒(a→m b)→(b→m c)[E]

[19]→a→m c[E]

[B]infixr 1>>>[23]

[B]infixr 0▹[23]

API for library functions

Our general task is as follows: implement an efficient finite mapping
from keys to values, in which the key is a tree.
Semantically, such a finite map is just a set of (key,value)
pairs; we query the map by looking up a target.
For example, the key might be a data type of syntax trees, defined like this:
[B]type Var=String[E]

[B]data Expr=App Expr Expr|Lam [34]
[34]Var Expr|Var Var[E]
Here  is the type of variables; these can be compared for
equality and used as the key of a finite map.  Its definition is not important
for this paper, but for the sake of concreteness,
you may wish to imagine it is simply a string:

The data type  is capable of representing expressions like $(add\,x\,y)$ and
$(\lambda{}x.\,add\,x\,y)$. We will use this data type throughout the paper, because it
has all the features that occur in real expression data types: free variables like $add$,
represented by a  node;
lambdas which can bind variables (), and occurrences of those bound variables ();
and nodes with multiple children ().  A real-world expression type would have
many more constructors, including literals, let-expressions and suchlike.

§.§ Alpha-renaming

In the context of a compiler, where the keys are expressions or types,
the keys may contain internal binders, such as the binder  in
$(\lambda{}x.x)$. If so, we would expect insertion and lookup to be insensitive
to $\alpha$-renaming, so we could, for example, insert with key $(\lambda{}x.x)$
and look up with key $(\lambda{}y.y)$, to find the inserted value.

§.§ Lookup modulo matching

Beyond just the basic finite maps we have described, our practical setting
in GHC demands more: we want to do a lookup that does matching.  GHC supports
so-called rewrite rules <cit.>, which the user can specify
in their source program, like this:
[B]{-# RULES 34 map/map34 [29]
[29]$\forall$  f g xs∘. [45]
[45]map f (map g xs)[E]

[48]map (f∘. g) xs #-}[E]
This rule asks the compiler to rewrite any target expression that matches the shape
of the left-hand side (LHS) of the rule into the right-hand side
(RHS).  We use the term pattern to describe the LHS, and target to describe
the expression we are looking up in the map.
The pattern is explicitly quantified over the pattern variables
(here , , and ) that
can be bound during the matching process.  In other words, we seek a substitution
for the pattern variables that makes the pattern equal to the target expression.
For example, if the program we are compiling contains the expression
, we would like to produce a substitution
so that the substituted RHS
becomes ; we would replace the former expression
with the latter in the code under consideration.

Of course, the pattern might itself have bound variables, and we would
like to be insensitive to $\alpha$-conversion for those. For example:
[B]{-# RULES 34 map/id34 [28]
[28]map (λx→x)=λy→y #-}[E]
We want to find a successful match if we see a call ,
even though the bound variable has a different name.

Now imagine that we have thousands of such rules.  Given a target
expression, we want to consult the rule database to see if any
rule matches.  One approach would be to look at the rules one at a
time, checking for a match, but that would be slow if there are many rules.
Similarly, GHC's lookup for
type-class instances and for type-family instances can have thousands
of candidates. We would like to find a matching candidate more efficiently
than by linear search.

§.§ Non-solutions

At first sight, our task can be done easily: define a total order on
and use a standard finite map library.
Indeed that works, but it is terribly slow.  A finite map is
implemented as a binary search tree; at every node of this tree,
we compare the key (an , remember) with
the key stored at the node; if it is smaller, go left; if larger, go right. Each lookup
thus must perform a (logarithmic) number of
potentially-full-depth comparisons of two expressions.

Another possibility might be to hash the  and use the
hash-code as the lookup key.  That would make lookup much faster, but
it requires at least two full traversals of the key for every lookup:
one to compute its hash code for every lookup, and a full equality
comparison on a “hit” because hash-codes can collide.

But the killer is this: neither binary search trees nor hashing is compatible
with matching lookup.  For our purposes they are non-starters.

What other standard solutions to matching lookup are there, apart from linear search?
The theorem proving and automated reasoning community has been working with huge sets
of rewrite rules, just as we describe, for many years.
They have developed term indexing techniques for the job <cit.>,
which attack the same problem from a rather different angle, as we discuss in <Ref>.

§ TRIES

A standard approach to a finite map in which the key has internal structure
is to use a trie[<https://en.wikipedia.org/wiki/Trie>].
Generalising tries to handle an arbitrary algebraic data type as the key is
a well established, albeit under-used, idea <cit.>.
We review these ideas in this section.
Let us consider a simplified
form of expression:
[B]data Expr=Var Var|App Expr Expr[E]
We omit lambdas for now,
so that all  nodes represent free variables, which are treated as constants.
We will return to lambdas in <Ref>.

§.§ The interface of a finite map

Building on the design of widely
used functions in Haskell (see <ref>), we
seek these basic operations:
[11]::ExprMap v[E]

[11]::Expr→ExprMap v→Maybe v[E]

[11]::Expr→TF v→ExprMap v→ExprMap v[E]
The lookup function [We use short names  and
consistently in this paper to reflect the single-column format.
has a type that is familiar from every finite map.
The update function , typically called  in Haskell libraries,
changes the value stored at a particular key.
The caller provides a value transformation function , an
abbreviation for  (see <Ref>). This function
transforms the existing value associated with the key, if any (hence the input
), to a new value, if any (hence the output ).
We can easily define  and  from :
[B]insertEM::Expr→v→ExprMap v→ExprMap v[E]

[B]insertEM e v=atEM e (92 95 →Just v)[E]

[B]deleteEM::Expr→ExprMap v→ExprMap v[E]

[B]deleteEM e=atEM e (92 95 →Nothing)[E]
You might wonder whether, for the purposes of this paper, we could just define ,
leaving  for the Appendix
[In the supplemental file ],
but as we will see in <Ref>, our approach using tries
requires the generality of .

These fundamental operations on a finite map must obey the following properties:
[B] [52]
[52]lookup e empty[80]
[80] ≡[87]

[B] [52]
[52]lookup e (alter e xt m)[80]
[80] ≡[87]
[87]xt (lookup e m)[E]

[52]lookup e_1 (alter e_2 xt m)[80]
[80] ≡[87]
[87]lookup e_1 m[E]

We also support other standard operations on finite maps,
with types analogous to those in <Ref>, including , , and .

§.§ Tries: the basic idea

Here is a trie-based implementation for :
[B]data ExprMap v[E]

[3]=EM {1.5mu em95 var[18]
[18]::Map Var v,em95 app[40]
[40]::ExprMap (ExprMap v)1.5mu}[E]
Here  is any standard finite map (e.g. in containers)
keyed by , with values .
One way to understand this slightly odd data type is to study its lookup function:
[B]lkEM::Expr→ExprMap v→Maybe v[E]

[B]lkEM e (EM {1.5mu em95 var=var,em95 app=app1.5mu})=case e of[E]

[3]Var x[14]
[14]→Map.lookup x var[E]

[3]App e_1 e_2[14]
[18]case lkEM e_1 app of[E]

[6]Just m_1[15]
[15]→lkEM e_2 m_1[E]
This function pattern-matches on the target .  The  alternative
says that to look up a variable occurrence, just look that variable up in the
But if the expression is an  node, we first look up
in the  field, which returns an .  We then look up
in that map.  Each distinct  yields a different  in which to look up .

We can substantially abbreviate this code, at the expense of making it more cryptic, thus:
[B]lkEM (Var x)[23]
[23]=em95 var[33]
[33]>>>Map.lookup x[E]

[B]lkEM (App e_1 e_2)[23]
[23]=em95 app[33]
[33]>>>lkEM e_1>=>lkEM e_2[E]
The function
is the auto-generated selector that picks the  field from an  record, and similarly .
The functions  and  are right-associative forward composition
operators, respectively monadic and non-monadic,
that chain the individual operations together (see <Ref>).
Finally, we have $\eta$-reduced the definition, by omitting the  parameter.
These abbreviations become quite worthwhile when we add more constructors, each with more fields,
to the key data type.

Notice that in contrast to the approach of <Ref>, we never compare two expressions
for equality or ordering.  We simply walk down the  structure, guided
at each step by the next node in the target.

This definition is extremely short and natural. But it embodies a hidden
complexity: it requires polymorphic recursion. The recursive call to
instantiates  to a different type than the parent function definition.
Haskell supports polymorphic recursion readily, provided you give type signature to
, but not all languages do.

§.§ Modifying tries

It is not enough to look up in a trie – we need to build them too.
First, we need an empty trie. Here is one way to define it:
[B]emptyEM::ExprMap v[E]

[B]emptyEM=EM {1.5mu em95 var=Map.empty,em95 app=emptyEM1.5mu}[E]
It is interesting to note that  is an infinite, recursive structure:
the  field refers back to .  We will change this
definition in <Ref>, but it works perfectly well for now.
Next, we need to  a triemap:
[B]atEM::Expr→TF v→ExprMap v→ExprMap v[E]

[B]atEM e tf m@(EM {1.5mu em95 var=var,em95 app=app1.5mu})=case e of[E]

[3]Var x[14]
[14]→m {1.5mu em95 var[29]
[29]=Map.alter tf x var1.5mu}[E]

[3]App e_1 e_2[14]
[14]→m {1.5mu em95 app[29]
[29]=atEM e_1 (liftTF (atEM e_2 tf)) app1.5mu}[E]

[B]liftTF::(ExprMap v→ExprMap v)→TF (ExprMap v)[E]

[B]liftTF f Nothing[21]
[21]=Just (f emptyEM)[E]

[B]liftTF f (Just m)[21]
[21]=Just (f m)[E]
In the  case, we must just update the map stored in the  field,
using the  function from <Ref>.

In the  case we look up  in ;
we should find a  there, which we want to alter with .
We can do that with a recursive call to , using
for impedance-matching.

The  case shows why we need the generality of .
Suppose we attempted to define an apparently-simpler  operation.
Its equation for  would look up  — and would then
need to alter that entry (an , remember) with the result of
inserting .  So we are forced to define  anyway.

We can abbreviate the code for  using combinators, as we did in the case of
lookup, and doing so pays dividends when the key is a data type with
many constructors, each with many fields.  However, the details are
fiddly and not illuminating, so we omit them here.  Indeed, for the
same reason, in the rest of this paper we will typically omit the code
for , though the full code is available in the Appendix.

§.§ Unions of maps

A common operation on finite maps is to take their union:
[B]unionEM::ExprMap v→ExprMap v→ExprMap v[E]
In tree-based implementations of finite maps, such union operations can be tricky.
The two trees, which have been built independently, might not have the same
left-subtree/right-subtree structure, so some careful rebalancing may be required.
But for tries there are no such worries –
their structure is identical, and we can simply zip them together.  There is one
wrinkle: just as we had to generalise  to ,
to accommodate the nested map in , so we need to generalise  to :

[18]ExprMap v→ExprMap v→ExprMap v[E]
When a key appears on both maps, the combining function is used to
combine the two corresponding values.
With that generalisation, the code is as follows:
[B]unionWithEM f [16]
[16](EM {1.5mu em95 var=var_1,em95 app=app_11.5mu}) [E]

[16](EM {1.5mu em95 var=var_2,em95 app=app_21.5mu})[E]

[3]=EM [9]
[9]{1.5mu em95 var=Map.unionWith f var_1 var_2[E]

[9],em95 app=unionWithEM (unionWithEM f) app_1 app_21.5mu}[E]
It could hardly be simpler.

§.§ Folds and the empty map

The strange, infinite definition of  given in <Ref>
works fine (in a lazy language at least) for lookup, alteration, and union, but it fails
fundamentally when we want to iterate over the elements of the trie.
For example, suppose we wanted to count the number of elements in the finite map; in
this is the function  (<Ref>).  We might attempt:
[B]sizeEM::ExprMap v→Int[E]

[B]sizeEM (EM {1.5mu em95 var=var,em95 app=app1.5mu})[E]

[3]=Map.size var+???[E]
We seem stuck because the size of the  map is not what we want: rather,
we want to add up the sizes of its elements, and we don't have a way to do that yet.
The right thing to do is to generalise to a fold:
[B]foldrEM::$\forall$  v∘. (v→r→r)→r→ExprMap v→r[E]

[B]foldrEM k z (EM {1.5mu em95 var=var,em95 app=app1.5mu})[E]

[3]=Map.foldr k z_1 var[E]

[5]z_1=foldrEM kapp z (app::ExprMap (ExprMap v))[E]

[5]kapp m_1 r=foldrEM k r m_1[E]
In the binding for  we fold over , using
to combine the map we find with the accumulator, by again
folding over the map with .

But alas,  will never terminate!  It always invokes itself immediately
(in ) on ; but that invocation will again recursively invoke
; and so on forever.
The solution is simple: we just need an explicit representation of the empty map.
Here is one way to do it (we will see another in <Ref>):
[B]data ExprMap v[17]
[17]=EmptyEM|EM {1.5mu em95 var::...,em95 app::...1.5mu}[E]

[B]emptyEM::ExprMap v[E]

[B]foldrEM::(v→r→r)→r→ExprMap v→r[E]

[B]foldrEM k z EmptyEM=z[E]

[B]foldrEM k z (EM {1.5mu em95 var=var,em95 app=app1.5mu})[E]

[3]=Map.foldr k z_1 var[E]

[5]z_1=foldrEM kapp z app[E]

[5]kapp m_1 r=foldrEM k r m_1[E]
Equipped with a fold, we can easily define the size function, and another
that returns the range of the map:
[B]sizeEM::ExprMap v→Int[E]

[B]sizeEM=foldrEM (λ n→n+1) 0[E]

[B]elemsEM::ExprMap v→[1.5mu v1.5mu][E]

[B]elemsEM=foldrEM (:) [1.5mu 1.5mu][E]

§.§ A type class for triemaps

Since all our triemaps share a common interface, it is useful to define
a type class for them:
[B]class Eq (Key tm)⇒TrieMap tm where[E]

[4]type Key tm::Type[E]

[17]::tm a[E]

[17]::Key tm→tm a→Maybe a[E]

[17]::Key tm→TF a→tm a→tm a[E]

[17]::(a→b→b)→tm a→b→b[E]

[17]::(a→a→a)→tm a→tm a→tm a[E]

The class constraint  says that the type  is a triemap, with operations
,  etc.
The class has an associated type <cit.>, ,
a type-level function that transforms the type of the triemap into
the type of keys of that triemap.

Now we can witness the fact that  is a , like this:
[B]instance TrieMap ExprMap where[E]

[3]type Key ExprMap=Expr[E]

Having a class allow us to write helper functions that work for any triemap,
such as
[B]insertTM::TrieMap tm⇒Key tm→v→tm v→tm v[E]

[B]insertTM k v=atTM k (92 95 →Just v)[E]

[B]deleteTM::TrieMap tm⇒Key tm→tm v→tm v[E]

[B]deleteTM k=atTM k (92 95 →Nothing)[E]
But that is not all.
Suppose our expressions had multi-argument apply nodes, , thus
[B]data Expr=…|AppV Expr [1.5mu Expr1.5mu][E]
Then we would need to build a trie keyed by a list of .
A list is just another algebraic data type, built with nil and cons,
so we could use exactly the same approach, thus
[B]lkLEM::[1.5mu Expr1.5mu]→ListExprMap v→Maybe v[E]
But rather than to define a  for keys of type ,
and a  for keys of type , etc, we would obviously prefer
to build a trie for lists of any type, like this <cit.>:
[B]instance TrieMap tm⇒TrieMap (ListMap tm) where[E]

[4]type Key (ListMap tm)=[1.5mu Key tm1.5mu][E]

[B]data ListMap tm v=LM [25]
[25]{1.5mu lm95 nil[35]
[35]::Maybe v[E]

[25],lm95 cons::tm (ListMap tm [54]

[B]emptyLM::TrieMap tm⇒ListMap tm[E]

[B]emptyLM=LM {1.5mu lm95 nil=Nothing,lm95 cons=emptyTM1.5mu}[E]

[B]lkLM::TrieMap tm⇒[1.5mu Key tm1.5mu]→ListMap tm v→Maybe v[E]

[B]lkLM [1.5mu 1.5mu][18]
[18]=lm95 nil[E]

[B]lkLM (k:ks)[18]
[18]=lm95 cons>>>lkTM k>=>lkLM ks[E]
The code for  and  is routine. Notice that all of
these functions are polymorphic in , the triemap for the list elements.

§.§ Singleton maps, and empty maps revisited

Suppose we start with an empty map, and insert a value
with a key (an ) such as
[3]App (App (Var 34 f34) (Var 34 x34)) (Var 34 y34)[E]
Looking at the code
for  in <Ref>, you can see that
because there is an  at the root, we will build an
record with an empty , and an
field that is... another
record.  Again the  field will contain an
empty map, while the  field is a further  record.

In effect, the key is linearised into a chain of  records.
This is great when there are a lot of keys with shared structure, but
once we are in a sub-tree that represents a single key-value pair it is
a rather inefficient way to represent the key.  So a simple idea is this:
when a  represents a single key-value pair, represent it
as directly a key-value pair, like this:
[B]data ExprMap v[17]

[17]|SingleEM Expr v[37]

[17]|EM {1.5mu em95 var::...,em95 app::...1.5mu}[E]
But in the triemap for for each new data type ,
we will have to tiresomely repeat these extra data constructors,  and .
For example we would have to add  and  to the  data type
of <Ref>.
It is better instead to abstract over the enclosed triemap, as follows
[ stands for singleton or empty map.]:
[B]data SEMap tm v[18]

[18]|SingleSEM (Key tm) v[E]

[18]|MultiSEM [30]
[30](tm v)[E]

[B]instance TrieMap tm⇒TrieMap (SEMap tm) where[E]

[3]type Key (SEMap tm)=Key tm[E]

The code for lookup practically writes itself. We abstract over
with some  combinators to enjoy forwards compatibility to
[B]lkSEM::TrieMap tm⇒Key tm→SEMap tm v→Maybe v[E]

[B]lkSEM k m=case m of[E]

[3]SingleSEM pk v[19]
[19]→guard (k==pk)>>pure v[E]

[3]MultiSEM m[19]
[19]→lkTM k m[E]
Where  means  and  means . The  expression
in the  will return  when the key expression  doesn't
equate to the pattern expression .
To test for said equality we require an  instance, hence it is
a superclass of  in the  declaration in <Ref>.

The code for alter is more interesting, because it governs the shift from
to  and thence to :
[11]::TrieMap tm[E]

[11]⇒Key tm→TF v→SEMap tm v→SEMap tm v[E]

[B]atSEM k tf EmptySEM=case tf Nothing of [46]

[46]Just v[55]
[55]→SingleSEM k v[E]

[B]atSEM k_1 tf (SingleSEM k_2 v_2)=if k_1==k_2[E]

[3]then case tf (Just v_2) of[E]

[7]Just v'[16]
[16]→SingleSEM k_2 v'[E]

[3]else case tf Nothing of[E]

[16]→SingleSEM k_2 v_2[E]

[7]Just v_1[16]
[16]→MultiSEM (insertTM k_1 v_1 (insertTM k_2 v_2 emptyTM))[E]

[B]atSEM k tf (MultiSEM tm)=MultiSEM (atTM k tf tm)[E]
Adding a new item to a triemap can turn  into  and
into ; and deleting an item from a  turns it back into .
You might wonder whether we can shrink a  back to a  when it has
only one remaining element?
Yes we can, but it takes quite a bit of code, and it is far from clear
that it is worth doing so.

Finally, we need to re-define  and  using :
[3]type ExprMap[22]
[22]=SEMap ExprMap'[E]

[3]data ExprMap' v[22]
[22]=EM {1.5mu em95 var[37]
[37]::...,em95 app[53]
[53]::ExprMap (ExprMap v)1.5mu}[E]

[3]type ListMap[23]
[23]=SEMap ListMap'[E]

[3]data ListMap' tm v[23]
[23]=LM {1.5mu lm95 nil[38]
[38]::...,lm95 cons::tm (ListMap tm v)1.5mu}[E]
The auxiliary data types  and  have only a single constructor, because
the empty and singleton cases are dealt with by .  We reserve the original,
un-primed, names for the user-visible  and  constructors.

§.§ Generic programming

We have not described a triemap library; rather we have described a design pattern.
More precisely, given a new algebraic data type , we have described a systematic way
of defining a triemap, , keyed by values of type .
Such a triemap is represented by a record:

* Each constructor  of  becomes a field  in .

* Each field of a constructor  becomes a nested triemap in the type of the field .

* If  is polymorphic then  becomes a triemap transformer, like

Actually writing out all this boilerplate code is tiresome, and it can of course be automated.
One way to do so would be to
use generic or polytypic programming, and Hinze describes precisely this <cit.>.
Another approach would be to use Template Haskell.

We do not develop either of these approaches here, because our focus is only the
functionality and expressiveness of the triemaps.  However, everything we do is compatible
with an automated approach to generating boilerplate code.

§ KEYS WITH BINDERS

[B]type DBNum=Int[E]

[B]data DBEnv=DBE {1.5mu dbe95 next::DBNum,dbe95 env::Map Var DBNum1.5mu}[E]

[B]emptyDBE=DBE {1.5mu dbe95 next=1,dbe95 env=Map.empty1.5mu}[E]

[B]extendDBE v (DBE {1.5mu dbe95 next=n,dbe95 env=dbe1.5mu})[E]

[3]=DBE {1.5mu dbe95 next=n+1,dbe95 env=Map.insert v n dbe1.5mu}[E]

[B]lookupDBE::Var→DBEnv→Maybe DBNum[E]

[B]lookupDBE v (DBE {1.5mu dbe95 env=dbe1.5mu})=Map.lookup v dbe[E]
De Bruijn leveling

If our keys are expressions (in a compiler, say) they may contain binders,
and we want insert and lookup to be insensitive to $\alpha$-renaming.
That is the challenge we address next. Here is our data type  from
<Ref>, which brings back binding semantics through the
[B]data Expr=App Expr Expr|Lam Var Expr|Var Var[E]
The key idea is simple: we perform De Bruijn numbering on the fly,
renaming each binder to a natural number, from outside in.
So, when inserting or looking up a key $(\lambda x.\, foo~ (\lambda y.\, x+y))$ we
behave as if the key was $(\lambda.\, foo ~(\lambda. \bv{1} + \bv{2}))$, where
each $\bv{i}$ stands for an occurrence of the variable bound by the $i$'th
lambda, counting from the root of the expression. In effect, then, we behave as
if the data type was like this:
[B]data Expr'=App Expr Expr|Lam Expr|FVar Var|BVar BoundKey[E]
Notice (a) the  node no longer has a binder and (b) there are
two sorts of  nodes, one for free variables and one for bound
variables, carrying a  (see below). We will not actually
build a value of type  and look that up in a trie keyed by ;
rather, we are going to behave as if we did. Here is the code
(which uses <Ref>):
[B]data ModAlpha a=A DBEnv a[E]

[B]type AlphaExpr=ModAlpha Expr[E]

[B]instance Eq AlphaExpr where...[E]

[B]type BoundKey[16]

[B]type ExprMap=SEMap ExprMap'[E]

[B]data ExprMap' v[E]

[3]=EM [9]
[9]{1.5mu [9E]
[12]em95 fvar[21]
[21]::Map Var v[42]

[12]em95 bvar[21]
[21]::Map BoundKey v[42]

[12]em95 app[21]
[21]::ExprMap (ExprMap v)[E]

[12]em95 lam[21]
[21]::ExprMap v1.5mu}[E]

[B]instance TrieMap ExprMap' where[E]

[3]type Key ExprMap'=AlphaExpr[E]

[B]lkEM::AlphaExpr→ExprMap' v→Maybe v[E]

[B]lkEM (A bve e)=case e of[E]

[3]Var v→case lookupDBE v bve of[E]

[14]→em95 fvar[26]
[26]>>>Map.lookup v[E]

[5]Just bv[14]
[14]→em95 bvar[26]
[26]>>>Map.lookup bv[E]

[3]App e_1 e_2[14]
[14]→em95 app[26]
[26]>>>lkTM (A bve e_1)>=>lkTM (A bve e_2)[E]

[3]Lam v e[14]
[14]→em95 lam[26]
[26]>>>lkTM (A (extendDBE v bve) e)[E]

[B]lookupClosedExpr::Expr→ExprMap v→Maybe v[E]

[B]lookupClosedExpr e=lkEM (A emptyDBE e)[E]
We maintain a  (cf. <ref>) that
maps each lambda-bound variable to its De Bruijn level
The De Bruijn index of the occurrence of a variable $v$ counts the number
of lambdas between the occurrence of $v$ and its binding site.  The De Bruijn level
of $v$ counts the number of lambdas between the root of the expression and $v$'s binding site.
It is convenient for us to use levels.]
<cit.>, its .
The expression we look up — the first argument of  — becomes an
, which is a pair of a  and an .
At a
node we extend the . At a  node we
look up the variable in the  to decide whether it is
lambda-bound or free, and behave appropriately
[The implementation from the Appendix uses more efficient s
for mapping .  is a itself trie data structure, so it could
have made a nice Tries all the way down argument. But we found it
distracting to present here, hence regular ordered .].

The construction of <Ref>, to handle empty and singleton maps,
applies without difficulty to this generalised map. To use it
we must define an instance  to satisfy the  super class constraint
on the trie key, so that we can instantiate .
That  instance simply equates two
$\alpha$-equivalent expressions in the standard way.
The code for  and  holds no new surprises either.

And that is really all there is to it: it is remarkably easy to extend the basic
trie idea to be insensitive to $\alpha$-conversion and even mix in trie
transformers such as  at no cost other than writing two instance

§ TRIES THAT MATCH

A key advantage of tries over hash-maps and balanced trees is
that we can support matching (<Ref>).

§.§ What “matching” means

Semantically, a matching trie can be thought of as a set of entries,
each of which is a (pattern, value) pair.
What is a pattern? It is a pair $(vs,p)$ where

* $vs$ is a set of pattern variables, such as $[a,b,c]$.

* $p$ is a pattern expression, such as $f\, a\, (g\, b\, c)$.

A pattern may of course contain free variables (not bound by the pattern), such as $f$ and $g$
in the above example, which are regarded as constants by the algorithm.
A pattern $(vs, p)$ matches a target expression $e$ iff there is a unique substitution
$S$ whose domain is $vs$, such that $S(p) = e$.

We allow the same variable to occur more than once in the pattern.
For example, the pattern $([x], f~ x~ x)$
should match targets like $(f~ 1~ 1)$ or $(f ~(g~ v)~ (g ~v))$,
but not $(f~ 1~ (g~ v))$.  This ability is important if we are to use matching tries
to implement class or type-family look in GHC.

In implementation terms, we can characterise matching by the following type
[B]class (Eq (Pat k),MonadPlus (Match k))⇒Matchable k where[E]

[3]type Pat [15]

[3]type Match [15]

[3]match::Pat k→k→Match k ()[E]
For any key type , the  function takes a pattern of type ,
and a key of type , and returns a monadic match of type , where
and  are associated types of .
Matching can fail or can return many results, so  is a :
[3]mzero::MonadPlus m⇒m a[E]

[3]mplus::MonadPlus m⇒m a→m a→m a[E]
To make this more concrete, here is a possible  instance for :
[B]instance Matchable AlphaExpr where[E]

[3]type Pat [15]

[3]type Match [15]

Let's look at the pieces, one at a time.

§.§.§ Patterns

A pattern  over  can be defined like this:
[B]data PatExpr=P PatKeys AlphaExpr[E]

[B]type PatKeys=Map PatVar PatKey[E]

[B]type PatVar[14]

[B]type PatKey[14]
A pattern  is a pair of an  and a  that maps
each of the quantified pattern variables to a canonical De Bruijn .
Just as in <Ref>,  make the pattern insensitive to
the particular names, and order of quantification, of the pattern variables.
We canonicalise the quantified pattern variables before starting a lookup,
numbering pattern variables in the order they appear in a left-to-right scan.
For example

\begin{array}{r@{\hspace{5mm}}l}
\text{Original pattern} & \text{Canonical \ensuremath{\conid{PatExpr}}} \\
\ensuremath{([\mskip1.5mu \varid{a},\varid{b}\mskip1.5mu],\varid{f}\;\varid{a}\;\varid{b}\;\varid{a})}  &  \ensuremath{\conid{P}\;[\mskip1.5mu \varid{a}\mapsto\mathrm{1},\varid{b}\mapsto\mathrm{2}\mskip1.5mu]\;(\varid{f}\;\varid{a}\;\varid{b}\;\varid{a})}\\
\ensuremath{([\mskip1.5mu \varid{x},\varid{g}\mskip1.5mu],\varid{f}\;(\varid{g}\;\varid{x})}  &  \ensuremath{\conid{P}\;[\mskip1.5mu \varid{x}\mapsto\mathrm{2},\varid{g}\mapsto\mathrm{1}\mskip1.5mu]\;(\varid{f}\;(\varid{g}\;\varid{x}))}
\end{array}

§.§.§ The matching monad

There are many possible implementation of the  monad, but here is one:
[B]type MatchExpr v=MR (StateT Subst [1.5mu 1.5mu] v)[E]

[B]type Subst=Map PatKey Expr[E]
The  type is isomorphic to ;
matching takes a substitution for pattern variables (more precisely, their
canonical s), and yields a possibly-empty list of values paired
with an extended substitution.  Notice that the substitution binds pattern keys
to , not , because the pattern variables cannot mention lambda-bound
variables within the target expression.

The formulation in terms of  endows us with just the right
and  instances, as well as favorable performance
because of early failure on contradicting es and the ability to
share work done while matching a shared prefix of multiple patterns.

The monad comes with some auxiliary functions that we will need later:
[B]runMatchExpr::MatchExpr v→[1.5mu (Subst,v)1.5mu][E]

[14]::Maybe v→MatchExpr v[E]

[14]::(Subst→Maybe Subst)→MatchExpr ()[E]
Their semantics should be apparent from their types.  For example,
runs a  computation, starting with an empty , and
returning a list of all the successful  matches.

§.§.§ Matching summary

The implementation of  is entirely straightforward, using
simultaneous recursive descent over the pattern and target.
The code is given in the Appendix.

The key point is this: nothing in this section is concerned with
tries.  Here we are simply concerned with the mechanics of matching,
and its underlying monad.  There is ample room for flexibility. For
example, if the key terms had two kinds of variables (say type
variables and term variables) we could easily define  to carry
two substitutions; or  could return just the first result
rather than a list of all of them; and so on.

§.§ The matching trie class

The core of our matching trie is the class , which
generalises the  class of <Ref>:
[B]class Matchable (MKey tm)⇒MTrieMap tm where[E]

[3]type MKey tm[21]

[17]::tm v[E]

[17]::MKey tm→tm v→Match (MKey tm) v[E]

[17]::Pat (MKey tm)→TF v→tm v→tm v[E]
The lookup function takes a key of type  as before, but
it returns something in the  monad, rather than the  monad.
The  takes a pattern (rather than just a key), of type
, and alters the trie's value at that pattern[
Remember, a matching trie represents a set of (pattern,value) pairs.].

We can generalise  (<Ref>) in a similar way:
[B]data MSEMap tm v[19]

[19]|SingleMSEM (Pat (MKey tm)) v[E]

[19]|MultiMSEM [32]
[32](tm v)[E]

[B]instance MTrieMap tm⇒MTrieMap (MSEMap tm) where[E]

[3]type MKey (MSEMap tm)=MKey tm[E]

Notice that  contains a pattern,
not merely a key, unlike  in <Ref>.
The code for  and  is straightforward;
we give the former here, leaving the latter for the Appendix
[B]lkMSEM::MTrieMap tm[31]
[31]⇒MKey tm→MSEMap tm a[E]

[31]→Match (MKey tm) a[E]

[B]lkMSEM k [18]

[B]lkMSEM k [18]
[18](MultiMSEM m)[38]
[38]=lkMTM k m[E]

[B]lkMSEM k [18]
[18](SingleMSEM pat v)[38]
[38]=match pat k>>pure v[E]
Notice the call to  to make the lookup fail if the map is empty; and, in the
case, the call  to match the pattern against the key.

§.§ Matching tries for

Next, we show how to implement a matching triemap for our running
example, .
The data type follows closely the pattern we developed for  (<Ref>):
[B]type MExprMap=MSEMap MExprMap'[E]

[B]data MExprMap' v[E]

[3]=MM [9]
[9]{1.5mu [9E]
[12]mm95 fvar[21]
[21]::Map Var v[41]

[12]mm95 bvar[21]
[21]::Map BoundKey v[41]

[12]mm95 pvar[21]
[21]::Map PatKey v[41]

[12]mm95 app[21]
[21]::MExprMap (MExprMap v)[E]

[12]mm95 lam[21]
[21]::MExprMap v1.5mu}[E]

[B]instance MTrieMap MExprMap' where[E]

[3]type MKey MExprMap'=AlphaExpr[E]

The main difference is that we add an extra field  to ,
for occurrences of a pattern variable.  You can see how this field is used
in the lookup code:
[B]lookupPatMM::$\forall$  v∘. AlphaExpr→MExprMap' v→MatchExpr v[E]

[B]lookupPatMM ae@(A bve e) (MM {1.5mu 1.5mu})[E]

[5]rigid=case e of[E]

[7]Var x[18]
[18]→case lookupDBE x bve of[E]

[9]Just bv[18]
[18]→mm95 bvar[30]
[35]liftMaybe∘. Map.lookup bv[E]

[18]→mm95 fvar[30]
[35]liftMaybe∘. Map.lookup x[E]

[7]App e_1 e_2[18]
[18]→mm95 app[30]
[35]lkMTM (A bve e_1)[E]

[35]lkMTM (A bve e_2)[E]

[7]Lam x e[18]
[18]→mm95 lam[30]
[35]lkMTM (A (extendDBE x bve) e)[E]

[5]flexi=mm95 pvar▹IntMap.toList▹map match95 one▹msum[E]

[5]match95 one::(PatVar,v)→MatchExpr v[E]

[5]match95 one (pv,v)=matchPatVarE pv ae>>pure v[E]
Matching lookup on a trie matches the target
expression against all patterns the trie represents.
The  case is no different from exact lookup; compare the
code for  in <Ref>.  The only difference is that we need
(from <Ref>) to
take the  returned by  and lift it into the  monad.

The  case handles the triemap entries whose pattern is simply one of
the quantified pattern variables; these entries are stored in the new  field.
We enumerate these entries with , to get a list of  pairs,
match each such pair against the target with , and finally accumulate
all the results with .  In turn  uses  to match
the pattern variable with the target and, if successful, returns corresponding
value .

The  function does the heavy lifting, using some
simple auxiliary functions whose types are given below:
[B]matchPatVarE::PatKey→AlphaExpr→MatchExpr ()[E]

[B]matchPatVarE pv (A bve e)=refineMatch$λms→[E]

[3]case Map.lookup pv ms of[E]

[7]|noCaptured bve e[27]
[27]→Just (Map.insert pv e ms)[E]

[5]Just sol[15]

[7]|noCaptured bve e[E]

[7],eqExpr e sol[27]
[27]→Just ms[E]

To match a pattern variable  against an expression ,
we first look up  in the current substitution (obtained from the
state monad.  If  is not bound we simply extend the

But wait!  Consider matching the pattern
against the target .  That's fine: we should succeed, binding
to .  But suppose we match that same pattern against target .
It would be nonsense to “succeed” binding  to , because  is
locally bound within the target.  Hence the  test, which
returns  iff the expression does not mention any of the locally-bound

If  is already bound in the substitution, we have a repeated pattern
variable (see <Ref>), and we must check that
the target expression is equal (using ) to the the one already bound to .
Once again, however, we must check that the target does not contain any locally-bound
variables, hence the  check.

is the trickiest case.  The code for , and
the other operations of the class, is very straightforward, and is given
in the Appendix.

§.§ The external API

The matching tries we have described so far use canonical pattern keys,
a matching monad, and other machinery that should be hidden from the client.
We seek an external API more like this:
[B]type PatMap::Type→Type[E]

[11]::([1.5mu Var1.5mu],Expr)→TF v→PatMap v→PatMap v[E]

[11]::Expr→PatMap v→[1.5mu (PatSubst,v)1.5mu][E]

[B]type PatSubst=[1.5mu (Var,Expr)1.5mu][E]
When altering a  we supply a client-side pattern, which is
just a pair  of the quantified pattern variables and the pattern.
When looking up in a  we supply a target expression, and get back
a list of matches, each of which is a pair of the value and the substitution
for those original pattern variables that made the pattern equal to the target.

So  must canonicalise the client-side pattern variables
before altering the trie; that is easy enough.
But how can  recover the client-side ?
Somehow we must remember the canonicalisation used when inserting
so that we can invert it when matching.   For example, suppose we insert the two
(pattern, value pairs)

\ensuremath{(([\mskip1.5mu \varid{p}\mskip1.5mu],\varid{f}\;\varid{p}\;\conid{True}),\varid{v}_{1})} \quad \text{and} \quad \ensuremath{(([\mskip1.5mu \varid{q}\mskip1.5mu],\varid{f}\;\varid{q}\;\conid{False}),\varid{v}_{2})}

Both patterns will canonicalise their (sole) pattern variable to the De Bruin index 1.
So if we look up the target  the  monad will produce a
final  that maps , paired with the value .  But we want to return
to the client, a  that uses the client variable , not
the internal index 1.

The solution is simple enough: we store the mapping in the triemap's domain,
along with the values, thus:
[B]type PatMap v=MExprMap (PatKeys,v)[E]
Now the code writes itself. Here is :
[B]alterPM::$\forall$  v∘. ([1.5mu Var1.5mu],Expr)→TF v→PatMap v→PatMap v[E]

[B]alterPM (pvars,e) tf pm=atMTM pat ptf pm[E]

[5]pks::PatKeys=canonPatKeys pvars e[E]

[5]pat::PatExpr=P pks (A emptyDBE e)[E]

[5]ptf::TF (PatKeys,v)[E]

[5]ptf Nothing[23]
[23]=fmap (λv→(pks,v)) (tf Nothing)[E]

[5]ptf (Just (,v))[23]
[23]=fmap (λv→(pks,v)) (tf (Just v))[E]

[B]canonPatKeys::[1.5mu Var1.5mu]→Expr→PatKeys[E]
The auxiliary function  takes the client-side pattern ,
and returns a  (<Ref>) that maps each pattern variable
to its canonical De Bruijn index.  is entirely straightforward:
it simply walks the expression, numbering off the pattern variables in
left-to-right order.

Then we can simply call the internal  function,
passing it: a canonical ; and
a transformer  that will pair the  with
the value supplied by the user via .
Lookup is equally easy:
[11]::Expr→PatMap v→[1.5mu (PatSubst,v)1.5mu][E]

[B]lookupPM e pm[E]

[3]=[1.5mu (Map.toList (subst`Map.compose`pks),x)[E]

[29]lkMTM (A emptyDBE e) pm1.5mu][E]
We use  to get a list of successful matches, and then pre-compose
(see <Ref>) the internal  with the  mapping that
is part of the match result. We turn that into a list to get the client-side
. The only tricky point is what to do with pattern variables that are
not substituted. For example, suppose we insert the pattern . No
lookup will bind , because  simply does not appear in the pattern. One
could reject this on insertion, but here we simply return a  with no
binding for .

§.§ Most specific match, and unification

It is tempting to ask: can we build a lookup that returns only the most
specific matches? And, can we build a lookup that returns all values whose
patterns unify with the target. Both would have useful applications, in
GHC at least.

However, both seem difficult to achieve. All our attempts became mired in
complexity, and we leave this for further work, and as a challenge for the
reader. We outline some of the difficulties of unifying lookup in Appendix B.

§ EVALUATION

bar width=7pt,

ylabel=Relative time (lower is better),

extra y ticks=1,
extra y tick style=grid=major, grid style=solid,black,

xticklabels from table=name,
x tick label style=font=,
major x tick style=opacity=0,
x tick label style=yshift=0.5em,

visualization depends on=rawy ,
nodes near coords=

[precision=2,fixed zerofill]
restrict y to domain*=

every node near coord/.append style=

Benchmarks comparing our trie map (TM)
to ordered maps (OM) and hash maps (HM)

So far, we have seen that trie maps offer a significant advantage over other
kinds of maps like ordered maps or hash maps: the ability to do a matching
lookup (in <Ref>). In this section, we will see that query
performance is another advantage. Our implementation of trie maps in Haskell
can generally compete in performance with other map data structures, while
significantly outperforming traditional map implementations on some operations.
Not bad for a data structure that we can also extend to support matching lookup!

We took runtime measurements of the (non-matching)  data
structure on a selection of workloads, conducted using the criterion
benchmarking library
[The benchmark machine runs Ubuntu 18.04 on an Intel Core i5-8500 with
16GB RAM. All programs were compiled on GHC 9.0.2 with  to eliminate code layout flukes and run with  for 128MB space in generation 0 in order to prevent major GCs from
skewing the results.].
<Ref> presents a quick overview of the results.

Appendix A is an extended version of this section, featuring a more in-depth
analysis, finer runtime as well as space measurements and indicators for
statistical significance.

§.§.§ Setup

All benchmarks except fromList are handed a pre-built
map containing 10000 expressions, each consisting of roughly 100  data
constructors drawn from a pseudo-random source with a fixed (and thus
deterministic) seed.

We compare three different non-matching map implementations, simply because we
were not aware of other map data structures with matching lookup modulo
$\alpha$-equivalence and we wanted to compare apples to apples.
The  forms the baseline. Asymptotics are given with respect to map
size $n$ and key expression size $k$:

*  (designated “TM” in <Ref>) is the trie map
implementation from this paper. Insertion and lookup perform at most
one full traversal of the key, so performance should scale with

*  (designated “OM”) is the ordered map implementation from
the mature, well-optimised containers library. It uses size
balanced trees under the hood <cit.>. Thus, lookup and insert
operations incur an additional log factor in the map size $n$, for a
total of $\mathcal{O}(k \log n)$ factor compared to both other maps.

*  (designated “HM”) is an implementation of hash array
mapped tries <cit.> from the unordered-containers
library. Like , map access incurs a full traversal of the key
to compute a hash and then a $\mathcal{O}(\log_{32} n)$ lookup in the
array mapped trie, as well as an expected constant number of key
comparisons to resolve collisions. The log factor can be treated like
a constant for all intents and purposes, so lookup and insert is
effectively in $\mathcal{O}(k)$.

Some clarification as to what our benchmarks measure:

* The lookup benchmark looks up every
expression that is part of the map. So for a map of size 10000, we
perform 10000 lookups of expressions each of which have approximately size

* lookup_lam is like lookup, but wraps a shared
prefix of 100 layers of  around each expression.

* fromList benchmarks a naïve
implementation on  against the tuned  implementations
of the other maps, measuring map creation performance from batches.

§.§.§ Querying

The results suggest that  is about as fast as  for
completely random expressions in lookup. But in a more realistic
scenario, at least some expressions share a common prefix, which is what
lookup_lam embodies. There we can see that  wins against
by a huge margin:  looks at the shared prefix exactly
once on lookup, while  has to traverse the shared prefix of length
$\mathcal{O}(k)$ on each of its $\mathcal{O}(\log n)$ comparisons.

Although  loses on most benchmarks compared to  and , most
measurements were consistently at most a factor of two slower than .
We believe that is due to the fact that it is enough to traverse the
twice during lookup barring any collisions (hash and then equate with the
match), thus it is expected to scale similarly as . Thus, both
and  perform much more consistently than .

§.§.§ Modification

While  consistently wins in query performance, the edge is melting into
insignificance for fromList and union. One reason is
the uniform distribution of expressions in these benchmarks, which favors .
Still, it is a surprise that the naïve  implementations of  and
as list folds beat the one of , although the latter has a tricky,
performance-optimised implementation using transient mutability.

What would a non-naïve version of  for  look like? Perhaps
the process could be sped up considerably by partitioning the input list
according to the different fields of  and then calling
the  implementations of the individual fields in turn. The process
would be very similar to discrimination sort <cit.>, which is a
generalisation of radix sort to tree-like data and very close to tries.
Indeed, the discrimination library provides such an optimised
$\mathcal{O}(n)$  implementation for .

§ RELATED WORK

§.§ Matching triemaps in automated reasoning

Matching triemaps, a kind of term index, have been used in the automated
reasoning community for decades.
An automated reasoning system has
hundreds or thousands of axioms, each of which is quantified over
some variables (just like the RULEs described in <Ref>). Each of these
axioms might apply at any sub-tree of the term under consideration, so efficient
matching of many axioms is absolutely central to the performance of these systems.

This led to a great deal of work on so-called discrimination trees, starting
in the late 1980's, which is beautifully surveyed in the Handbook of Automated Reasoning
All of this work typically assumes a single, fixed, data type of “first order terms”
like this[Binders in terms do not seem to be important
in these works, although they could be handled fairly easily by a De Bruijn pre-pass.]
[3]data MKey=Node Fun [1.5mu MKey1.5mu][E]
where  is a function symbol, and each such function symbol has a fixed arity.
Discrimination trees are described by imagining
a pre-order traversal that (uniquely, since function symbols have fixed arity)
converts the  to a list of type , and treating that as the key.
The map is implemented like this:
[3]data DTree v=DVal v|DNode (Map Fun DTree)[E]

[3]lookupDT::[1.5mu Fun1.5mu]→DTree v→Maybe v[E]

[3]lookupDT [1.5mu 1.5mu] [20]
[20](DVal v)[31]
[31]=Just v[E]

[3]lookupDT (f:fs) [20]
[20](DNode m)[31]
[31]=case Map.lookup f m of[E]

[35]Just dt→lookupDT fs dt[E]

[3]lookupDT  [20]
Each layer of the tree branches on the first , and looks up
the rest of the  in the appropriate child.
Extending this basic setup with matching is done by some kind of backtracking.

Discrimination trees are heavily used by theorem provers, such as Coq, Isabelle, and Lean.
Moreover, discrimination trees have been further developed in a number of ways.
Vampire uses code trees which are a compiled form of discrimination
tree that stores abstract machine instructions, rather than a data structure
at each node of the tree <cit.>.
Spass <cit.> uses substitution trees <cit.>,
a refinement of discrimination trees that can share common sub-trees
not just common prefixes. (It is not clear whether the extra complexity of
substitution trees pays its way.)  Z3 uses E-matching code trees, which solve
for matching modulo an ever-growing equality relation, useful in saturation-based
theorem provers.  All of these techniques except E-matching are surveyed in

If we applied our ideas to  we would get a single-field triemap which
(just like ) would initially branch on , and then go though
a chain of  constructors (which correspond to the  above).
You have to squint pretty hard  — for example, we do the pre-order traversal on the fly
— but the net result is very similar, although
it is arrived at by entirely different thought process.

Many of the insights of the term indexing world re-appear, in different guise,
in our triemaps.   For example, when a variable is repeated in a pattern we can
eagerly check for equality during the match, or instead gather an equality constraint
and check those constraints at the end <cit.>.

§.§ Haskell triemaps

Trie data structures have found their way into numerous Haskell packages over time.
There are trie data structures that are specific to , like the
StringMap package, or polymorphically, requiring just a type class for
trie key extraction, like the TrieMap package. None of these
libraries describe how to index on expression data structures modulo
$\alpha$-equivalence or how to perform matching lookup.

Memoisation has been a prominent application of tries in Haskell
Given a function , the idea is to build an infinite,
lazily-evaluated trie, that maps every possible argument  to (a thunk for)
$\ensuremath{(\varid{f}\;\varid{x})}$.  Now, a function call becomes a lookup in the trie.
The ideas are implemented in the MemoTrie library.
For memo tries, operations like alter, insert, union, and fold are all
irrelevant: the infinite trie is built once, and then used only for lookup.

A second strand of work concerns data type generic, or polytypic, approaches to
generating tries, which nicely complements the design-pattern approach
of this paper (<Ref>).
<cit.> describes the polytypic approach,
for possibly parameterised and nested data types in some detail, including the
realisation that we need  and  in order to define  and
A generalisation of those ideas then led to functor-combo. The
representable-tries library observes that trie maps are representable
functors and then vice versa tries to characterise the sub-class of
representable functors for which there exists a trie map implementation.

The twee-lib library defines a simple term index data structure based
on discrimination trees for the twee equation theorem prover. We would
arrive at a similar data structure in this paper had we started from an
expression data type
[B]data Expr=App Con [1.5mu Expr1.5mu]|Var Var[E]
In contrast to our , twee's  does path compression not
only for paths ending in leaves (as we do) but also for internal paths, as is
common for radix trees.

It is however unclear how to extend twee's  to support
$\alpha$-equivalence, hence we did not consider it for our benchmarks in

We warmly thank Leonardo de Moura and Edward Yang for their very helpful feedback.

§ CONCLUSION

We presented trie maps as an efficient data structure for representing a set of
expressions modulo $\alpha$-equivalence, re-discovering polytypic deriving
mechanisms described by <cit.>. Subsequently, we showed how to
extend this data structure to make it aware of pattern variables in order to
interpret stored expressions as patterns. The key innovation is that the
resulting trie map allows efficient matching lookup of a target expression
against stored patterns. This pattern store is quite close to discrimination
trees <cit.>, drawing a nice connection to term indexing problems
in the automated theorem proving community.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonStephen Adams.
Functional Pearls Efficient sets—a balancing
journalJournal of Functional Programming
volume3, number4 (year1993),

authorpersonPhil Bagwell.
booktitleIdeal Hash Trees.
typeTechnical Report.
institutionInfoscience Department, École Polytechnique Fédérale
de Lausanne.

[Chakravarty et al(2005)]
authorpersonManuel M. T. Chakravarty,
personGabriele Keller, and personSimon Peyton
Jones. year2005.
Associated Type Synonyms. In
booktitleProceedings of the Tenth ACM SIGPLAN International
Conference on Functional Programming (Tallinn, Estonia)
(seriesICFP '05). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Connelly and Morris(1995)]
authorpersonRichard Connelly and
personF Lockwood Morris. year1995.
A generalization of the trie data structure.
journalMathematical structure in computer science
volume5 (year1995), pages381–418.
Issue 3.

[de Bruijn(1972)]
authorpersonN.G de Bruijn.
Lambda calculus notation with nameless dummies, a
tool for automatic formula manipulation, with application to the
Church-Rosser theorem.
journalIndagationes Mathematicae (Proceedings)
volume75, number5 (year1972),

authorpersonConal Elliott.
titleComposing memo tries.

authorpersonConal Elliott.
titleElegant memoization with functional memo tries.

[Graf and Meyer(1996)]
authorpersonP Graf and personC Meyer.
Advanced indexing operations on substitution
trees. In booktitleProc International Conference on
Automated Deduction (CADE'96), LNCS 1104,
editorpersonMA McRobbie and personSlaney
JK (Eds.). publisherSpringer.

authorpersonFritz Henglein.
Generic Discrimination: Sorting and Paritioning
Unshared Data in Linear Time.
journalSIGPLAN Not. volume43,
number9 (dateSept. year2008),

authorpersonRalf Hinze.
Generalizing Generalized Tries.
journalJournal of Functional Programming
volume10, number4 (year2000),

authorpersonRalf Hinze.
Memo Functions, Polytypically!. In
booktitleProceedings of the 2nd Workshop on Generic
Programming, Lima‚ Portugal. pages17–32.

[Najd and Peyton Jones(2017)]
authorpersonShayan Najd and personSimon
Peyton Jones. year2017.
Trees that grow.
journalJournal of Universal Computer Science
(JUCS)  volume23 (dateJanuary
year2017), pages47–62.

[Peyton Jones et al(2001)]
authorpersonSimon Peyton Jones, personAndrew
Tolmach, and personTony Hoare.
Playing by the rules: rewriting as a practical
optimisation technique in GHC. In booktitle2001 Haskell
Workshop (edition2001 haskell workshop ed.). ACM SIGPLAN,

authorpersonAndré Luís De Medeiros Santos.
titleCompilation by Transformation in Non-Strict
Functional Languages.
thesistypePh. D. Dissertation.
schoolUniversity of Glasgow.

[Sekar et al(2001)]
authorpersonR Sekar, personIV Ramakrishnan,
and personA Voronkov. year2001.
booktitleHandbook of Automated Reasoning.
Vol. volume2.

authorpersonA Voronkov.
The anatomy of Vampire: Implementing bottom-up
procedures with code trees.
journalJournal of Automated Reasoning
volume15 (year1995), pages237–265.
Issue 2.

[Weidenbach et al(2009)]
authorpersonChristoph Weidenbach,
personDilyana Dimova, personArnaud Fietzke,
personRohit Kumar, personMartin Suda, and
personPatrick Wischnewski. year2009.
SPASS Version 3.5. In
booktitleProc International Conference on Automated
Deduction (CADE). publisherSpringer,

§ EVALUATION

So far, we have seen that trie maps offer a significant advantage over other
kinds of maps like ordered maps or hash maps: the ability to do a matching
lookup (in <Ref>). In this section, we will see that query
performance is another advantage. Our implementation of trie maps in Haskell
can generally compete in performance with other map data structures, while
significantly outperforming traditional map implementations on some operations.
Not bad for a data structure that we can also extend to support matching lookup!

§.§ Runtime

Benchmarks of different operations over our trie map  (TM),
ordered maps  (OM) and hash maps  (HM), varying the
size parameter $N$.  Each map is of size $N$ (so $M=N$) and the expressions
it contains are also each of size $N$ (so $E=N$).
We give the measurements of OM and HM relative to absolute runtime
measurements for TM. Lower is better. Digits whose order of magnitude is
no larger than that of twice the standard deviation are marked by squiggly

$N$      3c10     3c100     3c1000

(lr.5em)2-4 (lr.5em)5-7 (lr.5em)8-10
Data structure     TM     OM     HM
TM     OM     HM
TM     OM     HM

We measured the runtime performance of the (non-matching)  data
structure on a selection of workloads, conducted using the criterion
benchmarking library
[The benchmark machine runs Ubuntu 18.04 on an Intel Core i5-8500 with
16GB RAM. All programs were compiled with  to
eliminate code layout flukes and run with  for 128MB
space in generation 0 in order to prevent major GCs from skewing the results.].
<Ref> presents an overview of the results, while
<Ref> goes into more detail on some configurations.

§.§.§ Setup

All benchmarks except the fromList* variants are handed a pre-built
map containing $N$ expressions, each consisting of roughly $N$  data
constructors, and drawn from a pseudo-random source with a fixed (and thus
deterministic) seed. $N$ is varied between 10 and 1000.

We compare three different non-matching map implementations, simply because we
were not aware of other map data structures with matching lookup modulo
$\alpha$-equivalence and we wanted to compare apples to apples.
The  forms the baseline. Asymptotics are given with respect to map
size $n$ and key expression size $k$:

*  (designated “TM” in <Ref>) is the trie map
implementation from this paper. Insertion and lookup and have to perform
a full traversal of the key, so performance should scale with
$\mathcal{O}(k)$, where $k$ is the key  that is accessed.

*  (designated “OM”) is the ordered map implementation from
the mature, well-optimised containers library. It uses size
balanced trees under the hood <cit.>. Thus, lookup and insert
operations incur an additional log factor in the map size $n$, for a
total of $\mathcal{O}(k \log n)$ factor compared to both other maps.

*  (designated “HM”) is an implementation of hash array
mapped tries <cit.> from the unordered-containers
library. Like , map access incurs a full traversal of the key
to compute a hash and then a $\mathcal{O}(\log_{32} n)$ lookup in the
array mapped trie. The log factor can be treated like a constant for all
intents and purposes, so lookup and insert is effectively in

Benchmarks ending in _lam, _app1, _app2
add a shared prefix to each of the expressions before building the initial

* _lam wraps $N$ layers of  around each expression

* _app1 wraps $N$ layers of  around each expression

* _app2 wraps $N$ layers of  around each expression

where  is a name that doesn't otherwise occur in the generated expressions.

* The lookup* family of benchmarks looks up every
expression that is part of the map. So for a map of size 100, we
perform 100 lookups of expressions each of which have approximately size
100. lookup_one looks up just one expression that is
part of the map.

* insert_lookup_one inserts a random expression into the
initial map and immediately looks it up afterwards. The lookup is to
ensure that any work delayed by laziness is indeed forced.

* The fromList* family benchmarks a naïve
implementation on  against the tuned  implementations
of the other maps, measuring map creation performance from batches.

* fold simply sums up all values that are stored in the map
(which stores s).

§.§.§ Querying

The results show that lookup in  often wins against  and
. The margin is small on the completely random s of
lookup, but realistic applications of  often store
s with some kind of shared structure. The _lam and
_app1 variants show that  can win substantially against
an ordered map representation:  looks at the shared prefix exactly
once one lookup, while  has to traverse the shared prefix of length
$\mathcal{O}(N)$ on each of its $\mathcal{O}(\log N)$ comparisons. As
a result, the gap between  and  widens as $N$ increases,
confirming an asymptotic difference. The advantage is less pronounced in
the _app2 variant, presumably because  can't share
the common prefix here: it turns into an unsharable suffix in the pre-order
serialisation, blowing up the trie map representation compared to its sibling

Although  loses on most benchmarks compared to  and , most
measurements were consistently at most a factor of two slower than .
We believe that is due to the fact that it is enough to traverse the  once
to compute the hash, thus it is expected to scale similarly as .

Comparing the lookup* measurements of the same map data
structure on different size parameters $N$ reveals a roughly quadratic correlation
throughout all implementations, give or take a logarithmic factor.
That seems plausible given that $N$ linearly affects expression size and map
size (and thus, number of lookups). But realistic workloads tend to have much
larger map sizes than expression sizes!

Varying expression size $E$ and map size $M$ independently on benchmarks
lookup and insert_lookup_one.

2c2*$E$$M$     3c10

(lr.5em)3-5 (lr.5em)6-8 (lr.5em)9-12 (lr.5em)12-14
TM     OM     HM
TM     OM     HM
TM     OM     HM
TM     OM     HM

Let us see what happens if we vary map size $M$ and expression
size $E$ independently for lookup. The results in
<Ref> show that  scales better than  when we
increase $M$ and leave $E$ constant. The difference is even more pronounced than
in <Ref>, in which $N = M = E$.

The time measurements for  appear to grow almost linearly with $M$.
Considering that the number of lookups also increases $M$-fold, it seems the
cost of a single lookup remained almost constant, despite the fact that we store
varying numbers of expressions in the trie map. That is exactly the strength
of a trie implementation: Time for the lookup is in $\mathcal{O}(E)$, i.e.,
linear in $E$ but constant in $M$. The same does not hold for search trees,
where lookup time is in $\mathcal{O}(P \log M)$. $P \in \mathcal{O}(E)$ here and
captures the common short circuiting semantics of the lexicographic order on
. It denotes the size of the longest shared prefix of all expressions.

By contrast, fixing $M$ but increasing $E$ makes  easily catch up
on lookup performance with , ultimately outpacing it. The shared prefix
factor $P$ for  remains essentially constant relative to $E$: larger
expressions still are likely to differ very early because they are random.
Increasing $M$ will introduce more clashes and is actually more likely to
increase $P$ on completely random expressions. As written above, realistic
work loads often have shared prefixes like lookup_app1, where
we already saw that  outperforms . The fact that  performance
depends on $P$ makes it an extremely workload dependent pick, leading to
compiler performance that is difficult to predict.  shows performance
consistent with  but is a bit slower, as before. There is no subtle
scaling factor like $P$; just plain predictable $\mathcal{O}(E)$ like .

Returning to <Ref>, we see that folding over s is
considerably slower than over  or . The complex tree structure is
difficult to traverse and involves quite a few indirections.
This is in stark contrast to the situation with , where it's just a
textbook in-order traversal over the search tree. Folding over
performs similarly to .

We think that  folding performance dies by a thousand paper cuts: The
lazy fold implementation means that we allocate a lot of thunks for intermediate
results that we end up forcing anyway in the case of our folding operator .
That is a price that  and  pay, too, but not nearly as much as the
implementation of  does.
Furthermore, there's the polymorphic recursion in the head case of
with a different folding function , which allocates on each call
and makes it impossible to specialise  for a fixed folding function
like  with the static argument transformation <cit.>. Hence
we tried to single out the issue by ensuring that  and  in
fact don't specialise for  when running the benchmarks, by means of a
Another possible reason might be that the code generated for  is quite
a lot larger than the code for , say, so we are likely measuring caching
We are positive there are numerous ways in which the performance of
can be improved, but believe it is unlikely to exceed or just reach the
performance of .

§.§.§ Building

The insert_lookup_one benchmark demonstrates that  also
wins on insert performance, although the defeat against  for size
parameters beyond 1000 is looming. Again, <Ref> decouples
map size $M$ and expression size $E$. The data suggests that in comparison to
, $E$ indeed affects insert performance of  linearly. By contrast,
$M$ does not seem to affect insert performance at all.

The small edge that  seems to have over  and
doesn't carry over to its naïve  implementation, though.  wins
the fromList benchmark, albeit with  as a close second.
That is a bit surprising, given that 's  quickly falls back to a
list fold like  on unsorted inputs, while  has a less naïve
implementation: it makes use of transient mutability and performs destructive
inserts on the map data structure during the call to , knowing that
such mutability can't be observed by the caller. Yet, it still performs worse
than  or  for larger $E$, as can be seen in

We expected  to take the lead in fromList_app1. And indeed
it does, outperforming  for larger $N$ which pays for having to compare the
shared prefix repeatedly. But  is good for another surprise and keeps
on outperforming  for small $N$.

What would a non-naïve version of  for  look like? Perhaps
the process could be sped up considerably by partitioning the input list
according to the different fields of  like  and then calling
the  implementations of the individual fields in turn. The process
would be very similar to discrimination sort <cit.>, which is a
generalisation of radix sort to tree-like data and very close to tries.
Indeed, the discrimination library provides such an optimised
$\mathcal{O}(N)$  implementation for ordered maps.

The union* benchmarks don't reveal anything new;  and
win for small $N$, but  wins in the long run, especially when there's
a sharable prefix involved.

§.§ Space

Varying expression size $E$ and map size $M$ while measuring the
memory footprint of the different map implementions on 4 different expression
populations. Measurements of  (OM) and  (HM) are displayed as
relative multiples of the absolute measurements on  (TM). Lower is
better. †indicates heap overflow.

2c2*$E$$M$     3c10

(lr.5em)3-5 (lr.5em)6-8 (lr.5em)9-12 (lr.5em)12-14
TM     OM     HM
TM     OM     HM
TM     OM     HM
TM     OM     HM

We also measured the memory footprint of  compared to  and
. The results are shown in <Ref>. All four benchmarks simply
measure the size on the heap in bytes of a map consisting of $M$ expressions of
size $E$. They only differ in whether or not the expressions have a shared
prefix. As before, space is built over completely random expressions,
while the other three benchmarks build maps with common prefixes, as discussed in

In space, prefix sharing is highly unlikely for reasons discussed
in the last section: Randomness dictates that most expressions diverge quite
early in their prefix. As a result,  consumes slightly more space
than both  and , the latter of which wins every single instance.
The difference here is ultimately due to the fact that inner nodes in the trie
allocate more space than inner nodes in  or .

However, in space_app1 and space_lam, we can see that
is able to exploit the shared prefixes to great effect: For big
$M$, the memory footprint of space_app1 approaches that of
space because the shared prefix is only stored once. In the other
dimension along $E$, memory footprint still increases by similar factors as
in space. The space_lam family does need a bit more
bookkeeping for the de Bruijn numbering, so the results aren't quite as close to
space_app1, but it's still an easy win over  and .

For space_app2,  can't share any prefixes because the
shared structure turns into a suffix in the pre-order serialisation. As a result,
and  allocate less space, all consistent constant factors apart
from each other.  wins here again.

§ TRIEMAPS THAT UNIFY?

In effect, the s of the patterns stored in our matching triemaps act
like unification variables. The unification problems we solve are always
particularly simple, because pattern variables only ever match against are
expression keys in which no pattern variable can occur.

Another frustrating point is that we had to duplicate the  class in
<Ref> because the key types for lookup and insertion no
longer match up. If we managed to generalise the lookup key from expressions to
patterns, too, we could continue to extend good old .
All this begs the question: Can we extend our idiomatic triemaps to facilitate
unifying lookup?

At first blush, the generalisation seems simple. We already carefully confined
the matching logic to . It should be possible to generalise to
[B]class (Eq k,MonadPlus (Unify k))⇒Unifiable k where[E]

[3]type Unify k::Type→Type[E]

[3]unify::k→k→Unify k ()[E]

[B]class (Unifiable (Key tm),TrieMap tm)⇒UTrieMap tm where[E]

[3]lookupUniUTM::Key tm→tm v→Unify (Key tm) v[E]
But there are problems:

* We would need all unification variables to be globally unique lest we
open ourselves to numerous shadowing issues when reporting unifiers.

* Consider the Unimap for

(([a], T\;a\;A), v1) \quad \text{and} \quad (([b], T\;b\;B), v2)

After canonicalisation, we get

((T\;\pv{1}\;A), ([(a,\pv{1})], v1)) \quad \text{and} \quad (T\;\pv{1}\;B, ([(b,\pv{1})], v2))

and both patterns share a prefix in the trie.
Suppose now we uni-lookup the pattern $([c,d], T c d)$.
What should we store in our  when unifying $c$ with $\pv{1}$?
There simply is no unique pattern variable to decanonicalise to!
In general, it appears we'd get terms in the range of our substitution that
mix s and s. Clearly, the vanilla  datatype doesn't
accomodate such an extension and we'd have to complicate its definition with
techniques such as Trees that Grow <cit.>.

So while embodying full-blown unification into the lookup algorithm seems
attractive at first, in the end it appears equally complicated to present.