HaskellメタプログラミングによるEgisonのパターンマッチの実装— Meta-Programming in Haskell for Non-linear Pattern
Matching with Backtracking for Non-free Data Types
Nov 9, 2019
Satoshi Egi
Rakuten Institute of Technology
Rakuten, Inc.

Egison — a functional language that features expressive pattern matching

S. Egi and Y. Nishiwaki: “Non-linear Pattern Matching with Backtracking for Non-free
Data Types”, APLAS 2018 https://arxiv.org/pdf/1808.10603.pdf!2

MiniEgison: a new pattern-matching library for Haskell

This presentation introduces the implementation of miniEgison, aHaskell library that provides the pattern-matching facility of Egison,
which is compilable and type-inferable by GHC.

Haskell program that enumerates twin primes by pattern matching.

!3

MiniEgison: a new pattern-matching library for Haskell

MiniEgison is implemented utilizing the following Haskell features(GHC extensions):• Template Haskell;• generalized algebraic data types;• existential types;• datatype promotion;• multi-parameter type classes.
This presentation shows how these Haskell
features are utilized for implementing miniEgison.
!4

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!5

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!6

Tutorial: the matchAll expression!7

Tutorial: the matchAll expression

TargetPattern

Body!8

Tutorial: the matchAll expression

What is MatchAll?

What is matcher?

This expression has two characteristic parts.
!9

Tutorial: the matchAll expression

What is MatchAll?

What is matcher?

MatchAll returns a list of all pattern-matching
results.
!10

Tutorial: the matchAll expression

What is MatchAll?

What is matcher?

Matcher specifies the pattern matching method.
!11

Tutorial: ad-hoc polymorphism of patterns

Pattern-matching result depends on matchers.

The pattern-matching algorithms for List andMultiset are user-defined.
!12

Tutorial: non-linear pattern matching• (Mini)Egison can handle non-linear patterns.
• Non-linear patterns allow to refer to the value bound to thepattern variables appear in the left-side of the pattern.
• # is used to denote the value pattern.
• The expression that follows after # is evaluated and equality
against the target is checked.
!13

Tutorial: non-linear pattern matching with backtracking• (Mini)Egison uses backtracking for traversing thesearch trees.
• Therefore, no unnecessary enumerations occur like(naively implemented) pattern guards.
!14

Tutorial: infinitely many pattern-matching results!15

Tutorial: the match expression!16

Tutorial: the match expression!17

Tutorial: list functions in pattern-matching-oriented programming!18

Tutorial: list functions in pattern-matching-oriented programming• join splits a list into two lists.
• $x is matched to each element of the list.

!19

Tutorial: list functions in pattern-matching-oriented programming• A nested join-cons pattern is used fordescribing concat.

!20

Tutorial: list functions in pattern-matching-oriented programming• The not-pattern is used fordescribing a pattern for unique.
• This not-pattern describes thatthe element x does not appear
again.

!21

Tutorial: list functions in pattern-matching-oriented programming• Pattern-matching against a tuple is often used for comparing two data.
!22

Tutorial: SAT solver (Davis-Putnam Algorithm)!23

Tutorial: SAT solver (Davis-Putnam Algorithm)• dp takes a list of propositional variables
and a logical formula in CNF.
• Propositional variables and literals are
represented using integers.
• e.g. P -> 1, Q -> 2, ¬P -> -1.
• CNF is represented as a multiset of
multisets of literals.
• e.g. (P ∨ Q) ∧ (¬Q ∨ R) ∧ (¬P ∨ ¬R) ->{{1,2},{-2,3},{-1,-3}}• dp returns True when the given formula is satisfiable, otherwise
returns False.

!24

Tutorial: SAT solver (Davis-Putnam Algorithm)• vars and cnf are pattern-matched as amultiset of integers and a multiset of
multisets of integers, respectively.

!25

Tutorial: SAT solver (Davis-Putnam Algorithm)• If cnf is empty, cnf is satisfiable.

!26

Tutorial: SAT solver (Davis-Putnam Algorithm)• If cnf contains an empty clause,
cnf is unsatisfiable.

!27

Tutorial: SAT solver (Davis-Putnam Algorithm)• If cnf contains a clause that consistsof a single literal x, we can assign x
true at once.

!28

Tutorial: SAT solver (Davis-Putnam Algorithm)• If a propositional variable v appears
only positively in cnf, we can assign
v true at once.

!29

Tutorial: SAT solver (Davis-Putnam Algorithm)• If a propositional variable v appears
only negatively in cnf, we can assign
v false at once.

!30

Tutorial: SAT solver (Davis-Putnam Algorithm)• Otherwise, we apply the resolution
principle.
!31

Tutorial: SAT solver (Davis-Putnam Algorithm)• Egison pattern matching dramatically
improves the readability of programs.

!32

Tutorial: the essence of pattern-matching-oriented programming

There are two kinds of loops in programming:

Loops that narrow the
search space
Loops that can be
described by simple
backtracking
Functional programming
mixes these loops together
in a program.
!33

Tutorial: the essence of pattern-matching-oriented programming

There are two kinds of loops in programming:

Loops that narrow the
search space
Loops that can be
described by simple
backtracking
Functional programming
mixes these loops together
in a program.

=

Loops that narrow the
search space

Egison patternmatching
Pattern-matching-oriented
programming confines the later kind ofloops in patterns.
!34

Tutorial: SAT solver (Davis-Putnam Algorithm)• Pattern-matching-oriented
programming allows us to concentrateon describing the essential parts(loops) of algorithms.

!35

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!36

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!37

Scheme macros for Egison pattern matchingCompilation of Egison Pattern Matching to dynamically typed
programming languages (e.g., Scheme and Lisp) has been alreadyproposed.
The remaining problem is compilation for statically typed
languages (e.g., Haskell).
S. Egi: “Scheme Macros for Non-linear Pattern Matching with Backtracking for Non-free Data
Types”, Scheme Workshop 2019

MiniEgison takes a similar approach with the Scheme macros.

!38

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!39

Typing rules for matchAll and patterns

Unpublished work by Kawata and Egi designed a type system for Egison.

!40

Typing rules for matchAll!41

Typing rules for matchAll• Matcher and Pattern are built-in type operators:• Matcher T is a type for matchers for T;• Pattern T is a type for patterns for T.

!42

Typing rules for matchAll• Matcher and Pattern are built-in type operators:• Matcher T is a type for matchers for T;• Pattern T is a type for patterns for T.

• matchAll takes a matcher and a pattern for thesame type with the target.

!43

Typing rules for matchAll• Patterns have the special judgement operator forhandling non-linear patterns.

• ε and Δ denotes the a type environment for patterns.
• ε denotes an empty type environment.
• ε is an input type environment.
• Δ is an output type environment.
!44

Typing rules for matchAll• Patterns have the special judgement operator forhandling non-linear patterns.

• ε and Δ denotes the a type environment for patterns.
• ε denotes an empty type environment.
• ε is an input type environment.
• Δ is an output type environment.
• Δ is used for evaluating the body of the match clause.

!45

Typing rules for patterns!46

Typing rules for patterns• Wildcards and value patterns make no new bindings.
!47

Typing rules for patterns• A pattern variable adds a new binding to the type environment.
• If $x is the Pattern T, then x has the type T.
!48

Typing rules for patterns• A constructor pattern passes the type environment from left toright to handle non-linear patterns.
!49

Typing rules for matchAll and patterns

Translating Egison pattern matching expressions to a Haskell programon which the Haskell type system does type-checking equivalent to theabove typing rules is challenging!

!50

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!51

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!52

Typing the matchAll expression!53

Typing the matchAll expression• MatchAll takes a target, a matcher, and match clauses
and returns the results.

• a: the type of the target.
• m: the type of the matcher.
• b: the type of the body of matchclause.

!54

Typing the matchAll expression — matchers• Matcher is a type class with no methods.

• The name of the type and data constructor of Eql are identical.
• This instance declaration asserts that Eql is a matcher for athat is an instance of Eq.
!55

Typing the matchAll expression — matchers• Matcher is a type class with no methods.
• A multiple type class is effectively used
to describe the relation between amatcher and a type of target data.
• The name of the type and data constructor of Eql are identical.
• This instance declaration asserts that Eql is a matcher for athat is an instance of Eq.
!56

Typing the matchAll expression — match clauses!57

Typing the matchAll expression — match clauses• vs is the type of the pattern-matching results.

• vs is a list of types (a type-level list).

!58

Typing the matchAll expression — match clauses• The type vs is existentially quantified.

• This is because each pattern of the match clauses in the same
pattern-matching expression generally makes different bindings.

!59

Typing the matchAll expression — match clauses• The type vs is existentially quantified.

• This is because each pattern of the match clauses in the same
pattern-matching expression generally makes different bindings.
• Existential types are effectively used tohide vs from the type of MatchClause.

!60

Typing the matchAll expression — match clauses• mc is a quasi-quoter of Template Haskell for
describing match clause concisely.

!61

Typing the matchAll expression — match clauses• mc is a quasi-quoter of Template Haskell for
describing match clause concisely.
• The body of match clause is transformed to afunction that takes a heterogeneous list.

!62

Typing the matchAll expression — match clauses• Template Haskell is effectively used for
concise notation of match clauses.

• mc is a quasi-quoter of Template Haskell for
describing match clause concisely.
• The body of match clause is transformed to afunction that takes a heterogeneous list.

!63

Typing the matchAll expression — patterns• ctx: the type of the intermediate patternmatching result (the values bound to thepattern variables in the left-side of thepattern).
• vs: the type of the values bound to thepattern variables appear in this pattern.

!64

Typing the matchAll expression — patterns• Datatype promotion (DataKinds extension)is effectively used to represent the type of
pattern-matching results.
• ‘[] represent a type of the empty list.
• ‘[a] represent a type of the list that
contains single element a.

• GADTs allow vs (the 4th parameter of Pattern)changes for each data constructor (vs of
Wildcard is ‘[], vs of PatVar is ‘[a]).
!65Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!66

Overview of the pattern-matching algorithm inside miniEgison

Stack of matching atoms

Intermediate pattern-matching result

Pattern matching algorithm is defined as
reduction of matching states.
!67

Overview of the pattern-matching algorithm inside miniEgison

Pattern

Matcher

TargetA matching atom consists of a pattern, matcher, and target.
!68

Overview of the pattern-matching algorithm inside miniEgison

Next matching states are generated from thedefinition of cons in the multiset matcher.

1
2
3
!69

Overview of the pattern-matching algorithm inside miniEgison

Next matching states are generated from thedefinition of cons in the multiset matcher.

1
We examine only the reduction of this matching state.

2
3
!70

Overview of the pattern-matching algorithm inside miniEgison

The target 2 is added to the intermediate pattern-matching
result because the pattern is a pattern variable.

Next matching states are generated from the definition ofcons in the multiset matcher.

1

This matching state fails topattern-match and vanishes.

2!71

Overview of the pattern-matching algorithm inside miniEgison

The target 2 is added to the intermediate pattern-matching
result because the pattern is a pattern variable.

Next matching states are generated from the definition ofcons in the multiset matcher.

1

We examine the reduction of thismatching state.

2!72Overview of the pattern-matching algorithm inside miniEgison

The value pattern matches with the target and thematching atom is popped off.

The wildcard matches with any target.

If the stack of matching atoms becomes
empty, pattern matching succeeds.
!73

Typing matching atoms and matching states!74

Typing matching atoms and matching states• A matching atom is a triple of a pattern,a matcher, and a target.

!75

Typing matching atoms and matching states• a and m are existentially quantified.
• The reason is because the types of thetargets of the matching atoms in a stackof matching atoms are generally
different.

!76

Typing matching atoms and matching states• a and m are existentially quantified.
• The reason is because the types of thetargets of the matching atoms in a stackof matching atoms are generally
different.

• Existential types are effectively used tohide a and m from the type of MAtom.

!77

Typing matching atoms and matching states• MList is a datatype for a stack ofmatching atoms.
• ctx: the type of intermediate patternmatching results.
• vs: the type of the values bound byprocessing this MList itself.

!78

Typing matching atoms and matching states• MList is a datatype for a stack ofmatching atoms.
• ctx: the type of intermediate patternmatching results.
• vs: the type of the values bound byprocessing this MList itself.

!79

Typing matching atoms and matching states• MList is a datatype for a stack ofmatching atoms.
• ctx: the type of intermediate patternmatching results.
• vs: the type of the values bound byprocessing this MList itself.
• vs of MNil is an empty list.

!80Typing matching atoms and matching states!81

Typing matching atoms and matching states• The pattern-matching result of the firstmatching atom is appended to theintermediate result of the rest matchingatoms.
• :++: is a type operator for the type-level
append operation.

!82

Typing matching atoms and matching states• The concatenation of the pattern-matching
result (xs) of the first matching atom andthe rest matching atoms (ys) are the resultof the whole stack of matching atoms.

!83

Typing matching atoms and matching states• Datatype promotion (DataKinds extension)is effectively used here.
• ‘[] represent a type of the empty list.
• :++: is defined using TypeFamily.

!84

Typing matching atoms and matching states• GADTs allow vs (the 2nd parameter of MList)changes for each data constructor (vs of MNilis ‘[], vs of MCons is xs :++: ys).

!85

Typing matching atoms and matching states• vs is a type of the final pattern-matching
result.

!86

Typing matching atoms and matching states• MState takes an intermediate patternmatching results (HList xs) and a stackof matching atoms (MList xs ys).
• xs :++: ys is the final pattern-matching
results:!87

matchAllDFS!88

matchAllDFS• The initial matching state is created.

!89matchAllDFS• Each pattern-matching result is mapped to the body of match clause.

!90

matchAllDFS — processMStatesAllDFS• The main loop is tail-recursive.
• It is important for execution performance.

!91

matchAllDFS — processMState!92

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!93UnorderedPair!94

UnorderedPair• The pattern for 2-tuples for which we ignore
the order of elements.

!95

UnorderedPair• upair is a function that takes patterns andreturn a pattern.

!96

UnorderedPair• Let’s look into the definition of upair.

!97

UnorderedPair• The Pattern data constructor is used to define
a user-defined patterns.

!98UnorderedPair• Pattern takes a function that take• a intermediate pattern-matching result,• a matcher, and• a target,• and returns• a list of lists of matching atoms.

!99

UnorderedPair• Pattern takes a function that take• a intermediate pattern-matching result,• a matcher, and• a target,• and returns• a list of lists of matching atoms.

• twoMAtoms is a utility function to create an
MList that consists of two matching atoms.

!100List and Multiset!101

List and Multiset• CollectionPat is a type class for changing
the meaning of nil and cons for eachmatcher.

!102

Value Patterns• The pattern constructor of the value patterns aredefined as a method of type class.
• This is because ad-hoc polymorphism is important forvalue patterns.

!103Value Patterns• valuePat takes a function that takes an intermediate
pattern-matching result.

!104

Value Patterns• A value pattern is rewritten to the function that takes
an intermediate pattern-matching result.

!105

Value Patterns!106Value Patterns!107

Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!108

Experiment the overhead of miniEgison

Functional style

Pattern-matching-oriented style!109

Benchmark results• The overhead of miniEgison is not so large(only 2-4 times in this case).

!110Today’s Contents• Tutorial of MiniEgison• Background• Compilation of Egison Pattern Matching• Type System for Egison Pattern Matching• Implementation of MiniEgison• Typing MatchAll• Typing Matching States and Matching Atoms• User-Defined Pattern-Matching Algorithms• Performance• Conclusion!111

MiniEgison: a new pattern-matching library for Haskell

This presentation showed how miniEgison is implemented utilizing
the following Haskell features (GHC extensions):• Template Haskell is used to transform match clauses;• generalized algebraic data types are used to define patterns;• existential types are used to define match clauses and matchingatoms;• datatype promotion is used to represent intermediate patternmatching results;• multi-parameter type classes are used to type matchers.
!112

Future work

• Implement miniEgison as a GHC extension.
• Implement Egison pattern matching on theorem provers.

!113

Future work

• Implement miniEgison as a GHC extension.
• Implement Egison pattern matching on theorem provers.

!114

Proofs of fundamental theorem of arithmetic in Lean and Lean + Egison.

• Pattern matching for non-free data types (e.g., multisets) will makedescriptions of proofs concise.
!115

Acknowledgments• I thank Mayuko Kori for her help for implementing miniEgison.
• I thank Akira Kawata for implementing a proof-of-concept type system of
Egison in Typed Egison.
• I thank Yuichi Nishiwaki and Matthew Roberts for constructive discussion
while implementing miniEgison.

!116