日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集

GSOL: A Confluence Checker for Haskell
Rewrite Rules
Yao Faustin Date Makoto Hamana
We present a tool GSOL, a confluence checker for GHC. It checks the confluence property for rewrite rules ina Haskell program by using the confluence checker SOL (Second-Order Laboratory). The Glasgow Haskell
Compiler (GHC) allows programmers to use rewrite rules to optimize Haskell programs in the compilation
pipeline. Currently, GHC does not check the confluence of the user-defined rewrite rules. If the rewrite
rules are not confluent then the optimization using these rules may produce unexpected results. Therefore,checking the confluence of rewrite rules is important. We implement GSOL using the plugin mechanism of
GHC and provide three usages: (1) a stand-alone command gsol, (2) checking by Cabal building, and (3)a Web interface http://solweb.mydns.jp/. We demonstrate confluence checking of the rewrite rules in the
Arrow library.

module F where

1 Introduction
The Glasgow Haskell Compiler (GHC) [23]is an open source compiler and interactive environment for the functional language Haskell[22]. It has builtin transformation rules to optimize Haskell programs during the compilation[21] [18] [19]. Programmers can also add rewrite rules
to their code to specify optimizing transformations[20]. The notion of confluence is one of the important properties of rewrite rules known in thetheory of rewriting [16]. Confluence guarantees
the uniqueness of normal forms, which is particularly desirable in functional programming. However, GHC does not attempt to check the confluence of user-defined rewrite rules.
In this paper, we present GSOL, a GHC plugin
to check the confluence of rewrite rules in a Haskell
program. It uses a confluece checker, Second-Order
Laboratory (SOL) [13] [14]. To illustrate our work,
we consider the following Haskell program that involves two rewrite rules.
The code within the {-# ... #-} is called apragma †1 . In the RULES pragma, there are two∗ GSOL: Haskell 中の書換規則のための合流性検証器

This is an unrefereed paper. Copyrights belong to
the Authors.
Yao Faustin Date, 浜名 誠, 群馬大学大学院理工学府,
Gunma University.
†1 The NOINLINE pragma instructs the compiler not
to expand f 99 by using the function definition.
Without this indication, f 99 is inlined to 0 be-{-# RULES"f/0" forall x. f x = 0"f/1" forall x. f x = 1#-}
e = f 99{-# NOINLINE f #-}f :: Integer -> Integerf x = 0
図1

A program with rewrite rules

rules named "f/0" and "f/1". If the the compiler
chooses to apply the rule "f/0" then the expression f 99 is rewritten to 0. If it chooses to apply
the rule "f/1" then the expression f 99 is rewritten to 1. Therefore, they are not confluent. But the
GHC compiler does not notice this non-confluence.
To the best of our knowledge, there is no tool tocheck the confluence of rewrite rules directly froma Haskell program. In the field of term rewriting,a few confluence checkers for higher-order rewrite
systems have been developed [26] [25] [13]. We use
the tool SOL [13] [14] to check the confluence of
GHC rewrite rules. Since SOL has been shown
to be the strongest tool among the existing confluence tools that participated in the Higher-Order
Rewriting category of the International Confluence
Competition 2018 [1] and 2020 [7], we believe thatfore applying the rewrite rules, resulting that norewrite rules are fired.

this is the best choice for confluence checking of
Haskell rewrite rules.
Related work. Rewrite rules have been used as away to automate the optimization process of functional programs [11] [20] [27] [30]. We mention two
recent works.
In [30], Steuwer et al. applied rewrite rules
to transform a high-level functional program intoa low-level functional representation from which
OpenCL code is generated. They showed that thisapproach oﬀered performance on a par with highly
tuned code for multi-core CPUs and GPUs written
by experts.
In [11], a high-level program H was rewritten
into an equivalent program but with lower leverconstructs L. Then the program L went throughcode generation to produce platform specific program. The language of rewriting strategies ELEVATE was used to rewrite high-level RISE program
into low-level RISE program. ELEVATE forced theuser to specify the rules to apply and the order ofapplication. Hence they avoided the issue of nonconfluence.
This work. In the previous works on rewrite
rules for optimizations including [11] [20] [29] [27] [30],confluence and termination of rewrite rules havenot been checked automatically although ensuring
them has been recognized as an important problem.
In this work, we solve this problem by applying
the result of well-established rewriting technology
to the real-world functional programming language
Haskell. We use an automatic confluence checker
SOL to check the confluence of GHC rewrite rules
in a Haskell program.
Organisation. This paper is organised as follows. In §2, we first explain necessary backgroundfor developing GSOL. We then explain our implementation in §3. In §4, we demonstrate an example
of arrows. In §5, we discuss future work.

2 Background
GHC. The compilation process of a Haskell program consists of three big steps: frontend, optimizer, and backend. The frontend consists of parsing, type checking and the transformation into the
GHC’s intermediate language called GHC Core,
implementing System FC [24]. A GHC Core expression consists of variables, literals, abstractions,applications and variable bindings. The optimizer
optimizes the GHC Core program through various

図2

GHC compilation pipelinetransformations. The simplifier implements mostof those transformations using a set of builtin rules[21] [18] [19]. The simplifier can also use rewrite rules
specified in the program. The optimization of a
GHC Core program is divided in a series of Coreto-Core translations. The simplifier is one of them.
The role of the backend is to generate code for different platforms.
GHC plugins. The plugin mechanism of GHC[10] allows programmers to insert their own passes
in the compilation pipeline. We use it to implement a confluence checker. Our plugin receives aCore program, checks local confluence and termination, and outputs the result of the checks but does
not modify the Core program.
GHC rewrite rules. The user can use rewrite
rules in a Haskell program to teach the compiler optimizing transformations specific to their programs[20]. The syntax of rewrite rules is:{-# RULES"name" forall <var>...<var>. f <expr> = <expr>...
#-}

The left-hand side of a rule must be a function application f <expr> where the function f is in thescope. The left-hand side and right-hand side of
the rewrite rules are parsed as Core expressions at
the compile time and forms rewrite rules on Core,
which we call Core rules.
Notion of confluence. Term rewriting [2] [31]is a research field of theoretical computer science.
It studies rewrite relations on term structures us-

MA}} AAA∗∗}}AA~}}
M1AA CR
}M2
AA
}}
∗ A
∗
}
A ~}}
N

図3

M>>

>>
>>


M1>> LCR M2>>∗ >>  ∗
N

Confluence and local confluenceing various relational, order theoretic, and algebraic
methods. There are two important properties ofrewrite relation, namely, termination and confluence. Termination (which means strong normalisation) is to reach the normal form in finite time by
any way of rewriting. Confluence (CR) is a property of the rewrite relation, stating that any two
divergent computation paths are joinable, as shownin the diagram. Confluence ensures the existenceof unique normal forms, which is desirable in functional programming.
To deduce confluence, Newman’s lemma is useful [16]. It states “termination and local confluence
implies confluence”. Local confluence (LCR) is aweakened variant of the confluence property thatstates that if there is two (diﬀerent) ways of one
step rewriting “→” from a term M , then there exists a term N , to which the divergent terms M1 andM1 can be rewritten by many step rewriting “→∗ ”.
To prove local confluence, we should check all
possible situations that admit two ways of rewriting, and also to check their convergence. Insteadof examining possibly infinite number of such situations, it has been shown that checking the joinability of finite number of critical divergent terms,
called critical pairs, is enough to conclude local
confluence [2]. Critical pairs can be enumerated
by computing overlaps between the left-hand sides
of rules using high-order unification. For example,
there is a critical pair (1, 0) in the rewrite rules ofthe module F.hs given in Introduction. Our tool
GSOL can automatically show it as follows:******** Critical pairs ********
1: Overlap (1)-(2)--- X’|-> X -------------(1) |f(X)| => 1(2) f(X’) => 0f(X)
1 <-(1)-/\-(2)-> 0---> 1 =#= 0 <--#NON 1 joinable... (Total 1 CPs)..
NO

This shows that the left-hand sides f(X), f(X’) of

the rules are unifiable by the unifier {X’ 7→ X}. It
produces a term f(X), which is rewritten to two different terms 1, 0 forming a critical pair. If these canbe rewritten to a common term, then we conclude
local confluence. But in this case, these are already diﬀerent normal forms. Therefore, this nonjoinability is an evidence of non-confluence, hence
this outputs NO.
SOL. SOL is an implementation of a formal framework of second-order computation systems, which is
a computational counterpart of second-order algebraic theories [8] [9]. This framework has been usedin [13].
Second-order computation systems are based on
second-order abstract syntax given by the languageof meta-terms [12]:t ::= x | x.t | f (t1 , . . . , tn ) | M [t1 , . . . , tn ].
These forms are respectively variables, abstractions, and function terms, and the last form iscalled a meta-application. A meta-application
M [t1 , . . . , tn ] means: when we instantiate M with aterm s, free variables of s are replaced with (meta)terms t1 , . . . , tn .
The meta-terms have second-order types [13].
Computation rules are pairs of meta-terms.

3 Implementation
We implemented GSOL as a Core plugin to checkthe confluence of GHC rewrite rules. Our plugin
is installed into the beginning of the optimization
pipeline. The plugin proceeds as the following threesteps:
1. Collecting the Core rules.
2. Translating them to SOL rules.
3. Calling SOL for checking. SOL performs thechecking functions and print the output to thestandard output.
The translation of Core rules is done by applying
a structural recursive translation of Core terms toboth sides of each rule. It is basically a known
encoding method used in [13] [14], which encodes
λ-terms to meta-terms.
We provided three ways to use GSOL: (1) astand-alone shell command gsol for a single Haskell
file, (2) checking all files in a Cabal package by
specifying options and using the cabal build command, and (3) a Web interface.

{-# RULES"compose/arr"
forall f g. (arr f) . (arr g)= arr (f . g)"first/arr"
forall f.
first (arr f)= arr (first f)"compose/first" forall f g. (first f) . (first g)= first (f . g)"product/arr"
forall f g. arr f *** arr g= arr (f *** g)"fanout/arr"
forall f g. arr f &&& arr g= arr (f &&& g)"second/arr"
forall f.
second (arr f)= arr (second f)"compose/second" forall f g. (second f) . (second g) = second (f . g)#-}
図4

Rewrite rules in Control.Arrow (excerpt)

4 Example: Arrow
In this section, we demonstrate GSOL by examining the Arrow library of GHC. Arrows [17] [28]provide a way to programming with various computational eﬀects in Haskell. Control.Arrow is alibrary in the Haskell base package. Arrows are
implemented using a type class:class Category a => Arrow a wherearr:: (b -> c) -> a b c
first :: a b c -> a (b,d) (c,d)...

Instances of the arrow class satisfy various laws.
Most important laws are the laws of Freyd category( [28], Fig. 1: Arrow equations), which come fromthe semantics of arrows [15], hence are they valid
for any instance of arrows. Slight diﬀerent specific laws have been described in Control.Arrow as
GHC rewrite rules, which are excerpted in Fig. 4.
Note that the file also includes other extensions including ArrowChoice and their laws†2 . We try tocheck the confluence of them.
(1) Stand-alone command. We check the joinability of critical pairs in the Control.Arrow libraryin the shell by invoking the command:> gsol cri Control_Arrow.hs

It reports 8 critical pairs and all are non-joinable,
such as:7 : first(arr(x.f[x]))F • first(g)

x
xx
x
x
(compose/first)
xx
xx
|xx

first(arr(x.f[x]) • g)

FF
FF
F(first/arr)FFFFF"
̸=arr(first(y.f[y]))• first(g)Since these are normal forms, it shows nonconfluence of the rewrite rules in Control.Arrow,†2 Notice that the rewrite rules defined there arevalid only when the instance is a = (->). But
it is not mentioned in the file Control.Arrow. We
do not know why such specific laws (rather thanthe Freyd category laws) were described as rewrite
rules.

which has not been reported elsewhere†3 .
An intended scenario of the usage of GSOL is that
if the user receives this kind of infomation by applying GSOL, then the user tries to fix it by modifying
the rules or adding new rules. In this respect, reporting the non-confluence information is also an
important feature of GSOL.
Generally, the command gsol has two options:cri for critical pair checking to show local confluence, and sn for termination checking. If no options are given gsol checks both local confluenceand termination. If the rules are locally confluent
and terminating then they are confluent. The command gsol is implemented as invoking GHC withthe plugin SOL.Plugin.
(2) Cabal.
GSOL can also check the confluence of files provided as a Cabal packages. We
consider a sample package myarrows configuring
the Control.Arrow library. The file arrows.cabal
should contain the configuration as:
library myarrows
exposed-modules: Control.Arrowbuild-depends:
base ^>=4.13.0.0, SOL
ghc-options:-fplugin=SOL.Plugin-fplugin-opt=SOL.Plugin:cri

which also requires the SOL package. Invoking
the command cabal build, GSOL is automaticallycalled to check local confluence. One can also checktermination by -fplugin-opt=SOL.Plugin:sn.
(3) Web interface. To ease the checking with
GSOL, we have also developed a web interface,which is available at
http://solweb.mydns.jp/ .
Several examples are already available. Choosing the file Control_Arrow.hs from the pull-down
menu, and “GHC rule” format and “WCR” buttons, the user can get the result (cf. the screenshot,
Fig. 5).
One can also check the Freyd category laws bychoosing the file MyArrow.hs.
†3 This can be joinable by adding a new rule forall
f. arr(f) = f, which is valid again only when

図5

GSOL web interface

5 Summary and Future WorkIn this paper, we presented a tool GSOL, a confluence checker for GHC. It checks the confluence
property for rewrite rules in a Haskell program byusing SOL. We implemented GSOL using the pluginmechanism of GHC and provided three usages: (1)a stand-alone command, (2) Cabal, and (3) a Web
interface. We demonstrated confluence checking of
the rewrite rules in the Arrow library.

polymorphic rewrite rules [14] would be useful.
We believe that our development is also applicable to the termination and confluence checking oftype functions [5] [4]. We plan to apply the technology developed in this paper to them.
Recently, rewrite rules and checking their confluence have been an important topic in dependently
typed programming languages [3] [6]. We also plan
to apply our technology to this field.
参 考 文 献As a future work, we will improve the type translation of Core rules to SOL to deal with type constraints and type variables more properly. In Core
rules, type constraints in type signature in the original program become type parameters. The current translation in GSOL drops the type parameters, which suﬃces for critical pair checking, but
makes termination checking weaker. We need toinvestigate to solve this issue. The framework of

the instance is a = (->).

[ 1 ] Aoto, T., Hamana, M., Hirokawa, N., Middeldorp, A., Nagele, J., Nishida, N., Shintani, K., andZankl, H.: Confluence Competition 2018, Proc. of
FSCD 2018, LIPIcs, Vol. 108, 2018, pp. 32:1–32:5.
[ 2 ] Baader, F. and Nipkow, T.: Term Rewriting and
All That, Cambridge University Press, 1998.
[ 3 ] Blanqui, F.: Type Safety of Rewrite Rules in
Dependent Types, Proc. of FSCD 2020, LIPIcs,
Vol. 167, 2020, pp. 13:1–13:14.
[ 4 ] Chakravarty, M. M. T., Keller, G., and Jones,
S. P.: Associated type synonyms, Proc. of ICFP’05,
2005, pp. 241–253.

[ 5 ] Chakravarty, M. M. T., Keller, G., Jones, S. P.,
and Marlow, S.: Associated types with class, Proc.
of POPL’05, 2005, pp. 1–13.
[ 6 ] Cockx, J., Tabareau, N., and Winterhalter, T.:
The taming of the rew: a type theory with computational assumptions, Proc. ACM Program. Lang.,
Vol. 5, No. POPL(2021), pp. 1–29.
[ 7 ] : Confluence Competition oﬃcial site, 2020.
http://project-coco.uibk.ac.at/2020/.
[ 8 ] Fiore, M. and Hur, C.-K.: Second-Order Equational Logic, Proc. of CSL’10, LNCS 6247, 2010,
pp. 320–335.
[ 9 ] Fiore, M. and Mahmoud, O.: Second-Order Algebraic Theories, Proc. of MFCS’10, LNCS 6281,
2010, pp. 368–380.
[10] : Compiler Plugins, 2020.
https://downloads.haskell.org/~ghc/latest/docs/
html/users_guide/extending_ghc.html.
[11] Hagedorn, B., Lenfers, J., et al.: Achieving
High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies, Proc. ACM Program. Lang., Vol. 4, No. ICFP(2020).
[12] Hamana, M.: Free Σ-monoids: A Higher-order
Syntax with Metavariables, Proc. of APLAS’04,
LNCS 3302, 2004, pp. 348–363.
[13] Hamana, M.: How to prove decidability ofequational theories with second-order computation
analyser SOL, Journal of Functional Programming,Vol. 29, No. e20(2019).
[14] Hamana, M., Abe, T., and Kikuchi, K.: Polymorphic computation systems: Theory and practiceof confluence with call-by-value, Science of Computer Programming, Vol. 187, No. 102322(2020).
[15] Heunen, C. and Jacobs, B.: Arrows, like Monads, are Monoids, Proc. of MFPS 22, ENTCS,
Vol. 158, 2006, pp. 219–236.
[16] Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems,
Journal of ACM, Vol. 27, No. 4(1980), pp. 797–821.
[17] Hughes, J.: Generalising monads to arrows, Sci.
Comput. Program., Vol. 37, No. 1-3(2000), pp. 67–
111.
[18] Jones, S. P. and Santos, A.: Compilation bytransformation in the Glasgow Haskell Compiler,

Functional Programming, Glasgow 1994, Springer,
1995, pp. 184–204.
[19] Jones, S. P. and Santos, A.: A transformationbased optimiser for Haskell, Science of computer
programming, Vol. 32, No. 1-3(1998), pp. 3–47.
[20] Jones, S. P., Tolmach, A., and Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC, Haskell Workshop 2001,
2001.
[21] Jones, S. P., Will, P., and Santos, A.: Letfloating: moving bindings to give faster programs,
Proceedings of the first ACM SIGPLAN international conference on Functional programming, 1996,
pp. 1–12.
[22] Marlow, S.: Haskell 2010 language report, 2010.
[23] Marlow, S. and Jones, S. P.: The Glasgow
Haskell Compiler, Vol. 2, Lulu, January 2012.
[24] Martin, S., Manuel, C., Jones, S. P., and Kevin,
D.: System F with Type Equality Coercions, Proc.
of TLDI ’07, 2007, pp. 53–66.
[25] Nagele, J., Felgenhauer, B., and Middeldorp, A.:
CSI: New Evidence – A Progress Report, Proc. of
CADE’17, LNCS (LNAI) 10395, 2017, pp. 385–397.
[26] Onozawa, K., Kikuchi, K., Aoto, T., andToyama, Y.: ACPH: System Description, 6th Confluence Competition (CoCo 2017), 2017.
[27] Panyala, A., Chavarria-Miranda, D., and Krishnamoorthy, S.: On the use of term rewriting for performance optimization of legacy HPC applications,
Proc. International Conference on Parallel Processing, September 2012, pp. 399–409.
[28] Paterson, R.: A New Notation for Arrows, Proceedings of ICFP’07, 2001, pp. 229–240.
[29] Püschel, M., Moura, J. M. F., et al.: SPIRAL:
Code Generation for DSP Transforms, Proc. IEEE,
Vol. 93, No. 2(2005), pp. 232–275.
[30] Steuwer, M., Fensch, C., Lindley, S., andDubach, C.: Generating Performance Portable
Code Using Rewrite Rules: From High-Level Functional Expressions to High-Performance OpenCL
Code, Proc. of ICFP’15, 2015.
[31] Terese: Term Rewriting Systems, Cambridge
Tracts in Theoretical Computer Science, No. 55,
Cambridge University Press, 2003.