| CARVIEW |
Select Language
HTTP/2 200
cross-origin-resource-policy: cross-origin
etag: W/"6786420e64975bac63ebfb8e361bec61eba0b54550d0cc306868525b3c6ee259"
date: Fri, 16 Jan 2026 01:33:37 GMT
content-type: application/atom+xml; charset=UTF-8
server: blogger-renderd
expires: Fri, 16 Jan 2026 01:33:38 GMT
cache-control: public, must-revalidate, proxy-revalidate, max-age=1
x-content-type-options: nosniff
x-xss-protection: 0
last-modified: Fri, 13 Sep 2024 02:11:25 GMT
content-encoding: gzip
content-length: 45849
x-frame-options: SAMEORIGIN
alt-svc: h3=":443"; ma=2592000,h3-29=":443"; ma=2592000
tag:blogger.com,1999:blog-4642782805835050446 2024-09-12T19:11:25.494-07:00 Martin Sulzmann's Blog Unknown noreply@blogger.com Blogger 25 1 25 tag:blogger.com,1999:blog-4642782805835050446.post-1370158167031009327 2013-01-27T11:32:00.000-08:00 2013-01-27T11:32:39.153-08:00 Non-injective type functions and ambiguous types <br />
<br />
<br />
> {-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, TypeFamilies #-}<br />
<br />
Type inference for standard Hindley/Milner boils down to<br />
solving simple unification (Herbrand) constraints.<br />
Extensions such as type annotations and type functions require<br />
more complex constraints. For users of such extensions, it becomes harder<br />
to understand the reason why type inference (i.e. the underlying constraint solver)<br />
has failed.<br />
<br />
A re-occuring problem of type inference failure seems due to<br />
*non-injectivity* of type functions. GHC 7.4.1 provides some improved<br />
error message for such situations (some examples will shortly).<br />
I argue that the underlying reason for type inference failure<br />
in this context is that the program's type is *ambiguous*. <br />
In case of ambiguous types, type inference, to be successful, is required to guess<br />
types (i.e. the underlying constraint solver is required to guess<br />
solutions). But type inferencer generally don't guess and therefore fail.<br />
<br />
Hence, instead of non-injectivity, ambiguity should be blamed for failure<br />
(where of course non-injectivity is a possible reason for ambiguity).<br />
<br />
Interestingly, recasting the type function program in terms of<br />
functional dependencies yields the desired reason for<br />
failure (i.e. the program's type is detected as ambiguous).<br />
<br />
I yet have to check what's the status of the ambiguity check<br />
in more recent versions of GHC such as GHC 7.6.<br />
<br />
== Type functions are not injective<br />
<br />
OK, so let's start with some basic definitions<br />
<br />
A function F is injective iff<br />
from F a ~ F b we conclude that a ~ b.<br />
<br />
In general, type functions are not necessarily injective<br />
e.g. we could define<br />
type instance F Int = Bool<br />
type instance F Char = Bool<br />
<br />
== Type inference failure due to non-injective type functions?<br />
<br />
Consider the following simple example.<br />
<br />
> type family F a<br />
> f1 :: F a<br />
> f1 = undefined<br />
<br />
The above program is type correct.<br />
The type inference problem boils down to the<br />
following constraint problem<br />
<br />
(1) forall a. exists t. F a ~ t<br />
<br />
The unification type variable 't' arises from the program text (undefined).<br />
The 'exists' quantifier indicates we can apply unification.<br />
The type annoation demands 'F a' for any type 'a'.<br />
Therefore, there's an outermost forall quantifier.<br />
<br />
It's easy to see that the above constraint problem is satisfiable,<br />
e.g. take t = F a.<br />
<br />
[Note: t = F a is not necessarily the only solution, we will come<br />
back to this issue shortly]<br />
<br />
Here's a slightly more complicated variant of f1.<br />
<br />
> type family G a<br />
> {-<br />
> f2 :: G b<br />
> f2 = f2<br />
> -}<br />
<br />
The above is rejected by GHC.<br />
" Couldn't match type `G b' with `G a0'<br />
NB: `G' is a type function, and may not be injective<br />
...<br />
"<br />
<br />
Let's examine in more detail what's happening here.<br />
The type inference problem boils down here to<br />
the constraint problem<br />
<br />
(2) forall b. exists b. G b ~ G a<br />
<br />
The 'G a' bit arises from the program text and<br />
'G b' is the type demanded by the type annotation.<br />
<br />
It's quite easy to see that the constraint problem (2)<br />
is satisfiable, e.g. take a = b. But GHC's type inferencer<br />
is not capable of making such a guess and therefore<br />
GHC rejects the program f2.<br />
<br />
The slightly odd thing is that in case of constraint problem (1),<br />
GHC chooses the obvious guess t = G a.<br />
Depending on G's instances, further solutions are possible.<br />
<br />
For example, for<br />
<br />
> type instance G a = Int<br />
<br />
t = Int would be another guess/solution.<br />
<br />
== Ambiguous types<br />
<br />
I argue that the actual reason for type inference failure is<br />
that the type of f1 and f2 is ambiguous.<br />
Let's slightly recast the type of f2 as follows:<br />
<br />
> {-<br />
> f3 :: (G b ~ c) => c<br />
> f3 = f3<br />
> -}<br />
<br />
I have simply substituted 'G b' by the fresh type variable 'c'.<br />
Here, the unambiguity check demands that fixing<br />
the variable 'c' also fixes the variable 'b' in the context (G b ~ c)<br />
As we know, this is not necessarily the case because<br />
of non-injectivity of type function G.<br />
<br />
== The case of functional dependencies<br />
<br />
For fun, let's recast the above programs with functional dependencies.<br />
<br />
> class FD a b | a -> b<br />
<br />
> fd1 :: FD a b => b<br />
> fd1 = undefined<br />
<br />
The above program is accepted by GHC 7.4.1. It's not hard to see<br />
that fd1's type is ambiguous (so here GHC took a guess).<br />
<br />
The next program is rejected.<br />
<br />
> {-<br />
> fd2 :: FD a b => b<br />
> fd2 = fd2<br />
> -}<br />
<br />
GHC says<br />
"<br />
Ambiguous type variable `a0' in the constraint:<br />
(FD a0 b) arising from a use of `fd2'<br />
Probable fix: add a type signature that fixes these type variable(s)<br />
"<br />
<br />
== Type inference in the presence of ambiguous types<br />
<br />
Suppose we need this program (and switch on a hypothetical flag -XNoUnambiguityCheck).<br />
How can we convice the type inferencer to accept this program?<br />
We need some sort of type-level lambda annotation to fix the 'a' in 'FD a b => b'.<br />
We can mimic such a construct by<br />
(a) turning 'a' into an extra function argument and<br />
(b) lexically scoped type annotations.<br />
<br />
<br />
> fd3 :: (FD a b ) => a -> b<br />
> fd3 = undefined<br />
<br />
> fd4 :: forall a b. (FD a b) => b<br />
> fd4 = fd3 (undefined :: a)<br />
<br />
<br />
== Conclusion<br />
<br />
Someone might say. I never write such contrived ambiguous type annotations.<br />
Well, I argue that such types can arise quite frequently when doing<br />
some of the now fashionably type-level programming in Haskell.<br />
To be continued.<br />
<div>
<br /></div>
Unknown noreply@blogger.com 1 tag:blogger.com,1999:blog-4642782805835050446.post-3644746624015597604 2012-09-24T03:10:00.001-07:00 2012-09-24T03:10:33.340-07:00 Regular Expression Sub-Matching using Partial Derivatives Here's our <a href="https://www.home.hs-karlsruhe.de/~suma0002/publications/ppdp12-part-deriv-sub-match.pdf">paper</a> and the <a href="https://www.home.hs-karlsruhe.de/~suma0002/talks/ppdp12-part-deriv-sub-match-talk.pdf">talk</a> presented at PPDP'12.
There's quite a bit of recent interest in the use of derivatives for matching and parsing, e.g. see the works by Owens/Reppy/Turon on "Regular-expression derivatives reexamined" and Might/Darais/Spiewak on "Parsing with derivatives: a functional pearl".
Our use of derivatives and partial derivatives for regular expression sub-matching
is inspired by our own prior where we derive up-cast and down-cast coercions out of a proof system describing regular expression containment based on partial derivatives. See our APLAS'04 and ML Workshop'05 papers.
Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-7840893759373180447 2012-07-27T00:57:00.001-07:00 2012-07-27T00:57:13.421-07:00 Model Checking DSL-Generated C Source Code We report on the application of SPIN for
model-checking C source code which is generated out of
a textual domain-specific language (DSL).
We have built a tool which automatically generates the necessary
SPIN wrapper code using (meta-)information available at the DSL level.
The approach is part of a larger tool-chain
for developing mission critical applications.
The main purpose of SPIN is for bug-finding where
error traces resulting from SPIN
can be automatically replayed at the DSL level and
yield concise explanations in terms of a temporal specification DSL.
The tool-chain is applied in some large scale
industrial applications.
<p>
The paper appeared in <a href="https://qav.cs.ox.ac.uk/spin2012/">SPIN'12</a>.
Here are links to the <a href="https://ww2.cs.mu.oz.au/~sulzmann/spin12.pdf">paper</a>, <a href="https://ww2.cs.mu.oz.au/~sulzmann/talks/SPIN2012-talk.pdf">talk</a> and <a href="https://ww2.cs.mu.oz.au/~sulzmann/spin-dsls.html">implementation</a>. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-4284593404217447056 2012-06-08T11:44:00.000-07:00 2012-06-08T11:44:29.807-07:00 Regular Expression Sub-Matching using Partial Derivatives Regular expression sub-matching is the problem of finding for
each sub-part of a regular expression a matching sub-string.
Prior work applies Thompson and Glushkov NFA methods for the construction
of the matching automata. We propose the novel use of derivatives and
partial derivatives for regular expression sub-matching.
Our benchmarking results show that the run-time performance is promising
and that our approach can be applied in practice.
<p>
Here's a link to the <a href="https://ww2.cs.mu.oz.au/~sulzmann/manuscript/reg-exp-partial-derivatives.pdf">paper</a> and the <a href="https://code.google.com/p/xhaskell-library/">implementation</a>.
<p>
This is the substantially revised and almost completely re-written (paper and implementation) version of our earlier <a href="https://sulzmann.blogspot.de/2010/04/regular-expression-matching-using.html">draft</a>. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-2013502095512786647 2012-06-04T01:53:00.000-07:00 2012-06-04T01:53:14.954-07:00 Constructive Finite Trace Analysis with Linear Temporal Logic We consider linear temporal logic (LTL) for run-time testing
over limited time periods. The technical challenge
is to check if the finite trace produced by the system
under test matches the LTL property.
We present a constructive solution to this problem.
Our finite trace LTL matching algorithm
yields a proof explaining why a match exists.
We apply our constructive LTL matching
method to check if LTL properties are sufficiently covered
by traces resulting from tests.
<p>
The paper appeared in <a href=https://lifc.univ-fcomte.fr/tap2012/>TAP'12</a>.
Here's a link to the <a href =https://ww2.cs.mu.oz.au/~sulzmann/publications/tap12-constructive-ltl.pdf>paper</a> and the <a href=https://ww2.cs.mu.oz.au/~sulzmann/talks/tap12-talk.pdf>talk</a>.
<p>
The system has been implemented in Haskell and is applied in some real-world projects. Some of the Haskell source code will be made publicly available (later in the year). Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-3547590080717337871 2011-10-28T11:30:00.000-07:00 2011-10-28T12:34:41.744-07:00 Haskell Actors There's some recent interest about Actor-style concurrency in the Haskell context, e.g. see <br /><UL><br /> <LI> <a href="https://hackage.haskell.org/package/haskell-mpi">haskell-mpi</a> <br /> <LI> <a href="https://hackage.haskell.org/trac/ghc/wiki/ErlangInHaskell">ErlangInHaskell</a><br /></UL><br />My own work in this context, see <a href="https://hackage.haskell.org/package/actor">actor</a>, is orthogonal to the above mentioned works.<br /><br />The main point of <a href="https://hackage.haskell.org/package/actor">actor</a> is the ability to pattern match over multiple events (messages) in the message queue. Here's a simple example. Suppose, you write a market-place actor which receives requests from sellers and buyers. The task is to find matching sellers and buyers. In the <a href="https://hackage.haskell.org/package/actor">actor</a> extension this can be elegantly specified as follows (I'm using some pseudo-syntax here):<br /><br /><pre><br /> receive Seller item & Buyer item --> ...<br /></pre><br /><br />Try to express the same using standard actors where we can pattern match over a single message only. There's more info about actors with multi-headed receive clauses in some earlier <a href="https://sulzmann.blogspot.com/2008/10/actors-with-multi-headed-receive.html">post</a>. Please check out the COORDINATION'08 paper (online) for the details of the matching algorithm which is implemented in <a href="https://hackage.haskell.org/package/actor">actor</a>.<br /><br />I retrospect, I should have named the package 'multi-headed-actor', what a freaky name :)<br /><br />The <a href="https://hackage.haskell.org/package/actor">actor</a> approach is built upon concurrent channels but instead we could rely on distributed channels based on <a href="https://hackage.haskell.org/package/haskell-mpi">haskell-mpi</a> or <a href="https://hackage.haskell.org/trac/ghc/wiki/ErlangInHaskell">ErlangInHaskell</a>.<br /><br />This idea (of receive patterns with multiple heads) has been picked up by others, e.g. see the following works which basically adopt the matching algorithm from <a href="https://hackage.haskell.org/package/actor">actor</a><br /><br /><UL><br /><LI> Hubert Plociniczak and Susan Eisenbach. JErlang: Erlang with Joins<br /><br /><LI> Scala Joins Library:<br />Implementing Joins using Extensible Pattern Matching<br />by Philipp Haller and Tom Van Cutsem<br /><br /></UL> Unknown noreply@blogger.com 2 tag:blogger.com,1999:blog-4642782805835050446.post-2232523516938655431 2010-04-24T12:33:00.000-07:00 2010-04-26T10:13:32.792-07:00 Regular Expression Matching using Partial Derivatives Regular expression matching is a classical and well-studied problem.<br />Prior work applies DFA and Thompson NFA methods for the construction<br />of the matching automata. We propose the novel use of derivatives and<br />partial derivatives for regular expression matching.<br />We show how to obtain algorithms for various<br />matching policies such as POSIX and greedy left-to-right.<br />Our benchmarking results show that the run-time performance is promising<br />and that our approach can be applied in practice.<br /><br />This is a topic, Kenny and I have pursued for quite a while and we have finally<br />managed to write up the ideas.<br />Here's the link to the <a href="https://www.cs.mu.oz.au/~sulzmann/manuscript/reg-exp-partial-derivatives.pdf"> paper</a><br />The implementation is on hackage. See <a href="https://hackage.haskell.org/package/regex-pderiv">regex-pderiv</a><br />[Edit: regex-pderiv replaces xhaskell-library] Unknown noreply@blogger.com 5 tag:blogger.com,1999:blog-4642782805835050446.post-1024263017380350356 2009-11-08T07:06:00.000-08:00 2009-11-08T17:32:08.777-08:00 Tag-free Combinators for Binding-Time Polymorphic Program Generation Peter Thiemann and I have written a <a href="https://www.cs.mu.oz.au/~sulzmann/manuscript/polyspec.pdf">paper</a> on (off-line) partial evaluation for polymorphic languages using GHC's advanced typing features.<br /><br />The source code of the combinators is available <a href="https://proglang.informatik.uni-freiburg.de/projects/polyspec/">here</a>.<br /><br />Here's the abstract:<br><br /><ul><br />Binding-time polymorphism enables a highly flexible binding-time analysis for offline partial evaluation. This work provides the tools to translate this flexibility into efficient program specialization in the context of a polymorphic language.<br /><br />Following the cogen-combinator approach, a set of combinators is defined in Haskell that enables the straightforward transcription of a binding-time polymorphic annotated program into the corresponding program generator. The typing of the combinators mimics the constraints of the binding-time analysis. The resulting program generator is safe, tag-free, and it has no interpretive overhead.<br /></ul> Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-3847814832924127007 2008-12-11T14:52:00.000-08:00 2008-12-11T15:20:05.184-08:00 Equality, containment and intersection among regular expressions via symbolic manipulation Three standard regular expression operations<br /><pre><br />data RE a where<br /> Phi :: RE a -- empty language<br /> Empty :: RE a -- empty word<br /> L :: a -> RE a -- single letter taken from alphabet a<br /> Choice :: RE a -> RE a -> RE a -- r1 + r2<br /> Seq :: RE a -> RE a -> RE a -- (r1,r2)<br /> Star :: RE a -> RE a -- r*<br /> deriving Eq<br /><br />equality :: Eq a => RE a -> RE a -> Bool<br />intersect :: Eq a => RE a -> RE a -> RE a<br />contains :: Eq a => RE a -> RE a -> Bool<br /></pre><br />implemented via symbolic manipulation of regular expressions (no explicit finite automata construction) by adapting <a href="https://www.informatik.uni-trier.de/~ley/db/indices/a-tree/a/Antimirov:Valentin_M=.html">Antimirov's</a> regular expression rewriting algorithm via partial derivatives.<br /><br />The implementation is available via the Haskell platform hackage. Check out the <a href="https://hackage.haskell.org/cgi-bin/hackage-scripts/package/regexpr-symbolic">regexpr-symbolic</a> package.<br /><br />The source code describes some of the technical details. You can also check out an earlier <a href="https://sulzmann.blogspot.com/2008/11/playing-with-regular-expressions.html">post</a> which considers the specific case of intersection. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-5883009405446189818 2008-12-06T09:15:00.000-08:00 2008-12-06T14:21:00.028-08:00 Parallel Join Patterns with Guards and Propagation A paper in the works for quite some time. You can download the latest version <a href="https://www.cs.mu.oz.au/~sulzmann/manuscript/parallel-join-patterns.ps">here</a>.<br /><br />Here's what the abstract says:<br />Join patterns are a powerful concurrency abstraction to coordinate multiple events. We propose an extension with guards and propagation and argue that both features are essential in many programming situations. We develop a parallel execution scheme which we have fully implemented as a library in Haskell. Our results provide new insights how to write parallel programs on multi-core architectures.<br /><br />Interested? You can get the implementation via the Haskell platform hackage. Download the <a href="https://hackage.haskell.org/cgi-bin/hackage-scripts/package/join">join</a> package which in turn relies on the <a href="https://hackage.haskell.org/cgi-bin/hackage-scripts/package/multisetrewrite">multisetrewrite</a> package. The multisetrewrite package provides the basic functionality to execute join patterns (with guards and propagation) in parallel. The join package adds synchronous and asynchronous arguments and join method calls. The user interface is still a bit clumsy to use but this will hopefully be improved over time. Unknown noreply@blogger.com 2 tag:blogger.com,1999:blog-4642782805835050446.post-5983150260928471578 2008-12-05T14:04:00.000-08:00 2008-12-05T14:08:42.591-08:00 Concurrent Goal-Based Execution of Constraint Handling Rules We (my PhD student Edmund and me) have just submitted a paper with this title to Theory and Practice of Logic Programming. The paper complements our PPDP'08 paper on parallel Constraint Handling Rules execution. You can get the paper <a href="https://www.cs.mu.oz.au/~sulzmann/manuscript/concurrent-goal-chr-semantics.ps">here</a>.<br /><br />Here's what the abstract says:<br />We introduce a systematic, concurrent execution scheme for Constraint Handling Rules (CHR) based on a previously proposed goal-based CHR semantics. We establish strong correspondence results to the abstract CHR semantics, thus guaranteeing that any answer in the concurrent, goal-based CHR semantics is reproducible in the abstract CHR semantics. Our work provides the foundation to obtain efficient, parallel CHR execution schemes. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-4426333310163779713 2008-12-04T14:13:00.000-08:00 2008-12-05T21:42:16.786-08:00 STM with control: Communication for retrying transactions While working on the join pattern with guards and propagation implementation, we (my PhD student Edmund and me) came across an interesting problem which points out the current limited control/communication capabilities of retrying STM transactions (in Haskell). More on join patterns later. Here's the gist of the problem and a solution in form of a new Haskell library.<br /><br /><h3> The task </h3><br /><br />We're given a list of switches, they can either be on or off<br /><br /><pre><br />> data Switch = On | Off<br /></pre><br /><br />If all switches are on, we switch them all off and report True If one switch is off, we do nothing and report False.<br /><br />In a sequential setting, this task is straightforward. But what if the switches are shared among concurrent threads performing the above task?<br /><br />In a concurrent setting, the task must be formulated as follows.<br /><br />Atomically (<br />If all switches are on, we switch them all off and report True<br />If one switch is off, we do nothing and report False. )<br /><br />Sounds like an application of STM. Indeed, here's a solution.<br /><br /><pre><br />> verifyAndSwitchOff :: [TVar Switch] -> IO Bool<br />> verifyAndSwitchOff ts = <br />> atomically $ do <br />> bs <- mapM (\s -> do v <- readTVar s<br />> case v of<br />> On -> return True<br />> Off -> return False)<br />> ts<br />><br />> if (and bs)<br />> then do mapM (\s -> do writeTVar s Off) ts<br />> return True<br />> else return False<br /></pre><br /><br /><br />We first check that all switches are on. Only then we switch all of them off. Isolation and atomicity of STM are important here.<br /><br />Isolation guarantees that no intermediate step is visible to any other thread. After checking that all switches are on, we have the guarantee that they are still on, once we switch them off. Atomicity guarantees that all operations are executed all at once or not all which implies that some of the initially read switch values has changed. In this case, we abort the transaction and discard all changes so far and start over again.<br /><br /><br />It's tempting to immediately turn a switch off once we've read that the switch is on. But what if we read that a switch is still on? We need some additionally functionality to explicitly abort the transactions. That's what the retry and orElse combinators are for.<br /><br /><pre><br />> verifyAndSwitchOff2 :: [TVar Switch] -> IO Bool<br />> verifyAndSwitchOff2 ts = <br />> let loop [] = return True<br />> loop (s:xs) = do v <- readTVar s<br />> case v of<br />> On -> do writeTVar s Off<br />> loop xs<br />> Off -> return False<br />> in atomically $<br />> (do b <- loop ts<br />> if b then return True<br />> else retry)<br />><br />> `orElse`<br />><br />> return False <br /></pre><br /><br />The loop reads the status of each switch and turns the switch off if the switch is on. Otherwise, we 'abort' by returning False. For example, in case of the initial list [On, On, Off, On] we reach the third switch and the intermediate result [Off, Off, Off, On]. We can't just naively exit at this stage because the tasks demands that all changes are done atomically, ie to its full extent or not at all.<br /><br />Here comes the rescue. The retry combinator allows the programmer to explicitly abort a transaction. That is, we discard all changes (which is important) here. The orElse combinator allows the programmer to compose two transaction. The second transaction will be executed if the first transaction retries. Exactly what we require.<br /><br /><h3> Making the task more interesting </h3><br /><br />Suppose each switch is attached to an action, sort of a continuation. Let's say an IO action.<br /><br /><pre><br />> type Cnt = IO ()<br /></pre><br /><br />We want to return the continuation of the switch which first 'failed'. Here's the updated task description.<br /><br />Atomically (<br />If all switches are on, we switch them all off and report True<br />Otherwise, return the continuation of the first turned on switch.)<br /><br />The signature of the function we need to implement<br /><br /><pre><br />verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt<br /></pre><br /><br />What are our options how to implement the above?<br /><br />We could adapt our first solution verifyAndSwitchOff. This is pretty straightforward. What about verifyAndSwitchOff2? Previously, we simply return False in the second orElse branch. For the more interesting task, we need to iterate over the list of pairs of switches and continuation and select the continuation of the first switch which is still on. This means that in both case we possibly need to iterate over the list twice. This is inefficient and leads to clumsy code.<br /><br />Below we make use of an extension of STM where a retrying transaction can pass some information to the second transaction composed with orElse.<br /><br />The extension is implemented as the STMControl.STMC library. The new primitives are:<br /><br /><pre><br />newTVarC :: b -> STMC a (TVar b)<br />readTVarC :: TVar b -> STMC a b<br />writeTVarC :: TVar b -> b -> STMC a ()<br />atomicallyC :: STMC a b -> IO b<br />retryC :: a -> STMC a b<br />orElseC :: STMC a b -> (a -> STMC a b) -> STMC a b<br /></pre><br /><br /><br />STMC stands for STM with more control. The first parameter refers to the type of the value transmited in case of a retryC. The parameter in the orElseC combinator is now a function which accepts the result transmitted of the retrying transaction.<br /><br />The implementation is fairly simple and uses an (abused) reader monad on top of STM. Here's finally an application of the new functionality.<br /><br /><pre><br />> verifyAndSwitchOffCnt :: [(TVar Switch, Cnt)] -> IO Cnt<br />> verifyAndSwitchOffCnt tcs =<br />> let loop [] = return Nothing<br />> loop ((s,c):xs) = do v <- readTVarC s<br />> case v of<br />> On -> do writeTVarC s Off<br />> loop xs<br />> Off -> return (Just c)<br />> in atomicallyC $<br />> (do r <- loop tcs<br />> case r of<br />> Nothing -> return (return ()) -- default (donothing) continuation<br />> Just c -> retryC c)<br />><br />> `orElseC`<br />><br />> (\c -> return c)<br /></pre><br /><br />The loop checks and resets all switches. In case a switch is turned off we return the attached continuation. We use the Maybe type to indicate failure (Just c) or success (Nothing). In case of success, we return the donothing continuation. Otherwise, we retryC to discard all changes made so far and pass the continuation to the second transaction which then returns this continuation.<br /><br />I'd say compared to the other options, the STMC solution looks pretty clean and easy to understand.<br /><br /><h3> Making the task even more interesting </h3><br /><br />That's the final extension, I promise. Suppose that to each switch there's also an attached STM Bool transaction. In addition to testing that the switch is off, we also test that the STM Bool transaction evaluates to True. Otherwise, we discard our changes and return the attached continuation.<br /><br /><pre><br />> verifyAndSwitchOffCnt2 :: [(TVar Switch, STM Bool, Cnt)] -> IO Cnt<br />> verifyAndSwitchOffCnt2 tcs =<br />> let loop [] = return Nothing<br />> loop ((s,stm,c):xs) = <br />> do v <- readTVarC s<br />> case v of<br />> On -> do writeTVarC s Off<br />> b <- lift $ stm<br /><br /> STMC are (reader monad) lifted STM operations<br /><br />> if b then loop xs<br />> else return (Just c)<br />> Off -> return (Just c)<br />> in atomicallyC $<br />> (do r <- loop tcs<br />> case r of<br />> Nothing -> return (return ()) -- default (donothing) continuation<br />> Just c -> retryC c)<br />><br />> `orElseC`<br />><br />> (\c -> return c)<br /></pre><br /><br />The required changes to our previous solution are minor. In fact, I can't see how to implement the even more interesting task with STM alone. I believe that this task strictly requires STMC or something similar.<br /><br /><br />The complete source code of this example is available as part of the <a href="https://hackage.haskell.org/cgi-bin/hackage-scripts/package/stmcontrol">stmcontrol</a> package on the Haskell platform hackage.<br /><br /><h3> Implementation details </h3><br /><br /><pre><br />type STMC a b = ReaderT (IORef a) STM b<br /><br />retryC :: a -> STMC a b<br />retryC x = do msgChan <- ask<br /> lift $ unsafeIOToSTM (writeIORef msgChan x) -- L1<br /> lift $ retry <br /></pre><br /><br />What if the transaction is aborted just after execution of L1? Is our use of unsafeIOToSTM (un)safe? It's safe. It's okay to discard the IO action in case the transaction is rolled back. The important point is that if the transaction is explicitly retried, the IO action has been executed (which is the case as far as I understand the interplay of STM and unsafeIOToSTM). Unknown noreply@blogger.com 4 tag:blogger.com,1999:blog-4642782805835050446.post-4461880410619449628 2008-12-01T10:00:00.000-08:00 2008-12-01T10:04:47.582-08:00 XHaskell My PhD student Kenny has just submitted his thesis on XHaskell - Adding Regular Expression Type to Haskell.<br /><br />You can download the latest XHaskell implementation and Kenny's thesis draft <a href="https://www.comp.nus.edu.sg/~luzm">here</a> Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-2624575471634355155 2008-11-29T12:42:00.000-08:00 2008-11-29T13:08:05.836-08:00 Transactions in Constraint Handling Rules A <a href="https://www.cs.mu.oz.au/~sulzmann/publications/chr-transactions.pdf">paper</a> to be presented at <a href="https://iclp08.dimi.uniud.it/">ICLP'08</a>, Udine, Italy, December'08. My co-author Tom Schrijvers will give the presentation but here's already a draft of the <a href="https://www.cs.mu.oz.au/~sulzmann/talks/iclp08-chr-transactions.pdf"> talk</a>.<br /><br />If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.<br /><br />In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-3353150121192615737 2008-11-18T13:11:00.000-08:00 2008-11-19T10:53:21.121-08:00 High-level Software Transaction Protocols The topic is how to built high-level (composable) software transaction protocols on top of highly-concurrent, low-level data structures which are not composable. Yes, this is sort of a continuation of my previous 'Transactional Boosting' post. What I'm looking for is a systematic method to built boosted protocols. I believe that a promising formalism are join patterns (aka multi-set rewrite rules).<br /><br /><br /><h3> Transactional boosting revisited </h3><br /><br />Here's my attempt to recast the transactional boosting approach in terms of the join pattern language extension I'm currently working on. Join patterns can now have guards and propagation. For example, the following join patterns says<br /><pre><br />foo(x,y) \ bar(y,z) when x > z = ...<br /></pre><br />if we find method calls foo(x,y) and bar(y,z) where the condition x > z holds (notice the implicit constraint imposed via the shared variable z), then we remove (simplify) bar(y,z) from the method store but we keep (propagate) foo(x,y).<br /><br />Okay, so let's make use of such join patterns to specify the boosted transactional protocol. For simplicity, let's consider a very simple to be boosted object. A set with one 'add' operation.<br /><br /><br />The interface:<br /><pre><br />add x = do t <- readEnv<br /> r <- newSync<br /> addI(t,x,r)<br /> v <- readSync r<br /> <br /></pre><br />From the environment, we get the current transaction identifier (kind of ThreadId). We create a synchronization variable on which we will block. But first we call the method<br />addI(t,x,r) whose interaction with other method calls is specified below<br />(In a Join setting, method calls are recorded in a store).<br /><br /><br />The protocol to check for conflicts:<br /><pre><br />-- conflict --> suspend<br />addI(t1,x,_) \ addI(t2,x,r) = addS(t2,x,r)<br /><br />-- commute<br />addI(t1,x,_) \ addI(t2,y,r) when x \= y = do primAdd y<br /> register t2 'remove y'<br /> r:= ()<br /> addToStore 'addI(t,x,r)'<br /><br />-- first call<br />addI(t,x,r) = do primAdd x<br /> register t 'remove x'<br /> r:= ()<br /> addToStore 'addI(t,x,r)'<br /><br /></pre><br />The first join pattern checks for non-commuting method calls (subtle point: we assume that the propagated head will NOT be executed as a goal). Join patterns are tried from top to bottom (in our implementation). Hence, if the first join pattern can't fire we try the second one which applies if all calls to add commute and there exist at least two add calls (we assume multi-set semantics, one call can't match two occurrences). In the 'commute' case, we call the primitive add (relying on the highly-concurrent, low-level data structure) and unblock the original add call. Registering of the inverse operation is necessary in case we abort the transaction. The last join pattern applies if we're the first to call add. Adding add calls to the store guarantees that <br />all calls are made visible to each other.<br /><br />A transaction can only commit (reach the end) if it doesn't encounter conflicts. Otherwise, the transaction will be suspended.<br /><br />The commit protocol has two stages. We first unblock one suspended add call (if exists). Otherwise, we do nothing. The assumption is that the committing transaction calls 'commit(t)'.<br /><pre><br />commit(t), addI(t,x,_), addS(t2,x,r) = addI(t2,x,r)<br />commit(t) = return ()<br /></pre><br /><br />Actually, we could be more optimistic and unblock all commuting add calls. I can't see how to nicely formulate this with join pattern alone (we'd need to traverse all suspended calls and select all commuting ones).<br /><br />We yet to release all 'locks' (the stored add calls) held by transaction t. Once more, we call 'commit(t)'.<br /><pre><br />commit(t) \ addI(t,x,_) = return ()<br />commit(t) = return ()<br /></pre><br />The propagated goal 'commit(t)' guarantees that we exhaustively release all locks (a for loop join pattern style). <br /><br />In the last commit step, we erase all registered inverse operations.<br /><br />As said above, in the current formulation, a transaction can only reach the end (and thus commit) if it doesn't encounter conflicts. The transaction won't fail or retry. It can only happen that the transaction is suspended, possibly indefinitely.<br /><br />To avoid 'cyclic suspension' deadlocks, the 'transactional boosting' approach uses a time-out to actually fail a transaction. In case of failure, we need to remove the transaction's method calls<br /><pre><br />fail(t) \ addI(t,_,_) = return ()<br />fail(t) \ addS(t,_,_) = return ()<br />fail(t) = return ()<br /></pre><br />and we execute the registered inverse operations. Then, the transaction is started from scratch.<br /><br /><h3> Where to go next </h3><br /><br />The above description is not necessarily meant to be used in an efficient implementation. However, I believe that the use of join patterns allows us to to give a nice declarative specification of 'transactional boosting' and its underlying protocols. I will be interesting to consider alternative 'boosting' protocols. It appears that in general the 'boosting' approach can only support pessimistic concurrency. Optimistic concurrency requires that a transaction only commits its updates only after no conflicts have been detected. <br /><br />In my experience, transactional boosting and optimistic concurrency only works out for some specific cases, eg the multi-set rewrite stuff I mentioned in my earlier 'Transactional Boosting' post.<br /><br />Anyway, there's still lots to discover. Guess that's something for a future post. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-7410003183833996849 2008-11-16T03:45:00.000-08:00 2008-11-16T13:17:43.890-08:00 Transactional boosting This post is about software transactional memory (STM) and how to retain its benefits (composability) while trying to minimize its drawbacks (poor performance due to false conflicts).<br /><br /><h3> Software transactional memory: Composability and false conflicts </h3><br /><br />Software transactional memory (STM) is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing (wikipedia). Below is a simple example of a concurrent, unordered singly-linked list using STM as supported by GHC Haskell.<br /><br /><pre><br />date List a = Node {val :: a, next :: TVar a}<br /> | Nil<br /><br />insert :: TVar a -> a -> STM ()<br />find :: TVar a -> a -> STM Bool<br />-- True = present, False = absent<br />delete :: TVar a -> a -> STM Bool<br />-- True = present and deleted, False = absent<br /><br />-- atomically delete 3 and 4 if present<br />transaction :: TVar a -> IO Bool <br />transaction root = atomically $ do<br /> b1 <- find root 3<br /> b2 <- find root 4<br /> if b1 && b2 then do<br /> delete root 3<br /> delete root 4<br /> else return False<br /></pre><br /><br />The straightforward definitions of the linked list operations are left out. They are all executed within the STM monad which will guarantee that the operation is executed atomically, i.e. to its full extent or not at all which means in the programm language setting that we re-run (aka rollback/retry) the operation.<br /><br />In Haskell, we can easily build 'bigger' STM operations by gluing together 'smaller' STM operations. For example, the transaction checks if elements 3 and 4 are present in the list and then will delete both elements. The entire transaction is executed atomically which guarantees that in case we return True, elements 3 and 4 were present but have now been deleted. Neat!<br /><br />The benefits of STM over say locks are well documented. However, STM has (often) a significant performance disadvantage. Our (naive) STM implementation will protect the entire list. Suppose that elements 3 and 4 are stored towards the tail of the list. Hence, we (almost) need to traverse the entire list which then potentially leads to false conflicts with other concurrent STM operations. The effect is that many concurrent STM operations will be serialized (i.e.~sequential instead of parallel execution).<br /><br /><h3> Comparing concurrent linked-list implementations in Haskell </h3><br /><br />I recently wrote a paper with the above title to be presented at DAMP'09, in collaboration with Simon Marlow and Edmund Lam. Our results show that the naive STM implementation is no match against more fine-tuned implementations which<br /><br /><ul><br /> <li> either side-step the STM protocol (only each node operation is performed within the STM)<br /> <li> employ lock-coupling via Haskell's MVars, or<br /> <li> rely on atomic compare-and-swap.<br /></ul><br />Please check the paper for the details.<br /><br />The (well-known) downside of this more efficient singly-linked operations (efficient in the sense they enjoy a higher degree of concurrency) is that they are not composable anymore. That is, it is non-trivial to implement the above transaction (atomically find and delete 3 and 4) using the more efficient implementations.<br /><br /><h3> Transactional boosting </h3><br /><br />Maurice Herlihy and Eric Koskinen wrote two recent papers on a topic they refer to as transactional boosting: How to recover the 'high-level' benefits of STM while relying on 'low-level', highly concurrent data-structures.<br />The papers are (see Eric's website):<br /><ul><br /> <li> Transactional Boosting: A Methodology for Highly-Concurrent Transactional Objects<br /> M. Herlihy, E. Koskinen. PPoPP 2008<br /> <li> Aggressive Transactional Boosting<br /> E. Koskinen, M. Herlihy.<br /> Under submission. August 2008. <br /></ul><br /><br />My understanding of how the transactional boosting approach meant to work is that<br /><br /><ul><br /> <li> the user needs to verify if primitive operations 'commute', otherwise<br /> <li> the operands of (non-commuting) operations will be protected by an abstract lock,<br /> <li> each operations requires an inverse which will be executed if the transaction fails to commit.<br /></ul><br /><br />It seems that the transactional boosting approach assumes pessimistic concurrency. I'm still not clear about the exact details of the approach but it looks definitely very promising. <br /><br />Incidentally, I ran across the issue of transactional boosting in my own work on concurrent execution of multi-set rewrite rules.<br /><br /><h3> Multi-set rewriting and transactional boosting </h3><br /><br />Below are simple examples of (monomorphic for simplicity) multi-set rewrite rules.<br />Right-hand sides are omitted because they don't matter here.<br /><pre><br /> A, B <==> ...<br /> A, C <==> ...<br /></pre><br /><br />Multi-set rewrite rules operate on a store, a multi-set of elements. We can concurrently apply multi-set rewrite rules if they operate on non-conflict parts of the store. Suppose, we have the store <br /><pre><br />{A, A, B, C}<br /></pre><br />Then, the first rule can be applied on (the first) A and B and the second rule can be<br />applied on (the second A) and C. There's no conflict. Hence, both rules can be applied concurrently.<br /><br />The point is that the store is implemented as a concurrent data-structure and execution of a rewrite rule can be viewed as an STM transaction. For example, the operational interpretation of the first rule is<br /><pre><br /> atomically $ do <br /> find A<br /> find B<br /> if both present <br /> then do delete A<br /> delete B<br /> else return ()<br /></pre><br /><br />The first implementation of concurrent multi-set rewrite rules, in collaboration with Edmund Lam (my PhD student btw), presented here<br /><pre><br />Edmund S. L. Lam, Martin Sulzmann: <br />A concurrent constraint handling rules implementation <br />in Haskell with software transactional memory. DAMP 2007:<br /></pre><br />used a (naive) STM list to implement the store. Our experiments confirm that such an approach won't scale. Due to a high(ly likely) number of false conflicts, multi-set rewrite rules are executed sequentially, though, we ought to execute them in parallel.<br /><br />Our latest implementation, presented here<br /><pre><br />Martin Sulzmann, Edmund S. L. Lam: <br />Parallel execution of multi-set constraint rewrite<br />rules. PPDP 2008<br /></pre><br />uses a more low-level, 'more concurrent' data-structure which is *not* composable. Hence, we had to implement our own STM protocol on top of the low-level data-structure (The PPDP paper is a bit unclear about this but we'll present what we've achieved in its full glory in a forth-coming journal submission soon).<br /><br /><h3> Summary </h3><br /><br />STM is great but it often has poor performance. There are many applications where we wish to have a 'transactional boosting' approach. As far as I can tell, the approach laid out by Maurice Herlihy and Eric Koskinen is fairly different from the approach we used for concurrent execution of multi-set rewrite rules. Possibly, there's some unifying theory but I have the feeling that transactional boosting relies on some domain-specific assumption. Anyway, interesting times with many interesting topics. I'm sure there' more to say about transactional boosting. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-414956313140446703 2008-11-12T11:40:00.000-08:00 2008-11-12T12:26:10.047-08:00 Actor versus Join Concurrency This post tries to shed some light on the differences and commonalities between actor and join style concurrency and explains its connection to multi-set rewrite rules.<br /><br />Recently, I've published two libraries supporting<br /><br /><ul><br /> <li> Actor concurrency, see <a href="https://sulzmann.blogspot.com/2008/10/actors-with-multi-headed-receive.html">here</a>, and<br /> <li> Join concurrency, see <a href="https://sulzmann.blogspot.com/2008/10/multi-set-rewrite-rules-with-guards-and.html">here</a><br /></ul><br /><br /><h4> Coordination via multi-set rewrite rules with guards </h4><br /><br />Both libraries support similar forms of coordination primitives in terms of multi-set rewrite rules with guards. For example, consider<br /><pre><br />Seller x, Buyer x --> "do something"<br /></pre><br />which says that if there's a seller and a buyer where both agree on the object x to be sold, then we execute the right-hand side "do something". <br /><br />What's the connection to rewrite rules? Well, in case there's "Seller Obj" and "Buyer Obj", both will be rewritten to "do something". It's natural to view sellers and buyers as resources. To rewrite multiple resources, we simply use multi-set rewrite rules. For example,<br /><pre><br />A, A --> "blah"<br /></pre><br />will remove two occurences of "A" by "blah".<br /><br />Lesson learned so far. The basic coordination primitives behind actor and join style concurrency are expressed in terms of multi-set rewrite rules. In the join setting, these multi-set rewrite rules are commonly referred to as join-patterns. However, please take note that Erlang-style actors only support single-headed rewrite rules and join-style concurrency as found in JoCaml, Polyphonic C or Claudio Russo's Joins librariy does not support guards (both features are supported by the above mentioned libaries).<br /><br />Assuming we agree on a common set of multi-set rewrite rules (possibly with guards), what's the difference then between actor and join concurrency?<br /><br /><h4> Actor concurrency </h4><br /><br />In the actor setting, we commonly assume that multi-set rewrite are applied sequentially. In the special case of Erlang's single-headed rewrite rules, we start scanning the mailbox (that's the place where sellers, buyers etc are stored) from left to right. For each mailbox element (often referred to as message aka method or even constraint in the rewrite setting), we then try the single-headed rewrite rules from top to bottom, until a match is found. In the general case of multi-set (headed) rewrite rules, we can assume that things can get a bit more tricky. Check out the paper below for a formal sequential execution semantics<br /><pre><br />Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert, <br />Actors with Multi-headed Message Receive Patterns. <br />COORDINATION 2008<br /></pre><br />But if rewrite rules are executed sequentially where does concurrency come in? Well, we can have concurrent actors which communicate by sending each other messages (aka methods or constraints). The messages itself are processed and executed sequentially by each actor. You may therefore argue that the behavior of each actor is completely deterministic.<br /><br /><h4> Join concurrency </h4><br /><br />In the join setting, the place where methods (aka messages or constraints) are kept is commonly referred to as a "store". Any multi-set rewrite rule can fire as soon as we find a match for its left-hand side among the st of stored methods. The only condition is that if two rewrite rules fire concurrently, they must operate on non-overlapping parts. <br /><br /><h4> Summary </h4><br /><br />Both styles of concurrency use the same coordination primitive, i.e. multi-set rewrite rules. I'd argue that actor and join concurrency serve different purposes (hence, are equally useful). One can emulate the other but I prefer to have efficient support for both of them (not via emulation).<br /><br />NOTE: I wrote this post are seeing these comments on reddit.com:<br /><ul> <br /> <li> <a href="https://www.reddit.com/r/programming/comments/7a3he/actor_model_concurrency_for_haskell/">Actor model concurrency for Haskell</a><br /> <li> <a href="https://www.reddit.com/r/haskell/comments/79xfm/multiset_rewrite_rules_with_guards_and_a_parallel/">Multi-set rewrite rules with guards and a parallel execution scheme</a><br /></ul><br />So, having a blog is possibly useful after all :) Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-8527480946999078870 2008-11-12T02:15:00.000-08:00 2008-11-17T04:40:34.311-08:00 The BaggerProblem <h3> Description </h3><br /><br /> There are n number of bags which can be filled up with either large, medium or small items. The weight of items of a specific kind is fixed. The maximum weight carried by a bag is fixed.<br /><br />Bags are filled up with items in a fixed order:<br /><ul><br /> <li> 1. In sequential order from lowest to highest bag number<br /> <li> 2. Exhaustively fill up the bag first with<br /> <ul><br /> <li> (a) large items, then<br /> <li> (b) medium items, then<br /> <li> (c) small items.<br /> </ul><br /></ul><br /> <br /> The straightforward solution is to<br /><ul><br /> <li> 1. Fill up bags with large items, then<br /> <li> 2. with medium items, and then finally with<br /> <li> 3. small items.<br /></ul><br /><br /> However, once a bag has been exhaustively filled up with large items (we either stop because the bag reached its maximum capacity of large items, or we're simply running out of large items), we can start filling up this bag with medium items. The point is that we don't have to wait until all bags are exhaustively filled up with large items.<br /> <br /> This form of concurrency has clear connection to instruction pipelining. What we want to show here is how to come up with a concurrent solution to the bagger problem<br /><br />We'll give two solutions:<br /><br /> <ul> <br /> <li> a solution using join-patterns extended with guards,<br /> <li> from which we can easily derive a more 'elementary' solution using standard synchronization primitives such as Software Transactional Memory (STM).<br /> </ul><br /><br /><h3> Solution using Join extended with guards </h3><br /><br />The join-calculus (and languages implementing join-patterns) doesn't support guards. Hence, we make use of our join extension which supports guards. The guards we use here are in fact implicit (shared variables). Here we go:<br /><br /><pre><br /> The methods we introduce are:<br /><br /> Bag(kind,no,content) denotes a bag which<br /> <br /> - currently expects to be filled with items of kind 'kind'<br /> - no is the bags number<br /> - content refers to the current content<br /><br /> Initially, all bags are of the form<br /><br /> Bag(Large,i,Empty)<br /><br /><br /> Item(k) denotes an item of kind 'kind'<br /><br /><br /> The above methods are all asynchronous.<br /><br /> We introduce two synchronous methods.<br /><br /> Iterator(kind,no) fills up bag number no with items of kind 'kind'.<br /> Initially, there are three 'iterators':<br /><br /> - Iterator(Large,1)<br /> - Iterator(Medium,1)<br /> - Iterator(Small,1)<br /><br /> Each will run in its own thread. Each starts in 'Large' mode.<br /> That is, only the large iterator can fill up the bags (sequentially).<br /> Once the large iterator is done with bag number i, the bag is<br /> 'unlocked' by moving from 'Large' to 'Medium' mode and so on.<br /><br /> GetItem(kind,r) looks for an item of kind 'kind', the outcome<br /> is reported in r of type Maybe Weight.<br /><br /> Here are the join patterns and their bodies.<br /> (We assume that join patterns are executed from top to bottom,<br /> for convenience only)<br /><br /> Bag(kind,no,content) & Iterator(kind,no) = <br /> if (weight content) + (weight kind) >= maxBagWeight<br /> then do bag (next kind) no content<br /> if no < MaxBagNo<br /> then iterator kind (no+1)<br /> else return ()<br /> else do<br /> r <- getItem k<br /> case r of<br /> Nothing -> do<br /> bag (next kind) no content<br /> if no < MaxBagNo -- (***)<br /> then iterator kind (no+1)<br /> else return ()<br /> Just itemWeight -> do<br /> bag kind no (add content itemWeight)<br /> iterator kind no <br /> <br /><br /> Item(k) & GetItem(k,x) = case k of<br /> Large -> x := Just Large<br /> ...<br /><br /> GetItem(k,x) = x:= Nothing<br /><br /><br /> NOTE:<br /><br /> First, I thought we could replace (***) by the 'default' rule<br /><br /> Iterator(kind, no) = return ()<br /><br /> which we put *after* the first rule.<br /><br /> However, this won't work because the 'small' iterator waiting for<br /> the medium and large iterator may terminate prematurely.<br /><br /></pre><br /><br />A concrete implementation of the above can be found<br /><a href="https://sulzmann.blogspot.com/2008/10/multi-set-rewrite-rules-with-guards-and.html"> here </a> as part of the multisetrewrite library.<br /><br /><h3> Elementary solution in Haskell using STM </h3><br /><br /><br /><pre><br />> import IO<br />> import Data.IORef<br />> import Control.Concurrent<br />> import Control.Concurrent.STM<br />> import Control.Concurrent.Chan<br /><br /><br />We set up the item space by storing large, medium and small<br />items into their respective list. For each kind of items,<br />there's at most one thread trying to access the items.<br />Hence, using IORefs is fine.<br /><br />> data ItemSpace = IS { large :: IORef [()]<br />> , medium :: IORef [()]<br />> , small :: IORef [()] }<br /><br />We only store () values, the weights are fixed.<br /><br />> largeWeight = 6<br />> mediumWeight = 4<br />> smallWeight = 2<br /><br /><br />The kind of items we support are either large, medium or small.<br />Done is a "dummy" item. We'll move from large to medium to small items.<br />Done simply indicates that we are done.<br /><br />> data Item = Large | Medium | Small | Done deriving (Eq, Show)<br /><br /><br />> next :: Item -> Item<br />> next Large = Medium<br />> next Medium = Small<br />> next Small = Done<br /><br />> itemWeight :: Item -> Int<br />> itemWeight Large = largeWeight<br />> itemWeight Medium = mediumWeight<br />> itemWeight Small = smallWeight<br /><br /><br />The procedure to fetch items. There may be concurrent threads<br />accessing either large, medium or small items. But there's<br />at most one thread for each kind.<br /><br />> fetch :: ItemSpace -> Item -> IO (Maybe ())<br />> fetch is kind = <br />> let get m = do <br />> l <- readIORef m<br />> case l of<br />> (x:xs) -> do writeIORef m xs<br />> return (Just x)<br />> [] -> return Nothing<br />> in case kind of<br />> Large -> get (large is)<br />> Medium -> get (medium is)<br />> Small -> get (small is)<br /><br /><br />Each bag records its current weight and content.<br />The mode tells us which kind of items are currently allowed to <br />be put into the bag. The mode is protected by a TVar which allows us<br />to suspend until the large items are exhaustively put into the bag.<br /><br />> data Bag = Bag { mode :: TVar Item<br />> , curWeight :: IORef Int<br />> , content :: IORef [Item] } <br /><br />> printBag :: Bag -> IO ()<br />> printBag bag = do<br />> w <- readIORef (curWeight bag)<br />> c <- readIORef (content bag)<br />> putStrLn $ (show (w,c))<br /><br />The maximum weight held by each bag is fixed.<br /><br />> maxBagWeight = 16<br /><br /><br />We add an item to a bag by incrementing the bags weight<br />plus updating the content.<br /><br />> add :: Bag -> Item -> IO ()<br />> add bag kind = do<br />> w <- readIORef (curWeight bag)<br />> c <- readIORef (content bag)<br />> writeIORef (curWeight bag) (w + itemWeight kind)<br />> writeIORef (content bag) (kind : c)<br /><br /><br />We check if a bag becomes full (over-weight) if we would add<br />another item.<br /><br />> bagIsFull :: Bag -> Item -> IO (Bool)<br />> bagIsFull bag kind = do<br />> w <- readIORef (curWeight bag)<br />> return ((w + itemWeight kind) > maxBagWeight)<br /><br /><br /><br />fillBag fills up (exhaustively) a bag with items of a given kind.<br />We 'unlock' the bag by 'incrementing' the mode if<br /> - the bag is full<br /> - no more items of this kind are left<br /><br /><br />> incrementMode :: Bag -> IO ()<br />> incrementMode bag = <br />> atomically $ do status <- readTVar (mode bag)<br />> writeTVar (mode bag) (next status) <br /><br />> fillBag :: ItemSpace -> Bag -> Item -> IO ()<br />> fillBag is bag Done = error "not happening here"<br />> fillBag is bag kind = <br />> let loop = do<br />> b <- bagIsFull bag kind<br />> if b then incrementMode bag<br />> else do<br />> r <- fetch is kind<br />> case r of<br />> Nothing -> incrementMode bag<br />> Just _ -> do add bag kind<br />> loop<br />> in loop <br /><br /><br />We process (ie fill up) the list of bags sequentially.<br />For each bag we must wait untill its our turn.<br />The priorities are<br /><br /> large > medium > small<br /><br /><br />> waitMode :: Bag -> Item -> IO ()<br />> waitMode bag kind =<br />> atomically $ do status <- readTVar (mode bag)<br />> if status == kind then return ()<br />> else retry<br /><br />> processBags :: ItemSpace -> Item -> [Bag] -> IO ()<br />> processBags is kind bs = <br />> mapM_ (\b -> do waitMode b kind<br />> fillBag is b kind) bs<br /> <br /><br />For each kind we spawn a thread to fill up the list of bags.<br /><br /><br />> start :: ItemSpace -> [Bag] -> IO ()<br />> start is bs = do<br />> cnt <- atomically $ newTVar 0<br />> let spawn = \kind -> forkIO (do processBags is kind bs<br />> atomically $ do v <- readTVar cnt<br />> writeTVar cnt (v+1))<br />> spawn Large<br />> spawn Medium<br />> spawn Small<br />> atomically $ do v <- readTVar cnt<br />> if v == 3 then return ()<br />> else retry<br /><br /><br /><br /><br />testing<br /><br />> createIS ln mn sn = do<br />> l <- newIORef [ () | x <- [1..ln]]<br />> m <- newIORef [ () | x <- [1..mn]]<br />> s <- newIORef [ () | x <- [1..sn]]<br />> return (IS {large = l, medium = m, small = s})<br /><br />> emptyBag = do<br />> m <- atomically $ newTVar Large<br />> w <- newIORef 0<br />> c <- newIORef []<br />> return Bag {mode = m, curWeight = w, content = c}<br /><br />> test largeNo medNo smallNo bagNo = do <br />> is <- createIS largeNo medNo smallNo<br />> bs <- mapM (\_ -> emptyBag) [1..bagNo]<br />> mapM_ (\b -> printBag b) bs<br />> putStrLn "Start"<br />> start is bs <br />> putStrLn "Done"<br />> mapM_ (\b -> printBag b) bs<br /></pre><br /><br /><h3> Some observations </h3><br /><br />The STM solution can be improved. The thread filling up bags with large items doesn't need to check the status of the bag and the thread filling up small items only needs to be waken up once the 'medium' thread is done. We could achieve this behavior by replacing<br /><pre><br />mode :: TVar Item<br /></pre><br />with<br /><pre><br />mode1 :: TVar Item<br />mode2 :: TVar Item<br /></pre><br />That is, the 'medium' thread retries on mode1 and the 'small' thread retries on mode2. <br /><br />In the join solution none of these optimizations are necessary, they are dealt with implicitly. For example, if Iterator(Small,someNo) is unable to fire a join-pattern, this method will be suspended (i.e. the method is put into the store). If the mode of a bag finally switches to small, this active bag will then in combination with the inactive (ie suspended) Iterator(Small,someNo) trigger the join-pattern. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-2298172935749855257 2008-11-06T14:03:00.000-08:00 2008-11-06T14:21:37.863-08:00 Gossiping girls In my class on UPPAAL (a modeling and analysis tool for communicating FAs aka CFAs), I gave the following (classic) exercise:<br /><br />A number of girls initially know one distinct secret each. Each girl has access to a phone which can be used to call another girl to share their secrets. Each time two girls talk to each other they always exchange all secrets with each other (thus after the phone call they both know all secrets they knew together before the phone call). The girls can communicate only in pairs (no conference calls) but it is possible that different pairs of girls talk concurrently.<br /><br />Sounds like fun, right? Before, I discuss a sample solution in UPPAAL, let's consider some alternative frameworks which we could use to code up the above problem.<br /><br />Here's a solution using CHR (Constraint Handling Rules):<br /><pre><br /> Girl(name1,secrets1), Girl(name2,secrets2) <==> <br /> newSecrets(secrets1,secrets1) | let s=shareSecrets(secrets1,secrets2)<br /> in Girl(name1,s)<br /> Girl(name2,s)<br /></pre><br /><br />What about using Join-patterns extended with guards and synchronous method calls:<br /><pre><br /> Girl(name1,secrets1) & Girl(name,secrets2) = do <br /> secrets1 := secrets1 `union` secrets2<br /> secrets2 := secrets2 `union` secrets2<br /></pre><br /><br />Okay, so finally my UPPAAL solution. First, the declarations plus description. The actual CFA is displayed below.<br /><br /><br /><pre><br />// =========================<br />// == Global declarations ==<br /><br />// We introduce two channels. First, I thought we can do with just<br />// one channel but then I believe things will get really messy.<br /><br />chan call, call2;<br /><br />// We assume that there are three secrets: one, two and three<br /><br />// To pass secrets among girls we introduce three (global) variables, <br />// one for each secret.<br />// The value 0 indicates that the secret is not present (ie known).<br />// The value 1 indicates that the secret is known.<br /><br />int var_s1, var_s2, var_s3;<br /><br />// The actual transmission of values is performed in two steps:<br />// 1. First the caller tranfers her secrets<br />// 2. Then, it's the callee's turn to transfer her secrets.<br />// We must guarantee that this step happens atomically between<br />// two parties. We can either (a) use the UPPAAL feature of<br />// committed locations or (b) we simply transmit the callers identity <br />// which then the callee transmits back for verification. <br />// Option (a) sounds too easy, almost cheating :),<br />// so we'll pursue option (b). <br /><br />// To transmit the callers identity, we'll need another "message-passing" variable.<br /><br />int var_id;<br /><br />// WARNING: We use here the initial_secret as a unique identifier<br />// which implies that we only supports girls which initially now<br />// a distinct secret.<br /><br />// Please check the declarations of the girl template which<br />// describes the ideas and functionality of the CFA.<br /></pre><br /><br /><br /><pre><br />// =======================================<br />// == Declarations of the girl template ==<br /><br />// Three variables to represent the girl's knowledge/status about<br />// the three secrets.<br /><br />// We will initialize the variables when instantiating<br />// the girl template. The input parameter initial_secret<br />// refers to the secret that's initially known.<br /><br />int s1, s2, s3;<br /><br />// local variables to store the transmitted messages (secrets and caller id)<br /><br />int in1, in2, in3, in_id;<br /><br />// The first step of the girl CFA is to record (locally) the initially known<br />// secret. View as programming if-then-else statements using CFA transitions.<br />// If initial_secret == 1 then s1 = 1, s2 = 0, s3 = 0<br />// else and so on<br /><br />// It gets interesting once we reach the "Start" state.<br />// In the first stage, we can either make a call, via "call!", or receive a call via "call?".<br />// In case we're the caller, we transmit our secrets and our identity (in form of the<br />// initial_secret). In case we're the receiver of the call, we're storing the<br />// transmitted values. Then, in the second stage, the roles switch and the caller <br />// becomes the receive and vice versa. Notice the use of a different channel.<br />// This is to avoid that a caller of the first stage can interact with a receiver<br />// of the second stage. We yet need to check that the caller and receiver of the<br />// first stage are still the same for the second stage. We perform this check<br />// in state "Verify" by comparing the transmited identify with our own (the initial_secret).<br />// A point to note is that this check is only performed by the receiver<br />// of the second stage.<br />// States "Update_Secrets1" and "Update_Secrets2" then update the secrets after the<br />// exchange. The formula (x+y) - (x*y) evaluates to 1 or 0 for values 0 and 1.<br />// Sure, this could be done smarter using bit operations or simply using UPPAAL's<br />// C-style array.<br /></pre><br /><br /><pre><br />// =========================<br />// == System declarations ==<br /><br />girl1 = Girl(1);<br />girl2 = Girl(2);<br />girl3 = Girl(3);<br /><br />// List one or more processes to be composed into a system.<br />system girl1, girl2, girl3;<br /></pre><br /><br />And finally the CFA:<br /><a title="View Girl document on Scribd" href="https://www.scribd.com/doc/7794675/Girl" style="margin: 12px auto 6px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 14px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block; text-decoration: underline;">Girl</a> <object codebase="https://download.macromedia.com/pub/shockwave/cabs/flash/swflash.cab#version=9,0,0,0" id="doc_55627205366861" name="doc_55627205366861" classid="clsid:d27cdb6e-ae6d-11cf-96b8-444553540000" align="middle" height="500" width="100%"> <param name="movie" value="https://documents.scribd.com/ScribdViewer.swf?document_id=7794675&access_key=key-8jf6ejz03qy5zucvups&page=1&version=1&viewMode="> <param name="quality" value="high"> <param name="play" value="true"> <param name="loop" value="true"> <param name="scale" value="showall"> <param name="wmode" value="opaque"> <param name="devicefont" value="false"> <param name="bgcolor" value="#ffffff"> <param name="menu" value="true"> <param name="allowFullScreen" value="true"> <param name="allowScriptAccess" value="always"> <param name="salign" value=""> <embed src="https://documents.scribd.com/ScribdViewer.swf?document_id=7794675&access_key=key-8jf6ejz03qy5zucvups&page=1&version=1&viewMode=" quality="high" pluginspage="https://www.macromedia.com/go/getflashplayer" play="true" loop="true" scale="showall" wmode="opaque" devicefont="false" bgcolor="#ffffff" name="doc_55627205366861_object" menu="true" allowfullscreen="true" allowscriptaccess="always" salign="" type="application/x-shockwave-flash" align="middle" height="500" width="100%"></embed> </object> <div style="margin: 6px auto 3px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 12px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block;"> <a href="https://www.scribd.com/upload" style="text-decoration: underline;">Get your own</a> at Scribd or <a href="https://www.scribd.com/browse" style="text-decoration: underline;">explore</a> others: </div><br /><br />So, which solution do you prefer? To be fair, UPPAAL is not meant for programming, it has its strength in analyzing CFAs via its expressive query language and model checker. Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-8801367595901655407 2008-11-05T12:42:00.000-08:00 2008-11-06T02:59:17.937-08:00 From Join to UPPAAL and back I'm currently teaching a course using UPPAAL for modelling and anlysis of communicating FAs (finite automatas). In this post, I will show some interesting connections between communicating FAs and coordination patters as found in the Join calculus (referred to as Join for brevity).<br /><br />For concreteness, let's consider a (classic) coordination example: The 'bridge' problem. We have four soldiers on the left (unsafe) side of the bridge. They'd like to cross the bridge to get to the right (safe) side. The problem is it's at night and they need a torch to cross the bridge. The torch can carry a maximum of two soliders. We assume that the torch always carries two soliders from right to left and only solider goes back (left to right).<br /><br />In Join, we can specify/model this problem as follows. We introduce synchronous methods 'take', 'release' and 'takeBack' to model the actions. We introduce asynchronous methods 'free', 'one', 'two', 'oneLeft', 'rightSide' and 'oneFrom' to represent the states of the torch and 'unsafe(i)', 'towards(i)', 'safe(i)' and 'back(i)' to represent the states of soldier i. Their meaning will become clear once see the join-patterns describing the interaction between torch and soldiers.<br /><br />The behavior of the torch is specified via the following join-patterns (using Haskell-style syntax).<br /><pre><br />free = do take<br /> one<br /><br />one = do take<br /> two<br /><br />two = do release<br /> oneLeft<br /><br />oneLeft = do release<br /> rightSide<br /><br />rightSide = do takeBack<br /> oneFrom<br /><br />oneFrom = do release<br /> free<br /></pre><br /><br />Of course, we could have unfolded the above definitions into the following (and thus omitting the intermediate states)<br /><br /><pre><br />free = do take<br /> take<br /> release<br /> release<br /> takeBack<br /> release<br /> free<br /></pre><br />This makes it even clearer that the torch waits for two soldiers to grab the torch. Then, the torch (with the soldiers) crosses the bridge (this is implicit). The torch releases both soliders and the torch will take back a soldier and release this soldier on the unsafe side again. The more verbose representation (using the intermediate states) will be useful later when discussing the connection to communicating FAs.<br /><br />We yet need to model the behavior of solider(i). We finally make use of some multi-headed join-patterns.<br /><pre><br />unsafe(i) & take = towards(i)<br /><br />towards(i) & release = safe(i)<br /><br />safe(i) & takeBack = back(i)<br /><br />back(i) & release = unsafe(i)<br /></pre><br /><br />For example, the first join-pattern above says that if solider i is in the unsafe state and we can take the torch, then we unblock the caller of take (remember that take is synchronous) and we issue a new asynchronous method call towards(i). The semantics of join-pattern is actually fairly simply. In essence, multi-set rewriting where the methods are treated as resources. The multisetrewrite library introduced in a previous post, can easily encode join-patterns (and even more, eg guards etc).<br />I will release some runnable code at some later stage.<br /><br />The point of this exercise is not to show what can be done with Join, rather, we want to establish some connections to communicating FAs. So, what's the connection? In Join, a join-pattern is triggered (aka executed) if we can match the pattern head with the specified method calls. In communicating FAs, two automatas 'communicate' if we find matching send (!) and receive (?) transitions.<br /><pre><br /><br /> p --- a! --> q r --- a? --> t<br /><br />-----------------------------------------<br /><br /> (p,r) --- a --> (q,t)<br /><br /></pre><br />Each component of the tuple corresponds to the states of a communicating FA (CFA). If one CFA has a send edge (a!) which matches the receiving edge (a?) of another CFA, then we make a transition along those edges as shown in the above diagram. This smells similar to Join, right? Indeed, in Join we can represent<br /><pre><br /> p --- a! --> q<br /></pre><br />by<br /><pre><br />p = do a<br /> q<br /></pre><br />and <br /><pre><br /> p --- a? --> q<br /></pre><br />by<br /><pre><br />p & a = q<br /></pre><br />The states are turned into asynchronous method calls and the actions 'a' are turned into synchronous method calls.<br /><br /><br />In fact, the Join program shown above was derived from the following CFAs<br />using this translation scheme.<br /><br />The torch CFA:<br /><br /><a title="View Torch document on Scribd" href="https://www.scribd.com/doc/7770247/Torch" style="margin: 12px auto 6px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 14px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block; text-decoration: underline;">Torch</a> <object codebase="https://download.macromedia.com/pub/shockwave/cabs/flash/swflash.cab#version=9,0,0,0" id="doc_187238637089065" name="doc_187238637089065" classid="clsid:d27cdb6e-ae6d-11cf-96b8-444553540000" align="middle" height="500" width="100%"> <param name="movie" value="https://documents.scribd.com/ScribdViewer.swf?document_id=7770247&access_key=key-h7bfuhnnajkktvhttkh&page=1&version=1&viewMode="> <param name="quality" value="high"> <param name="play" value="true"> <param name="loop" value="true"> <param name="scale" value="showall"> <param name="wmode" value="opaque"> <param name="devicefont" value="false"> <param name="bgcolor" value="#ffffff"> <param name="menu" value="true"> <param name="allowFullScreen" value="true"> <param name="allowScriptAccess" value="always"> <param name="salign" value=""> <embed src="https://documents.scribd.com/ScribdViewer.swf?document_id=7770247&access_key=key-h7bfuhnnajkktvhttkh&page=1&version=1&viewMode=" quality="high" pluginspage="https://www.macromedia.com/go/getflashplayer" play="true" loop="true" scale="showall" wmode="opaque" devicefont="false" bgcolor="#ffffff" name="doc_187238637089065_object" menu="true" allowfullscreen="true" allowscriptaccess="always" salign="" type="application/x-shockwave-flash" align="middle" height="500" width="100%"></embed> </object> <div style="margin: 6px auto 3px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 12px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block;"> <a href="https://www.scribd.com/upload" style="text-decoration: underline;">Get your own</a> at Scribd or <a href="https://www.scribd.com/browse" style="text-decoration: underline;">explore</a> others: </div><br /><br />The soldier CFA:<br /><a title="View Soldier document on Scribd" href="https://www.scribd.com/doc/7770522/Soldier-3" style="margin: 12px auto 6px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 14px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block; text-decoration: underline;">Soldier 3</a> <object codebase="https://download.macromedia.com/pub/shockwave/cabs/flash/swflash.cab#version=9,0,0,0" id="doc_552798581192173" name="doc_552798581192173" classid="clsid:d27cdb6e-ae6d-11cf-96b8-444553540000" align="middle" height="500" width="100%"> <param name="movie" value="https://documents.scribd.com/ScribdViewer.swf?document_id=7770522&access_key=key-mm97og9meqaxpvvnm9f&page=1&version=1&viewMode="> <param name="quality" value="high"> <param name="play" value="true"> <param name="loop" value="true"> <param name="scale" value="showall"> <param name="wmode" value="opaque"> <param name="devicefont" value="false"> <param name="bgcolor" value="#ffffff"> <param name="menu" value="true"> <param name="allowFullScreen" value="true"> <param name="allowScriptAccess" value="always"> <param name="salign" value=""> <embed src="https://documents.scribd.com/ScribdViewer.swf?document_id=7770522&access_key=key-mm97og9meqaxpvvnm9f&page=1&version=1&viewMode=" quality="high" pluginspage="https://www.macromedia.com/go/getflashplayer" play="true" loop="true" scale="showall" wmode="opaque" devicefont="false" bgcolor="#ffffff" name="doc_552798581192173_object" menu="true" allowfullscreen="true" allowscriptaccess="always" salign="" type="application/x-shockwave-flash" align="middle" height="500" width="100%"></embed> </object> <div style="margin: 6px auto 3px auto; font-family: Helvetica,Arial,Sans-serif; font-style: normal; font-variant: normal; font-weight: normal; font-size: 12px; line-height: normal; font-size-adjust: none; font-stretch: normal; -x-system-font: none; display: block;"> <a href="https://www.scribd.com/upload" style="text-decoration: underline;">Get your own</a> at Scribd or <a href="https://www.scribd.com/browse" style="text-decoration: underline;">explore</a> others: </div><br /><br />It's also possible to systematically translate Join programs to CFAs but it's getting more tedious to work out the details. Both languages are equally expressive. However, (I claim) Join allows us to specify more complex coordination patterns more easily than CFAs (therefore the transformation to CFAs gets quite involved). The advantages of having a Join representation of CFAs is that we know how to efficiently execute Join programs (eg see the multisetrewrite library which exploits join-style concurrency by executing non-overlapping join-patterns in parallel). On the other hand, a CFA representation of Join allows to make use of UPPAAL's expressive query language and its model checking facilities. For example, via the query<br /><pre><br />E<> safe(1) and safe(2) and safe(3) and safe(4)<br /></pre><br />we can check if (assuming we have four soldiers) it's possible for all four soldiers to reach the safe side. E says there exists a trace and <> says there exists a state. <br /><br />We can also check if the system does not deadlock<br /><pre><br />A[] not deadlock<br /></pre><br />This property is not satisfied for the following reason. In case all four soldiers are on the safe side and one solider makes its way back to the unsafe side, the soldier gets to the unsafe side but won't be able to get back to the safe side. Remember that in our torch model, we require two soldiers per torch. For this example at least, the deadlock property doesn't say much. We only know that the program will terminate (possibly in some undesired state).<br /><br />UPPAAL's query language is a subset of CTL btw. This implies that we canNOT verify (very compliated) queries such as "are the join-patterns confluent". Confluence requires to quantify over traces, then over states and then again over traces which is beyond CTL (for good reasons because it gets way too complex to check such properties). <br /><br />Anyway, the connection between Join and CFAs is quite useful. This way I became a much better UPPAAL user. First write your program in Join and then convert to CFAs. I will write more about this connection at some later stage. Unknown noreply@blogger.com 2 tag:blogger.com,1999:blog-4642782805835050446.post-7379957968145451327 2008-11-05T05:21:00.000-08:00 2008-11-09T08:42:24.954-08:00 Playing with regular expressions: Intersection We implement symbolic intersection among regular expression<br />by adapting Antimirov's regular expression rewriting algorithm.<br />By symbolic we mean that regular expression are not transformed to <br />automata. We rewrite regular expressions by using partial derivatives.<br /><br />The algorithm (highlights):<br /><br /><pre><br /> r1 `intersect` r2 =<br /><br /> let [l1,...,ln] = lettersOf (r1 | r2)<br /> in<br /><br /> (l1, partDeriv r1 l1 `intersect` partDeriv r2 l1)<br /> | ...<br /> | (l1, partDeriv r1 ln `intersect` partDeriv r2 ln)<br /></pre><br /><br />The idea is that each regular expression is turned into a <br />'disjunction' of clauses where each clause starts with<br />a letter, followed by the partial derivative of the regular<br />expression wrt that letter.<br /><br />You probably will know Brzozowski's derivative operation <br />which says that <br /><br /><pre><br /> derivative r l = [ w | (l,w) in L(r) ]<br /></pre><br /><br />If we would use derivatives the above algorithm<br />is non-terminating. For example,<br /><br /><pre><br /> deriv (Star (L 'A')) 'A'<br />--> <<>,'A'*><br /><br /> deriv (deriv (Star (L 'A')) 'A') 'A'<br />--> (<{},'A'*>|<<>,'A'*>)<br /></pre><br /><br />and so on. The nice property of partial derivatives is that<br />they are 'finite'. Each regular expression has a finite<br />number of partial derivatives. For example,<br /><br /><pre><br /> partDeriv (Star (L 'A')) 'A'<br /><br />--> <<>,'A'*><br /><br /> partDeriv (partDeriv (Star (L 'A')) 'A') 'A'<br />--> <<>,'A'*><br /></pre><br /><br />Please check the paper<br /><br />Valentin M. Antimirov: Partial Derivatives of Regular Expressions and Finite Automaton Constructions. <br />Theor. Comput. Sci. 155(2): 291-319 (1996)<br /><br />for more details on derivatives, partial derivatives and their connection<br />(roughly, derivatives correspond to DFA states and partial derivatives correspond to NFA states).<br /><br /><br />There's another source of non-termination which we explain via<br />the following example.<br /><br /><pre><br /> A* `intersect` A*<br /><br />--> (A, A* `intersect` A*)<br /></pre><br /><br />where we simplified partDeriv A* A --> <<>,A*> to A*<br /><br />The point to note is that the proof tree is infinite. The standard approach<br />is to use co-induction which then yields a finite (recursive) proof.<br /><br />OK, here's finally the Haskell implementation:<br /><br /><pre><br />> {-# LANGUAGE GADTs #-} <br /><br />We're just using the GADT syntax to write 'ordinary' algebraic data types<br /><br />> module RegExpIntersection where<br /><br />> import List<br /><br /><br />> data RE a where<br />> Phi :: RE a -- empty language<br />> Empty :: RE a -- empty word<br />> L :: a -> RE a -- single letter taken from alphabet a<br />> Choice :: RE a -> RE a -> RE a -- r1 + r2<br />> Seq :: RE a -> RE a -> RE a -- (r1,r2)<br />> Star :: RE a -> RE a -- r*<br />> Var :: Int -> RE a -- first-order variables to represent regular equations<br />> deriving Eq<br /><br />A word is a list of alphabet letters<br /><br />> type Word a = [a]<br /><br />Pretty printing of regular expressions<br /><br />> instance Show a => Show (RE a) where<br />> show Phi = "{}"<br />> show Empty = "<>"<br />> show (L c) = show c<br />> show (Choice r1 r2) = ("(" ++ show r1 ++ "|" ++ show r2 ++ ")")<br />> show (Seq r1 r2) = ("<" ++ show r1 ++ "," ++ show r2 ++ ">")<br />> show (Star r) = (show r ++ "*")<br /><br />Turning a list of regular expressions into a regular expression by using | (choice)<br /><br />> resToRE :: [RE a] -> RE a<br />> resToRE (r:res) = foldl Choice r res<br />> resToRE [] = Phi<br /><br /><br />Computing the set of letters of a regular expression<br /><br />> sigmaRE :: Eq a => RE a -> [a]<br />> sigmaRE (L l) = [l]<br />> sigmaRE (Seq r1 r2) = nub ((sigmaRE r1) ++ (sigmaRE r2))<br />> sigmaRE (Choice r1 r2) = nub ((sigmaRE r1) ++ (sigmaRE r2))<br />> sigmaRE (Star r) = sigmaRE r<br />> sigmaRE Phi = []<br />> sigmaRE Empty = []<br /><br /><br />Testing if a regular expression is empty (empty word)<br /><br />> isEmpty :: RE a -> Bool<br />> isEmpty Phi = False<br />> isEmpty Empty = True<br />> isEmpty (Choice r1 r2) = (isEmpty r1) || (isEmpty r2)<br />> isEmpty (Seq r1 r2) = (isEmpty r1) && (isEmpty r2)<br />> isEmpty (Star r) = True<br />> isEmpty (L _) = False<br /><br />Testing if a regular expression contains nothing<br /><br />> isPhi :: RE a -> Bool<br />> isPhi Phi = True<br />> isPhi Empty = False<br />> isPhi (Choice r1 r2) = (isPhi r1) && (isPhi r2)<br />> isPhi (Seq r1 r2) = (isPhi r1) || (isPhi r2)<br />> isPhi (Star r) = False<br />> isPhi (L _) = False<br /><br /><br />Brzozowski's derivative operation <br />deriv r l denotes the regular expression where the <br />"leading l has been removed"<br />(not necessary for the intersection algorithm,<br />only included to illustrate the difference<br />to the upcoming partial derivative algorithm)<br /><br />> deriv :: Eq a => RE a -> a -> RE a<br />> deriv Phi _ = Phi<br />> deriv Empty _ = Phi<br />> deriv (L l1) l2<br />> | l1 == l2 = Empty<br />> | otherwise = Phi<br />> deriv (Choice r1 r2) l = <br />> Choice (deriv r1 l) (deriv r2 l)<br />> deriv (Seq r1 r2) l =<br />> if isEmpty r1 <br />> then Choice (Seq (deriv r1 l) r2) (deriv r2 l)<br />> else Seq (deriv r1 l) r2<br />> deriv (this@(Star r)) l =<br />> Seq (deriv r l) this<br /><br /><br /><br />(a variant) of Antimirov's partial derivative operation<br /><br />Antimirov demands that partDeriv (Star (L 'A')) 'A' yields [A*]<br />whereas our version yields [<<>,'A'*>].<br />The difference is not essential here.<br /><br />> partDeriv :: Eq a => RE a -> a -> [RE a]<br />> partDeriv Phi l = []<br />> partDeriv Empty l = []<br />> partDeriv (L l') l <br />> | l == l' = [Empty]<br />> | otherwise = []<br />> partDeriv (Choice r1 r2) l = nub ((partDeriv r1 l) ++ (partDeriv r2 l))<br />> partDeriv (Seq r1 r2) l <br />> | isEmpty r1 = <br />> let s1 = [ (Seq r1' r2) | r1' <- partDeriv r1 l ]<br />> s2 = partDeriv r2 l<br />> in nub (s1 ++ s2)<br />> | otherwise = [ (Seq r1' r2) | r1' <- partDeriv r1 l ]<br />> partDeriv (Star r) l = [ (Seq r' (Star r)) | r' <- partDeriv r l ]<br /><br /><br />Here's finally the partial derivative based intersection algorithm.<br /><br /><br />> type Env a = [((RE a, RE a), RE a)]<br /><br /><br />> intersectRE :: Eq a => RE a -> RE a -> RE a<br />> intersectRE r1 r2 = intersectC [] r1 r2<br /><br />> intersectC :: Eq a => Env a -> RE a -> RE a -> RE a<br />> intersectC env r1 r2 <br />> | r1 == Phi || r2 == Phi = Phi<br />> | r1 == Empty || r2 == Empty = Empty<br />> | otherwise =<br />> case lookup (r1,r2) env of<br />> Just r -> r<br />> Nothing -><br />> let letters = sigmaRE (r1 `Choice` r2)<br />> env' = ((r1,r2),r):env<br />> r1l l = resToRE $ partDeriv r1 l<br />> r2l l = resToRE $ partDeriv r2 l<br />> r' = resToRE $ map (\l -> Seq (L l) (intersectC env' (r1l l) (r2l l))) letters<br />> r = if (isEmpty r1) && (isEmpty r2)<br />> then Choice r' Empty<br />> else r'<br />> in r<br /><br />The problem with the algorithm is that we use recursion in Haskell to model<br />recursive proofs. For example, try<br /><br />intersect rAstar rAstar<br /><br /><br /><br /><br />Converting a regular equation into a regular expression<br /><br />We assume that variables x appears (if at all) at position (r,Var x)<br />convert2 traveres the regexp and yields (r1,r2)<br />where the invariant is that r1 is part of the loop and r2 is the base case<br /><br />> convert :: Int -> RE a -> RE a<br />> convert x r = let (r1,r2) = convert2 x r<br />> in Seq (Star r1) r2<br /><br />> convert2 :: Int -> RE a -> (RE a, RE a)<br />> convert2 x Empty = (Empty, Empty)<br />> convert2 x (Var y)<br />> | x == y = (Empty,Empty)<br />> | otherwise = (Empty, Var y) -- can this happen?<br />> convert2 x (r@(Seq l r1))<br />> | contains x r1 = let (r2,r3) = convert2 x r1<br />> in (Seq l r2, r3)<br />> | otherwise = (Empty, r)<br />> convert2 x (Choice r1 r2) = let (r1', r1'') = convert2 x r1<br />> (r2', r2'') = convert2 x r2<br />> in (Choice r1' r2', Choice r1'' r2'')<br /><br />> contains :: Int -> RE a -> Bool<br />> contains x (Var y) = x == y<br />> contains x (Seq r1 r2) = contains x r1 || contains x r2<br />> contains x (Star r) = contains x r<br />> contains x (Choice r1 r2) = contains x r1 || contains x r2<br />> contains x _ = False<br /><br /><br />We use first-order syntax to represent recursive proofs/regular expressions.<br />We then use convert to actually build the non-recursive regular expression.<br /><br /><br />> intersectRE2 :: Eq a => RE a -> RE a -> RE a<br />> intersectRE2 r1 r2 = intersectC2 1 [] r1 r2<br /><br />> intersectC2 :: Eq a => Int -> Env a -> RE a -> RE a -> RE a<br />> intersectC2 cnt env r1 r2 <br />> | r1 == Phi || r2 == Phi = Phi<br />> | r1 == Empty || r2 == Empty = Empty<br />> | otherwise =<br />> case lookup (r1,r2) env of<br />> Just r -> r<br />> Nothing -><br />> let letters = sigmaRE (r1 `Choice` r2)<br />> env' = ((r1,r2),Var cnt):env<br />> r1l l = resToRE $ partDeriv r1 l<br />> r2l l = resToRE $ partDeriv r2 l<br />> r' = resToRE $ map (\l -> Seq (L l) (intersectC2 (cnt+1) env' (r1l l) (r2l l))) letters<br />> r = if (isEmpty r1) && (isEmpty r2)<br />> then Choice r' Empty<br />> else r'<br />> in convert cnt r<br /><br /><br />For testing purposes, it's handy to have a function which tests for (semantic)<br />equality among regular expressions (again written using partial derivatives).<br /><br /><br />> type EnvEq a = [(RE a, RE a)]<br /><br />> eqRE :: Eq a => RE a -> RE a -> Bool<br />> eqRE r1 r2 = eqREC [] r1 r2<br /><br />> eqREC :: Eq a => EnvEq a -> RE a -> RE a -> Bool<br />> eqREC env r1 r2 <br />> | isEmpty r1 && (not (isEmpty r2)) = False<br />> | isPhi r1 && (not (isPhi r2)) = False<br />> | otherwise =<br />> if elem (r1,r2) env<br />> then True<br />> else let letters = sigmaRE (r1 `Choice` r2)<br />> env' = (r1,r2):env<br />> r1l l = resToRE $ partDeriv r1 l<br />> r2l l = resToRE $ partDeriv r2 l<br />> in and $ map (\l -> eqREC env' (r1l l) (r2l l)) letters<br /><br />examples<br /><br />> rA = L 'A'<br />> rAstar = Star rA<br />> rB = L 'B'<br />> rBstar = Star rB<br />> rAorBstar = Star (Choice rA rB)<br /><br />Some sample runs (using intersectRE2, intersectRE won't terminate for interesting cases)<br /><br />*RegExpIntersection> intersectRE2 rAstar rBstar<br /><((<>|<>)|<>)*,((<'A',{}>|<'B',{}>)|<>)><br />*RegExpIntersection> eqRE Empty (intersectRE2 rAstar rBstar)<br />True<br />*RegExpIntersection> intersectRE2 rAorBstar rBstar<br /><((<>|<>)|<>)*,((<'A',{}>|<'B',<((<>|<'B',<>>)|<>)*,((<'A',{}>|<>)|<>)>>)|<>)><br />*RegExpIntersection> eqRE rBstar (intersectRE2 rAorBstar rBstar)<br />True<br />*RegExpIntersection> intersectRE2 rAorBstar rAorBstar<br /><((<>|<>)|<>)*,((<'A',<((<'A',<>>|<'B',<>>)|<>)*,((<>|<>)|<>)>>|<'B',<((<'A',<>>|<'B',<>>)|<>)*,((<>|<>)|<>)>>)|<>)><br />*RegExpIntersection> eqRE rAorBstar (intersectRE2 rAorBstar rAorBstar)<br />True<br />*RegExpIntersection> eqRE rAstar (intersectRE2 rAorBstar rAorBstar)<br />False<br />*RegExpIntersection> eqRE rBstar (intersectRE2 rAorBstar rAorBstar)<br />False<br /><br /><br />The regular expressions generated by the convert function are 'very verbose'.<br />There's space for lots of improvement.<br /></pre> Unknown noreply@blogger.com 15 tag:blogger.com,1999:blog-4642782805835050446.post-5444462411862247889 2008-10-28T12:32:00.000-07:00 2008-12-06T09:36:01.911-08:00 Multi-set rewrite rules with guards and a parallel execution scheme <h3> Latest news/updates </h3><br /><br /><ul> <br /><li> Sat Dec 6 18:34:20 CET 2008:<br /><ul><br /> <li> Parallel join pattern with guards and propagation extension built on top of multisetrewrite.<br /><li> Check here <a href="https://sulzmann.blogspot.com/2008/12/parallel-join-patterns-with-guards-and.html">here</a> for more information.<br /></ul><br /><li> Wed Nov 12 11:08:47 CET 2008:<br /><ul><br /> <li><br />New <a href ="https://hackage.haskell.org/cgi-bin/hackage-scripts/package/multisetrewrite-0.1.1"> multisetrewrite-0.1.1</a> version uploaded to hackage<br /> <li> Includes more examples, a CHRSolver.hs and Join.hs abstraction<br /> built on top of multi-set rewrite<br /> <li> Some fun examples using these abstractions: GossipingGirls and BaggerProblem.<br /></ul><br /><br /></ul><br /><br /><h3> Brief description </h3><br /><br /><br />We provide a library for multi-set rewrite rules with guards. Rewrite rules are executed concurrently as long as they operate on non-overlapping left-hand sides. We make use of highly-concurrent, non-blocking data structures based on CAS lists. Thus, we can parallelize concurrent rule executions on a multi-core architecture.<br /><br />The library is similar in style to the below described actor library. The difference is that while actors run concurrently, their receive clauses (sort of multi-set rewrite rules) are only executed sequentially.<br /><br /><h3> Download </h3><br /><br />The multisetrewrite library is implemented in Haskell and available<br />via<br /><br />https://hackage.haskell.org<br /><br />(look for the multisetrewrite library among the Concurrency packages)<br /><br /><h3> Examples </h3><br /><br />The library comes with two examples (will hopefully increase over time).<br /><br /><h4> Concurrent stack </h4><br /><br />The gist of the multi-set rewrite rules describing a concurrent stack (the actual example in Stack.hs is more verbose, after all it's 'only' a library and not<br />a new compiler).<br /><br /><pre><br /> [push x, pop y] .->. y := x<br /><br /> [push x, stack s] .->. stack (x:s)<br /><br /> [pop y, stack s] `when` (isNotEmptyStack s) .->. let (x:xs) = s<br /> y := x<br /> stack xs<br /></pre><br /><br />push is synchronous whereas pop and stack are asynchronous. The above shows how to encode join-patterns via multisetrewrite. We are more expressive than join-patterns because we also support guards, non-linear (aka shared) variables (doesn't show up in the above).<br /><br /><h4> CHR solver </h4><br /><br />On top of multisetrewrite we implement a CHR solver. See CHR.hs in the distribution.<br />To illustrate the expressive power, we implement the mergesort algorithm<br />via multi-set rewrite rules.<br /><br /><br />Here's the gist of the rules (as said above already, the actual implementation is more verbose).<br /><pre><br /> Leq(x,a) \ Leq(x,b) when a < b <==> Leq(a,b)<br /> Merge(n,a), Merge(n,b) when a < b <==> \Leq(a,b),\Merge(n+1,a)<br /></pre><br /><br /><br />Points to note:<br /><ul><br /> <li> The right-hand side of the first rule uses a mix of propagation and simplification. Leq(x,a) is propagated (ie not removed) whereas Leq(x,b) is simplified.<br /><li> We make use of non-linear variables and guards in both rules.<br /><br /></ul> Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-5584058610486512919 2008-10-20T11:15:00.000-07:00 2008-10-21T02:03:11.091-07:00 Actors with Multi-Headed Receive Clauses The actor model provides high-level concurrency abstractions to coordinate simultaneous computations by message passing. Languages implementing the actor model such as Erlang commonly only support single-headed pattern matching over received messages.<br />In <br /><pre><br />Martin Sulzmann, Edmund S. L. Lam, Peter Van Weert: <br />Actors with Multi-headed Message Receive Patterns. <br />COORDINATION 2008: 315-330<br /></pre><br />we propose an extension of the Actor model with receive clauses supporting multi-headed message patterns.<br /><br />Here's a simple example of a market-place actor<br /><pre><code><br />receive<br /> Seller x, Buyer x -> "match found"<br /></code></pre><br /><br />We employ the combination of multiple messages in a receive pattern and non-linear patterns to test for a matching seller and a buyer. Non-linear patterns are in fact a short-hand for guards. That is, the above is equivalent to<br /><pre><br />receive<br /> Seller x, Buyer y when x == y -> "match found"<br /></pre><br /><br />The formal details of a such an enriched actor model are described in the above mentioned paper. We have also implemented the system as a library extension in Haskell. More on this below.<br /><br /><br /><br /><h2> Haskell-Actor Implementation </h2><br /><br /><h3> Download </h3><br /><br />Available via<br /><br />https://hackage.haskell.org<br /><br />(look for the actor library among the Concurrency packages)<br /><br /><h3> Overview </h3><br /><br />The Haskell-Actor implementation makes use of<br /><br /><ul><br /> <li> Haskell channels to represent the actors mailbox, and<br /> <li> user-definable pattern matching implemented via type class overloading.<br /></ul><br /><br />Haskell channels provide the basic abstraction to write (send) and read (receive) from a channel (mailbox). Thus, we can straightforwardly model actors with *single-headed* receive clauses. That is, we read messages one at a time and check for the occurrence of a specific message. The novelty of Haskell-Actor mailboxes is that we can test for the ocurrence of multiple messages via *multi-headed* receive clauses (see the above market-place example).<br /><br />Messages are user-definable via Haskell data types. The user needs to provide some boiler-plate code (type class instances) to define message pattern matching.<br /><br /><br /><h3> Details </h3><br /><br />To use Haskell-Actor library you'll need<br />to understand the following combinators.<br /><br /><ul><br /> <li> receive<br /> <li> send<br /> <li> createActor<br /> <li> runActor<br /> <li> kill<br /></ul><br /><br />We'll discuss each of the above in turn.<br /><br /><h4> receive </h4><br /><br />receive is similar to case statements in Haskell. One difference is that we can match against multiple messages (see the above market-place actor).<br /><br />Haskell doesn't allow us to overload the pattern matching syntax (it's a library extension). We solve this by providing (generic) primitives to implement multi-headed message pattern matching in receive clauses by providing a (generic) set of primitives which need to be extended by the user for the specific message type (described as a data type).<br /><br />For example, consider the following simple message type found in the Chain.hs example<br /><br /><pre><br />data Msg = Blah deriving (Eq,Show)<br /></pre><br /><br />There are two things, the user needs to provide.<br /><br /><ul><br /> <li> Hash-map: Message are indexed based on their constructor names to speed up the search for matching message patterns.<br /><br /><pre><br />valhashOp = HashOp { numberOfTables = 1, hashMsg = \ _ -> 1 }<br /></pre><br /><br /><li> Specific pattern matcher:<br /><br /><pre><br />instance EMatch Msg where<br /> match tags m1 m2 = return (m1 == m2, tags)<br /></pre><br /><br />We extend the generic matcher by a message specific case.<br /><br /></ul><br /><br />By providing the hash-map and the message-specific matcher, we can define an actor which waits for the 'Blah' message to arrive and then sends the same message to its neighbor.<br /><br /><pre><br />actorChain neighbor self = <br /> receive self<br /> [ [Blah] .->. send (toPID neighbor) Blah ]<br /></pre><br /><br />NOTE: The receive statement is similar to case statements in Haskell. That is, we make explicit the actor/mailbox to which we apply a list of receive clauses. In Erlang, the actor/mailbox is implicit.<br /><br /><h4> send </h4><br /><br />Given the pid (process identification number, similar to Erlang) we can send a message to an actor. For example,<br /><br /><pre><br />send (toPID neighbor) Blah <br /></pre><br /><br />toPID is a primitive which extracts the pid from the neighbor actor<br /><br /><h4> createActor </h4><br /><br /><pre><br />createActor :: HashOp msg -> IO (Act msg)<br /></pre><br />creates a new actor for a specific message type, given<br />a hash-map. For example,<br /><pre><br />(initialActor :: Act Msg) <- createActor valhashOp<br /></pre><br /><br /><h4> runActor </h4><br /><br /><pre><br />runActor :: Act msg -> (Act msg -> IO ()) -> IO ()<br /></pre><br /><br />We spawn a new (Haskell) thread in which we apply the first argument (the actor) to the second argument (the behavior). For example,<br /><br /><pre><br />runActor curr (actorChain prev)<br /></pre><br />where curr refers to the current actor and prev to the previous actor.<br /><br /><br /><h4> kill </h4><br /><br /><pre><br />kill :: PID msg -> IO ()<br /></pre><br /><br />simply kills the thread (we don't kill any sub-actor threads, must be taken care of by the user).<br /><br /><h3> Examples </h3><br /><br />The below examples are part of the distribution.<br /><br /><h4> Chain.hs </h4><br /><br />Creates some n number of actors which pass around some message.<br /><br /><br /><h4> PingPong.hs </h4><br /><br />The standard ping-pong actor example. Simply call the main function and see what's happening.<br /><br /><h4> MarketPlace.hs </h4><br /><br />A market-place using server and client actors. Call the main function to invoke the server. To invoke a client open a new terminal and execute 'telnet localhost 4242' for connecting clients to the server. You'll be asked for your name (sent to the server and the server informs everybody about new clients) and what item you'd like to sell or buy. The server then checks for matching buyers and sellers.<br /><br />This example uses pattern variables and multi-headed pattern receive clauses.<br />Pattern variable need to be created explicitly because we implement actors<br />(i.e. pattern matching over messages) as a library.<br />Here are some code snippets.<br /><br /><pre><br /> ; x <- newVar :: IO (VAR String)<br /> ; let go = <br /> receive client<br /> [ [arrivedMsg x] .->.<br /> do { v1 <- readVar x<br /> ; hPutStrLn hdl ("\n Arrived: " ++ show v1)<br /> ; go <br /> } <br /> , ... ]<br /></pre><br /><br />We explicitly create a pattern variable x which we then<br />use in the message pattern 'arrivedMsg x'.<br /><br />To distinguish between values and variables we use 'lifted' types.<br /><br /><pre><br />data L a = Val a <br /> | Var (VAR a) deriving Eq<br /> -- see ActorBase.hs for the internal variable representation<br /> -- (only for the curious reader/user)<br /><br />data MsgClient = Arrived (L String)<br /> -- notifies about newly arrived clients<br /></pre><br /><br />It's of course pretty clumsy to write down lifted types.<br />Here's a nicer (type class) interface.<br /><br /><pre><br />-- client interface<br />class ArrivedMsg a where<br /> arrivedMsg :: a -> MsgClient<br /><br />instance ArrivedMsg (VAR String) where<br /> arrivedMsg x = Arrived (Var x)<br />instance ArrivedMsg String where<br /> arrivedMsg s = Arrived (Val s)<br /></pre><br /><br /><br />In case of many different types of messages/constructors, this 'boilerplate' code is straightforward but tedious to write down. We should eventually look into Template Haskell (future work). Unknown noreply@blogger.com 1 tag:blogger.com,1999:blog-4642782805835050446.post-6883547476151514438 2008-05-01T01:23:00.000-07:00 2008-05-01T01:32:55.110-07:00 Partial Derivative Regular Expression Pattern Matching <pre><br /><br /><span class="'conid'">Regular</span> <span class="'varid'">expression</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'keyword'">as</span> <span class="'varid'">found</span> <span class="'keyword'">in</span> <span class="'varid'">domain</span><span class="'comment'">-</span><span class="'varid'">specific</span><br /><span class="'definition'">languages</span> <span class="'varid'">such</span> <span class="'keyword'">as</span> <span class="'conid'">XDuce</span><span class="'layout'">,</span> <span class="'conid'">CDuce</span><span class="'layout'">,</span> <span class="'conid'">XHaskell</span> <span class="'varid'">is</span> <span class="'varid'">a</span> <span class="'varid'">highly</span> <span class="'varid'">useful</span><br /><span class="'definition'">concept</span> <span class="'varid'">but</span> <span class="'varid'">is</span> <span class="'varid'">not</span> <span class="'varid'">commonly</span> <span class="'varid'">supported</span> <span class="'varid'">by</span> <span class="'varid'">mainstream</span> <span class="'varid'">languages</span><span class="'varop'">.</span><br /><span class="'conid'">Below</span> <span class="'conid'">I</span> <span class="'varid'">give</span> <span class="'varid'">an</span> <span class="'varid'">elementary</span> <span class="'conid'">Haskell</span> <span class="'varid'">implementation</span> <span class="'keyword'">of</span> <span class="'varid'">regular</span> <span class="'varid'">expression</span><br /><span class="'definition'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">based</span> <span class="'varid'">on</span> <span class="'layout'">(</span><span class="'varid'">partial</span><span class="'layout'">)</span> <span class="'varid'">derivatives</span> <span class="'keyword'">of</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span><span class="'varop'">.</span><br /><br /><br /><span class="'conid'">This</span> <span class="'varid'">work</span> <span class="'varid'">is</span> <span class="'varid'">part</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'conid'">XHaskell</span> <span class="'varid'">project</span><span class="'layout'">,</span> <span class="'varid'">carried</span><br /><span class="'definition'">out</span> <span class="'keyword'">in</span> <span class="'varid'">collaboration</span> <span class="'varid'">with</span> <span class="'varid'">my</span> <span class="'conid'">PhD</span> <span class="'varid'">student</span> <span class="'conid'">Kenny</span> <span class="'conid'">Lu</span> <span class="'conid'">Zhuo</span><span class="'varop'">.</span><br /><span class="'conid'">Thanks</span> <span class="'varid'">to</span> <span class="'conid'">Burak</span> <span class="'conid'">Emir</span> <span class="'varid'">for</span> <span class="'varid'">helpful</span> <span class="'varid'">discussions</span><br /><span class="'layout'">(</span><span class="'varid'">and</span> <span class="'varid'">suggesting</span> <span class="'varid'">the</span> <span class="'varid'">name</span> <span class="'varid'">partial</span> <span class="'varid'">derivate</span> <span class="'varid'">regexp</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /><span class="'conid'">This</span> <span class="'varid'">post</span> <span class="'varid'">is</span> <span class="'varid'">a</span> <span class="'varid'">literate</span> <span class="'conid'">Haskell</span> <span class="'varid'">file</span> <span class="'layout'">(</span><span class="'varid'">converted</span> <span class="'varid'">to</span> <span class="'varid'">html</span> <span class="'varid'">thanks</span><br /><span class="'definition'">to</span> <span class="'conid'">Malcolm</span> <span class="'conid'">Wallace's</span> <span class="'varid'">hscolour</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /><span class="'comment'">---------------</span><br /><span class="'comment'">-- Motivation </span><br /><br /><span class="'conid'">Our</span> <span class="'varid'">goal</span> <span class="'varid'">is</span> <span class="'varid'">to</span> <span class="'varid'">understand</span> <span class="'varid'">and</span> <span class="'varid'">implement</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">involving</span><br /><span class="'definition'">regular</span> <span class="'varid'">expressions</span> <span class="'varid'">a</span> <span class="'varid'">la</span> <span class="'conid'">XDuce</span><span class="'layout'">,</span> <span class="'conid'">CDuce</span> <span class="'varid'">and</span> <span class="'conid'">XHaskell</span><span class="'varop'">.</span><br /><span class="'conid'">Here's</span> <span class="'varid'">a</span> <span class="'varid'">simple</span> <span class="'varid'">example</span> <span class="'varid'">that</span> <span class="'varid'">illustrates</span> <span class="'varid'">what's</span> <span class="'varid'">going</span> <span class="'varid'">on</span><span class="'varop'">.</span><br /><br /><span class="'definition'">f</span> <span class="'keyglyph'">::</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'keyglyph'">-></span> <span class="'conid'">Text</span><span class="'varop'">*</span><br /><span class="'definition'">f</span> <span class="'conid'">()</span> <span class="'keyglyph'">=</span> <span class="'conid'">()</span><br /><span class="'definition'">f</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Text</span><span class="'varop'">+</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span> <span class="'varid'">f</span> <span class="'varid'">y</span><span class="'layout'">)</span><br /><span class="'definition'">f</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Space</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">f</span> <span class="'varid'">y</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">above</span> <span class="'varid'">function</span> <span class="'varid'">removes</span> <span class="'varid'">all</span> <span class="'layout'">(</span><span class="'varid'">white</span><span class="'layout'">)</span> <span class="'varid'">space</span> <span class="'varid'">from</span> <span class="'varid'">a</span> <span class="'varid'">text</span><span class="'varop'">.</span><br /><span class="'conid'">We</span> <span class="'varid'">assume</span> <span class="'varid'">that</span> <span class="'conid'">Text</span> <span class="'varid'">refers</span> <span class="'varid'">to</span> <span class="'varid'">some</span> <span class="'varid'">alpha</span><span class="'comment'">-</span><span class="'varid'">numeric</span> <span class="'varid'">character</span><span class="'varop'">.</span><br /><br /><span class="'conid'">We</span> <span class="'varid'">expect</span> <span class="'varid'">that</span><br /><br /><span class="'definition'">f</span> <span class="'str'">" Hello Bye"</span> <span class="'varid'">yields</span> <span class="'str'">"HelloBye"</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">what's</span> <span class="'varid'">happening</span> <span class="'varid'">during</span> <span class="'varid'">the</span> <span class="'varid'">evaluation</span> <span class="'keyword'">of</span> <span class="'varid'">f</span> <span class="'str'">" Hello Bye"</span><span class="'varop'">.</span><br /><br /><span class="'conid'">We</span> <span class="'varid'">match</span> <span class="'varid'">the</span> <span class="'varid'">input</span> <span class="'str'">" Hello Bye"</span> <span class="'varid'">against</span> <span class="'varid'">each</span> <span class="'varid'">pattern</span> <span class="'varid'">clause</span><br /><span class="'layout'">(</span><span class="'varid'">from</span> <span class="'varid'">top</span> <span class="'varid'">to</span> <span class="'varid'">bottom</span><span class="'layout'">)</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">first</span> <span class="'varid'">clause</span> <span class="'varid'">cleary</span> <span class="'varid'">doesn't</span> <span class="'varid'">apply</span><span class="'layout'">,</span> <span class="'varid'">so</span> <span class="'varid'">does</span> <span class="'varid'">not</span> <span class="'varid'">the</span> <span class="'varid'">second</span> <span class="'varid'">clause</span><br /><span class="'definition'">becaues</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Text</span><span class="'varop'">+</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varid'">matches</span> <span class="'varid'">only</span><br /><span class="'definition'">input</span> <span class="'varid'">that</span> <span class="'varid'">starts</span> <span class="'varid'">with</span> <span class="'varid'">some</span> <span class="'conid'">Text</span><span class="'varop'">.</span><br /><span class="'conid'">The</span> <span class="'varid'">third</span> <span class="'varid'">pattern</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Space</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varid'">applies</span><span class="'varop'">.</span><br /><span class="'conid'">The</span> <span class="'varid'">subpattern</span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Space</span><span class="'varop'">*</span> <span class="'varid'">binds</span> <span class="'varid'">any</span> <span class="'varid'">number</span> <span class="'keyword'">of</span> <span class="'varid'">spaces</span><span class="'varop'">.</span> <span class="'conid'">We</span> <span class="'varid'">assume</span><br /><span class="'definition'">that</span> <span class="'varid'">we</span> <span class="'varid'">greedily</span> <span class="'varid'">consumes</span> <span class="'varid'">spaces</span><span class="'varop'">.</span> <span class="'conid'">Hence</span><span class="'layout'">,</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">match</span><br /><span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Space</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">Space</span> <span class="'keyglyph'">|</span> <span class="'conid'">Text</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varid'">against</span> <span class="'str'">" Hello Bye"</span> <span class="'varid'">yields</span> <span class="'str'">"HelloBye"</span><br /><span class="'definition'">yields</span><br /><br /> <span class="'varid'">x</span> <span class="'varid'">holds</span> <span class="'str'">" "</span> <span class="'layout'">(</span><span class="'varid'">the</span> <span class="'varid'">three</span> <span class="'varid'">leading</span> <span class="'varid'">spaces</span><span class="'layout'">)</span><br /> <span class="'varid'">y</span> <span class="'varid'">holds</span> <span class="'str'">"Hello Bye"</span> <span class="'layout'">(</span><span class="'varid'">the</span> <span class="'varid'">rest</span><span class="'layout'">)</span><br /><br /><span class="'layout'">(</span><span class="'conid'">Note</span><span class="'conop'">:</span> <span class="'conid'">We</span> <span class="'varid'">view</span> <span class="'varid'">here</span> <span class="'varid'">a</span> <span class="'varid'">string</span> <span class="'keyword'">as</span> <span class="'varid'">a</span> <span class="'varid'">concenation</span> <span class="'keyword'">of</span> <span class="'conid'">Space</span> <span class="'varid'">and</span> <span class="'conid'">Text</span><span class="'layout'">)</span><br /><br /><span class="'conid'">Having</span> <span class="'varid'">established</span> <span class="'varid'">the</span> <span class="'varid'">binding</span> <span class="'keyword'">of</span> <span class="'varid'">pattern</span> <span class="'varid'">variables</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">can</span><br /><span class="'definition'">execute</span> <span class="'varid'">the</span> <span class="'varid'">body</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">clause</span><span class="'varop'">.</span> <span class="'conid'">This</span> <span class="'varid'">leads</span> <span class="'varid'">to</span><br /><br /><span class="'varid'">f</span> <span class="'str'">"Hello Bye"</span><br /><br /><span class="'conid'">Again</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">check</span> <span class="'varid'">which</span> <span class="'varid'">pattern</span> <span class="'varid'">matches</span> <span class="'varid'">the</span> <span class="'varid'">input</span> <span class="'str'">"Hello Bye"</span><span class="'varop'">.</span><br /><span class="'conid'">This</span> <span class="'varid'">time</span> <span class="'varid'">the</span> <span class="'varid'">second</span> <span class="'varid'">pattern</span> <span class="'varid'">applies</span> <span class="'varid'">and</span> <span class="'varid'">we</span> <span class="'varid'">find</span> <span class="'varid'">that</span><br /><br /> <span class="'varid'">x</span> <span class="'varid'">holds</span> <span class="'str'">"Hello"</span> <span class="'layout'">(</span><span class="'varid'">all</span> <span class="'varid'">non</span><span class="'comment'">-</span><span class="'varid'">empty</span> <span class="'varid'">text</span><span class="'layout'">)</span><br /> <span class="'varid'">y</span> <span class="'varid'">holds</span> <span class="'str'">" Bye"</span> <span class="'layout'">(</span><span class="'varid'">the</span> <span class="'varid'">rest</span><span class="'layout'">)</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">subsequent</span> <span class="'varid'">call</span> <span class="'varid'">is</span><br /><br /><span class="'varid'">f</span> <span class="'str'">" Bye"</span><br /><br /><span class="'conid'">It</span> <span class="'varid'">should</span> <span class="'varid'">be</span> <span class="'varid'">clear</span> <span class="'varid'">now</span> <span class="'varid'">how</span> <span class="'varid'">the</span> <span class="'varid'">rest</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'varid'">computation</span> <span class="'varid'">progresses</span><span class="'varop'">.</span><br /><span class="'conid'">We</span> <span class="'varid'">keep</span> <span class="'varid'">all</span> <span class="'varid'">text</span> <span class="'varid'">but</span> <span class="'varid'">throw</span> <span class="'varid'">away</span> <span class="'varid'">all</span> <span class="'varid'">spaces</span><span class="'varop'">.</span><br /><span class="'conid'">Hence</span><span class="'layout'">,</span><br /><br /><span class="'definition'">f</span> <span class="'str'">" Hello Bye"</span><br /><br /><span class="'definition'">evaluates</span> <span class="'varid'">to</span><br /><br /><span class="'str'">"HelloBye"</span><br /><br /><br /><span class="'conid'">The</span> <span class="'varid'">main</span> <span class="'varid'">difference</span> <span class="'varid'">to</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">a</span> <span class="'varid'">la</span> <span class="'conid'">ML</span> <span class="'varid'">and</span> <span class="'conid'">Haskell</span> <span class="'varid'">is</span> <span class="'varid'">that</span><br /><span class="'definition'">we</span> <span class="'varid'">can</span> <span class="'conid'">NOT</span> <span class="'varid'">perform</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">match</span> <span class="'varid'">by</span> <span class="'varid'">comparing</span> <span class="'varid'">the</span> <span class="'varid'">structure</span><br /><span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">against</span> <span class="'varid'">the</span> <span class="'varid'">structure</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'varid'">incoming</span> <span class="'varid'">value</span><span class="'varop'">.</span><br /><span class="'conid'">The</span> <span class="'varid'">reason</span> <span class="'varid'">is</span> <span class="'varid'">that</span> <span class="'varid'">a</span> <span class="'varid'">pattern</span> <span class="'varid'">like</span><br /><br /><span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><span class="'definition'">can</span> <span class="'varid'">possibly</span> <span class="'varid'">match</span> <span class="'varid'">a</span> <span class="'varid'">number</span> <span class="'keyword'">of</span> <span class="'varid'">structurally</span> <span class="'varid'">different</span> <span class="'varid'">values</span> <span class="'varid'">such</span> <span class="'keyword'">as</span><br /><br /> <span class="'str'">""</span> <span class="'layout'">(</span><span class="'varid'">also</span> <span class="'varid'">known</span> <span class="'keyword'">as</span> <span class="'varid'">epsilon</span><span class="'layout'">)</span><br /><br /> <span class="'str'">"A"</span><br /><br /> <span class="'str'">"AA"</span><br /><br /> <span class="'varid'">and</span> <span class="'varid'">so</span> <span class="'varid'">on</span><br /><br /><br /><span class="'conid'">The</span> <span class="'varid'">challenge</span> <span class="'varid'">is</span> <span class="'varid'">that</span> <span class="'varid'">we</span> <span class="'varid'">need</span> <span class="'varid'">to</span> <span class="'varid'">take</span> <span class="'varid'">into</span> <span class="'varid'">account</span> <span class="'varid'">the</span> <span class="'varid'">semantic</span><br /><span class="'definition'">meaning</span> <span class="'keyword'">of</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span> <span class="'varid'">when</span> <span class="'varid'">performing</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">match</span><span class="'varop'">.</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">another</span> <span class="'varid'">tricky</span> <span class="'varid'">example</span><span class="'varop'">.</span><br /><span class="'conid'">Matching</span> <span class="'varid'">the</span> <span class="'varid'">input</span> <span class="'str'">"AB"</span> <span class="'varid'">against</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'conop'">:</span><span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span><span class="'conop'">:</span><span class="'layout'">(</span><span class="'layout'">(</span><span class="'conid'">A</span><span class="'layout'">,</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'keyglyph'">|</span> <span class="'conid'">B</span><span class="'layout'">)</span><span class="'layout'">)</span><br /><span class="'definition'">yields</span> <span class="'varid'">the</span> <span class="'varid'">following</span> <span class="'varid'">pattern</span> <span class="'varid'">bindings</span><br /><br /> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'str'">""</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'str'">"AB"</span><span class="'layout'">)</span><br /><br /><span class="'definition'">and</span><br /><br /> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'str'">"A"</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'str'">"B"</span><span class="'layout'">)</span><br /><br /><span class="'conid'">This</span> <span class="'varid'">shows</span> <span class="'varid'">that</span> <span class="'varid'">regular</span> <span class="'varid'">expression</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span><br /><span class="'definition'">is</span> <span class="'varid'">indeterministic</span> <span class="'layout'">(</span><span class="'varid'">unless</span> <span class="'varid'">we</span> <span class="'varid'">fix</span> <span class="'varid'">a</span> <span class="'varid'">specific</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">policy</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /><br /><span class="'comment'">-----------------------------------------------</span><br /><span class="'comment'">-- Formalizing the Pattern Matching Relation</span><br /><br /><br /><span class="'conid'">We</span> <span class="'varid'">first</span> <span class="'varid'">need</span> <span class="'varid'">to</span> <span class="'varid'">fix</span> <span class="'varid'">the</span> <span class="'varid'">language</span> <span class="'keyword'">of</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span> <span class="'varid'">and</span> <span class="'varid'">patterns</span><span class="'varop'">.</span><br /><br /><br /><span class="'varid'">r</span> <span class="'conop'">::=</span> <span class="'varid'">r</span> <span class="'varop'">+</span> <span class="'varid'">r</span> <span class="'comment'">-- choice</span><br /> <span class="'comment'">-- later, we often write (r | r) instead of (r + r)</span><br /> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">,</span><span class="'varid'">r</span><span class="'layout'">)</span> <span class="'comment'">-- concatenation</span><br /> <span class="'keyglyph'">|</span> <span class="'varid'">r</span><span class="'varop'">*</span> <span class="'comment'">-- repetition</span><br /> <span class="'keyglyph'">|</span> <span class="'varid'">epsilon</span> <span class="'comment'">-- empty word</span><br /> <span class="'keyglyph'">|</span> <span class="'conid'">A</span> <span class="'keyglyph'">|</span> <span class="'conid'">B</span> <span class="'keyglyph'">|</span> <span class="'varop'">...</span> <span class="'comment'">-- alphabet symbols/letters</span><br /><br /><span class="'varid'">p</span> <span class="'conop'">::=</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'comment'">-- r is a regular expression</span><br /> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varid'">p</span><span class="'layout'">,</span><span class="'varid'">p</span><span class="'layout'">)</span> <span class="'comment'">-- pairs</span><br /> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varid'">p</span> <span class="'varop'">+</span> <span class="'varid'">p</span><span class="'layout'">)</span> <span class="'comment'">-- choice</span><br /><br /><br /><br /><span class="'conid'">The</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">relation</span><br /><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p</span> <span class="'varop'">~></span> <span class="'varid'">env</span><br /><br /><span class="'definition'">pronounced</span><br /><br /><span class="'str'">"word w matches pattern p and yiels the environment env"</span><br /><br /><span class="'layout'">(</span><span class="'conid'">Note</span><span class="'conop'">:</span> <span class="'varid'">words</span> <span class="'varid'">are</span> <span class="'varid'">strings</span><span class="'layout'">,</span> <span class="'varid'">sequences</span> <span class="'keyword'">of</span> <span class="'varid'">letters</span><span class="'varop'">/</span><span class="'varid'">characters</span><span class="'layout'">)</span><br /><br /><br /><span class="'conid'">Here</span> <span class="'varid'">are</span> <span class="'varid'">the</span> <span class="'varid'">rules</span> <span class="'varid'">describing</span> <span class="'varid'">all</span> <span class="'varid'">valid</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">relations</span><span class="'varop'">.</span><br /><span class="'conid'">We</span> <span class="'varid'">write</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">)</span> <span class="'varid'">to</span> <span class="'varid'">denote</span> <span class="'varid'">the</span> <span class="'varid'">language</span> <span class="'varid'">describe</span> <span class="'varid'">by</span> <span class="'varid'">a</span> <span class="'varid'">regular</span> <span class="'varid'">expression</span><span class="'varop'">.</span><br /><br /><br /> <span class="'varid'">w</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">)</span><br /><span class="'layout'">(</span><span class="'conid'">Var</span><span class="'layout'">)</span> <span class="'comment'">-------------------------</span><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'keyglyph'">::</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">w</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><br /> <span class="'varid'">w</span> <span class="'keyglyph'">=</span> <span class="'varid'">w1</span> <span class="'varid'">w2</span><br /> <span class="'varid'">w1</span> <span class="'varop'"><|</span> <span class="'varid'">p1</span> <span class="'varop'">~></span> <span class="'varid'">env1</span><br /> <span class="'varid'">w2</span> <span class="'varop'"><|</span> <span class="'varid'">p2</span> <span class="'varop'">~></span> <span class="'varid'">env2</span> <br /><span class="'layout'">(</span><span class="'conid'">Pair</span><span class="'layout'">)</span> <span class="'comment'">-----------------------------</span><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">p1</span><span class="'layout'">,</span><span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'varid'">env1</span> <span class="'varop'">++</span> <span class="'varid'">env2</span><br /><br /><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p1</span> <span class="'varop'">~></span> <span class="'varid'">env1</span><br /><span class="'layout'">(</span><span class="'conid'">Choice1</span><span class="'layout'">)</span> <span class="'comment'">------------------------</span><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p1</span> <span class="'varop'">+</span> <span class="'varid'">p2</span> <span class="'varop'">~></span> <span class="'varid'">env1</span><br /><br /><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p2</span> <span class="'varop'">~></span> <span class="'varid'">env2</span><br /><span class="'layout'">(</span><span class="'conid'">Choice1</span><span class="'layout'">)</span> <span class="'comment'">------------------------</span><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p1</span> <span class="'varop'">+</span> <span class="'varid'">p2</span> <span class="'varop'">~></span> <span class="'varid'">env2</span><br /><br /><br /><span class="'conid'">How</span> <span class="'varid'">to</span> <span class="'varid'">implement</span> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p</span> <span class="'varop'">~></span> <span class="'varid'">env</span><br /><span class="'conid'">How</span> <span class="'varid'">to</span> <span class="'varid'">cope</span> <span class="'varid'">with</span> <span class="'varid'">indeterminism</span><span class="'varop'">?</span><br /><br /><span class="'conid'">For</span> <span class="'varid'">example</span><span class="'layout'">,</span> <span class="'varid'">consider</span><br /><br /><span class="'layout'">(</span><span class="'num'">1</span><span class="'layout'">)</span><br /><br /><span class="'conid'">AA</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">epsilon</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">AA</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'conid'">A</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">A</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'conid'">AA</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'varid'">epsilon</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><br /><span class="'conid'">A</span> <span class="'varid'">sample</span> <span class="'varid'">derivation</span> <span class="'varid'">for</span> <span class="'varid'">the</span> <span class="'varid'">first</span> <span class="'keyword'">case</span><br /><br /><br /> <span class="'varid'">epsilon</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /> <span class="'comment'">----------------------------------</span><br /> <span class="'varid'">epsilon</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'conop'">:</span><span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">epsilon</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><br /> <span class="'conid'">AA</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /> <span class="'comment'">-----------------------</span><br /> <span class="'conid'">AA</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'conop'">:</span><span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">AA</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /> <span class="'comment'">------------------------------------------------</span><br /> <span class="'conid'">AA</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">epsilon</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">AA</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><span class="'layout'">(</span><span class="'num'">2</span><span class="'layout'">)</span><br /><br /><span class="'conid'">Recall</span> <span class="'varid'">the</span> <span class="'varid'">earlier</span> <span class="'varid'">example</span><span class="'varop'">.</span><br /><br /><span class="'conid'">AB</span> <span class="'varop'"><|</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'layout'">(</span><span class="'conid'">A</span><span class="'layout'">,</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'keyglyph'">|</span> <span class="'conid'">B</span><span class="'layout'">)</span><span class="'layout'">)</span><br /><br /> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'conid'">A</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /> <span class="'varop'">~></span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">epsilon</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'varid'">y</span><span class="'layout'">,</span><span class="'conid'">AB</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><br /><span class="'conid'">Before</span> <span class="'varid'">we</span> <span class="'varid'">develop</span> <span class="'varid'">an</span> <span class="'varid'">algorithm</span> <span class="'varid'">for</span> <span class="'varid'">the</span><br /><span class="'definition'">regular</span> <span class="'varid'">expression</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">problem</span><br /><span class="'definition'">let's</span> <span class="'varid'">consider</span> <span class="'varid'">a</span> <span class="'varid'">simpler</span> <span class="'varid'">problem</span><span class="'conop'">:</span><br /><br /><span class="'conid'">How</span> <span class="'varid'">to</span> <span class="'varid'">check</span> <span class="'varid'">that</span> <span class="'varid'">w</span> <span class="'varid'">is</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'varid'">pronounced</span> <span class="'keyword'">as</span><br /><br /><span class="'str'">"Word w matches the regular expression r"</span><br /><br /><span class="'layout'">(</span><span class="'conid'">This</span> <span class="'varid'">is</span> <span class="'varid'">also</span> <span class="'varid'">known</span> <span class="'keyword'">as</span> <span class="'varid'">the</span> <span class="'varid'">word</span> <span class="'varid'">problem</span><span class="'layout'">)</span><br /><br /><span class="'conid'">We</span> <span class="'varid'">solve</span> <span class="'varid'">the</span> <span class="'varid'">word</span> <span class="'varid'">problem</span> <span class="'varid'">by</span> <span class="'varid'">applying</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span> <span class="'varid'">algorithm</span><span class="'conop'">:</span><br /><br /> <span class="'varid'">w</span> <span class="'varid'">matches</span> <span class="'varid'">r</span> <span class="'varid'">iff</span><br /><br /> <span class="'keyword'">case</span> <span class="'varid'">w</span> <span class="'keyglyph'">=</span> <span class="'varid'">epsilon</span><span class="'conop'">:</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r</span><br /><br /> <span class="'varid'">isEmpty</span> <span class="'varid'">yields</span> <span class="'conid'">True</span> <span class="'keyword'">if</span> <span class="'varid'">the</span> <span class="'varid'">r</span> <span class="'varid'">is</span> <span class="'varid'">empty</span><span class="'layout'">,</span> <span class="'varid'">otherwise</span> <span class="'conid'">False</span><br /> <span class="'conid'">The</span> <span class="'varid'">definition</span> <span class="'varid'">is</span> <span class="'varid'">straightforward</span><span class="'varop'">.</span> <span class="'conid'">See</span> <span class="'varid'">below</span><span class="'varop'">.</span><br /><br /> <span class="'keyword'">case</span> <span class="'varid'">w</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">l</span><span class="'layout'">,</span><span class="'varid'">v</span><span class="'layout'">)</span><span class="'conop'">:</span> <span class="'varid'">v</span> <span class="'varid'">matches</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><br /><br /> <span class="'keyword'">where</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'varid'">is</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span> <span class="'keyword'">of</span> <span class="'varid'">r</span> <span class="'varid'">wrt</span> <span class="'varid'">l</span><br /><br /><br /> <span class="'conid'">We</span> <span class="'varid'">obtain</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'varid'">by</span> <span class="'varid'">take</span> <span class="'varid'">away</span> <span class="'varid'">all</span> <span class="'str'">"leading"</span> <span class="'varid'">l's</span><span class="'varop'">.</span><br /> <span class="'conid'">Semantically</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">can</span> <span class="'varid'">explain</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span><br /> <span class="'varid'">operation</span> <span class="'keyword'">as</span> <span class="'varid'">follows</span><span class="'conop'">:</span><br /><br /> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">{</span> <span class="'varid'">w</span> <span class="'keyglyph'">|</span> <span class="'varid'">lw</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">)</span> <span class="'layout'">}</span><br /><br /> <span class="'conid'">Below</span> <span class="'varid'">we</span> <span class="'varid'">define</span> <span class="'varid'">a</span> <span class="'varid'">function</span> <span class="'varid'">which</span> <span class="'varid'">computes</span> <span class="'varid'">an</span><br /> <span class="'varid'">expression</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'varid'">representing</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span> <span class="'keyword'">of</span><br /> <span class="'varid'">r</span> <span class="'varid'">wrt</span> <span class="'varid'">l</span><span class="'varop'">.</span><br /><br /> <span class="'conid'">We</span> <span class="'varid'">can</span> <span class="'varid'">build</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'varid'">by</span> <span class="'varid'">composition</span><br /> <span class="'keyword'">of</span> <span class="'varid'">its</span> <span class="'varid'">partial</span> <span class="'varid'">derivatives</span><span class="'varop'">.</span><br /> <span class="'conid'">For</span> <span class="'varid'">example</span><span class="'layout'">,</span><br /><br /> <span class="'layout'">(</span><span class="'varid'">r1</span> <span class="'keyglyph'">|</span> <span class="'varid'">r2</span><span class="'layout'">)</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'varid'">r1</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'keyglyph'">|</span> <span class="'varid'">r2</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><br /><br /> <span class="'conid'">We</span> <span class="'varid'">call</span> <span class="'varid'">r1</span><span class="'keyglyph'">\</span><span class="'varid'">l</span> <span class="'varid'">the</span> <span class="'varid'">partial</span> <span class="'varid'">derivative</span> <span class="'keyword'">of</span> <span class="'layout'">(</span><span class="'varid'">r1</span> <span class="'keyglyph'">|</span> <span class="'varid'">r2</span><span class="'layout'">)</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><span class="'varop'">.</span><br /> <span class="'conid'">Therefore</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">often</span> <span class="'varid'">refer</span> <span class="'varid'">to</span> <span class="'varid'">derivatives</span> <span class="'keyword'">as</span><br /> <span class="'varid'">partial</span> <span class="'varid'">derivatives</span><span class="'varop'">.</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">the</span> <span class="'varid'">implementation</span> <span class="'keyword'">in</span> <span class="'conid'">Haskell</span><span class="'varop'">.</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">regular</span> <span class="'varid'">expression</span> <span class="'varid'">language</span><span class="'layout'">,</span> <span class="'varid'">parameterized</span> <span class="'varid'">over</span> <span class="'varid'">some</span> <span class="'varid'">alphabet</span><br /><br /><span class="'varop'">></span> <span class="'keyword'">data</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'conid'">Phi</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- empty language</span><br /><span class="'varop'">></span> <span class="'conid'">Empty</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- empty word</span><br /><span class="'varop'">></span> <span class="'conid'">L</span> <span class="'keyglyph'">::</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- single letter taken from alphabet a</span><br /><span class="'varop'">></span> <span class="'conid'">Choice</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- r1 + r2</span><br /><span class="'varop'">></span> <span class="'conid'">Seq</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- (r1,r2)</span><br /><span class="'varop'">></span> <span class="'conid'">Star</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'comment'">-- r*</span><br /><span class="'varop'">></span> <span class="'keyword'">deriving</span> <span class="'conid'">Eq</span><br /><br /><span class="'conid'">Some</span> <span class="'varid'">combinators</span><br /><br /><span class="'varop'">></span> <span class="'varid'">re_star</span> <span class="'varid'">r</span> <span class="'keyglyph'">=</span> <span class="'conid'">Star</span> <span class="'varid'">r</span><br /><span class="'varop'">></span> <span class="'varid'">re_empty</span> <span class="'keyglyph'">=</span> <span class="'conid'">Empty</span><br /><span class="'varop'">></span> <span class="'varid'">re_letter</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'conid'">L</span> <span class="'varid'">l</span><br /><span class="'varop'">></span> <span class="'varid'">re_choice</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span> <span class="'keyglyph'">=</span> <span class="'conid'">Choice</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><br /><span class="'varop'">></span> <span class="'varid'">re_pair</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span> <span class="'keyglyph'">=</span> <span class="'conid'">Seq</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><br /><br /><span class="'conid'">A</span> <span class="'varid'">word</span> <span class="'varid'">is</span> <span class="'varid'">a</span> <span class="'varid'">list</span> <span class="'keyword'">of</span> <span class="'varid'">alphabet</span> <span class="'varid'">letters</span><br /><br /><span class="'varop'">></span> <span class="'keyword'">type</span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">=</span> <span class="'keyglyph'">[</span><span class="'varid'">a</span><span class="'keyglyph'">]</span><br /><br /><span class="'conid'">Pretty</span> <span class="'varid'">printing</span> <span class="'keyword'">of</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span><br /><br /><span class="'varop'">></span> <span class="'keyword'">instance</span> <span class="'conid'">Show</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Show</span> <span class="'layout'">(</span><span class="'conid'">RE</span> <span class="'varid'">a</span><span class="'layout'">)</span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'conid'">Phi</span> <span class="'keyglyph'">=</span> <span class="'str'">"{}"</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'conid'">Empty</span> <span class="'keyglyph'">=</span> <span class="'str'">"<>"</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'varid'">c</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">show</span> <span class="'varid'">c</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">Choice</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'str'">"("</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">r1</span> <span class="'varop'">++</span> <span class="'str'">"|"</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">r2</span> <span class="'varop'">++</span> <span class="'str'">")"</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">Seq</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'str'">"<"</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">r1</span> <span class="'varop'">++</span> <span class="'str'">","</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">r2</span> <span class="'varop'">++</span> <span class="'str'">">"</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">show</span> <span class="'varid'">r</span> <span class="'varop'">++</span> <span class="'str'">"*"</span><span class="'layout'">)</span><br /><br /><br /><span class="'conid'">Matching</span> <span class="'varid'">words</span> <span class="'varid'">against</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span><br /><br /><span class="'varop'">></span> <span class="'varid'">matchWord</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Bool</span><br /><span class="'varop'">></span> <span class="'varid'">matchWord</span> <span class="'varid'">r</span> <span class="'conid'">[]</span> <span class="'keyglyph'">=</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r</span><br /><span class="'varop'">></span> <span class="'varid'">matchWord</span> <span class="'varid'">r</span> <span class="'layout'">(</span><span class="'varid'">l</span><span class="'conop'">:</span><span class="'varid'">w</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">matchWord</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">w</span><br /><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'keyglyph'">::</span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Bool</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'conid'">Phi</span> <span class="'keyglyph'">=</span> <span class="'conid'">False</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'conid'">Empty</span> <span class="'keyglyph'">=</span> <span class="'conid'">True</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'conid'">Choice</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">isEmpty</span> <span class="'varid'">r1</span><span class="'layout'">)</span> <span class="'varop'">||</span> <span class="'layout'">(</span><span class="'varid'">isEmpty</span> <span class="'varid'">r2</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'conid'">Seq</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">isEmpty</span> <span class="'varid'">r1</span><span class="'layout'">)</span> <span class="'varop'">&&</span> <span class="'layout'">(</span><span class="'varid'">isEmpty</span> <span class="'varid'">r2</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">True</span><br /><span class="'varop'">></span> <span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'keyword'">_</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">False</span><br /><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">RE</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'conid'">Phi</span> <span class="'keyword'">_</span> <span class="'keyglyph'">=</span> <span class="'conid'">Phi</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'conid'">Empty</span> <span class="'keyword'">_</span> <span class="'keyglyph'">=</span> <span class="'conid'">Phi</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'varid'">l1</span><span class="'layout'">)</span> <span class="'varid'">l2</span> <span class="'keyglyph'">=</span> <span class="'keyword'">if</span> <span class="'varid'">l1</span> <span class="'varop'">==</span> <span class="'varid'">l2</span> <span class="'keyword'">then</span> <span class="'conid'">Empty</span> <span class="'keyword'">else</span> <span class="'conid'">Phi</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'conid'">Choice</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'conid'">Choice</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r2</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'conid'">Seq</span> <span class="'varid'">r1</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'keyword'">if</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r1</span><br /><span class="'varop'">></span> <span class="'keyword'">then</span> <span class="'conid'">Choice</span> <span class="'layout'">(</span><span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r2</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyword'">else</span> <span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">r2</span><br /><span class="'varop'">></span> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'varid'">this</span><span class="'keyglyph'">@</span><span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'varid'">r</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">this</span><br /><br /><br /><span class="'conid'">Most</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'varid'">cases</span> <span class="'varid'">are</span> <span class="'varid'">straightforward</span><span class="'varop'">.</span><br /><span class="'conid'">In</span> <span class="'keyword'">case</span> <span class="'keyword'">of</span> <span class="'layout'">(</span><span class="'varid'">r1</span><span class="'layout'">,</span> <span class="'varid'">r2</span><span class="'layout'">)</span> <span class="'keyglyph'">\</span> <span class="'varid'">l</span> <span class="'varid'">we</span> <span class="'varid'">need</span> <span class="'varid'">to</span> <span class="'varid'">take</span> <span class="'varid'">care</span> <span class="'keyword'">of</span> <span class="'varid'">the</span> <span class="'keyword'">case</span> <span class="'varid'">that</span> <span class="'varid'">r1</span> <span class="'varid'">is</span> <span class="'varid'">empty</span><span class="'varop'">!</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">an</span> <span class="'varid'">example</span><br /><br /> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'conid'">A</span><br /><span class="'keyglyph'">=</span> <span class="'layout'">(</span> <span class="'varid'">partDeriv</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span> <span class="'conid'">A</span> <span class="'layout'">,</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'layout'">)</span><br /><span class="'keyglyph'">=</span> <span class="'layout'">(</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'conid'">A</span> <span class="'conid'">A</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'conid'">B</span> <span class="'conid'">A</span><span class="'layout'">)</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><span class="'keyglyph'">=</span> <span class="'layout'">(</span> <span class="'conid'">()</span> <span class="'keyglyph'">|</span> <span class="'conid'">Phi</span><span class="'layout'">,</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><span class="'varid'">effectively</span><br /><br /><span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">above</span> <span class="'varid'">also</span> <span class="'varid'">explains</span> <span class="'varid'">why</span> <span class="'varid'">we</span> <span class="'varid'">need</span> <span class="'conid'">Phi</span><span class="'varop'">.</span><br /><br /><br /><span class="'definition'">some</span> <span class="'varid'">examples</span><br /><br /><span class="'varop'">></span> <span class="'varid'">r1</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'conid'">Choice</span> <span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'layout'">(</span><span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'A'</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'B'</span><span class="'layout'">)</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'B'</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'comment'">-- ((A,B)*|B)</span><br /><span class="'varop'">></span> <span class="'varid'">r2</span> <span class="'keyglyph'">=</span> <span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'A'</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'conid'">Star</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'A'</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'comment'">-- (A*,A*)</span><br /><span class="'varop'">></span> <span class="'varid'">r3</span> <span class="'keyglyph'">=</span> <span class="'conid'">Star</span> <span class="'layout'">(</span><span class="'conid'">Choice</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'A'</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'conid'">L</span> <span class="'chr'">'B'</span><span class="'layout'">)</span><span class="'layout'">)</span> <span class="'comment'">-- (A|B)*</span><br /><br /><span class="'varop'">></span> <span class="'varid'">w1</span> <span class="'keyglyph'">=</span> <span class="'str'">"AABBAAA"</span><br /><span class="'varop'">></span> <span class="'varid'">m1</span> <span class="'keyglyph'">=</span> <span class="'varid'">matchWord</span> <span class="'varid'">r1</span> <span class="'varid'">w1</span><br /><span class="'varop'">></span> <span class="'varid'">m2</span> <span class="'keyglyph'">=</span> <span class="'varid'">matchWord</span> <span class="'varid'">r2</span> <span class="'varid'">w1</span><br /><span class="'varop'">></span> <span class="'varid'">m3</span> <span class="'keyglyph'">=</span> <span class="'varid'">matchWord</span> <span class="'varid'">r3</span> <span class="'varid'">w1</span><br /><br /><br /><span class="'conid'">Let's</span> <span class="'varid'">get</span> <span class="'varid'">back</span> <span class="'varid'">to</span> <span class="'varid'">our</span> <span class="'varid'">problem</span> <span class="'keyword'">of</span> <span class="'varid'">implementing</span><br /><span class="'definition'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span> <span class="'varid'">relation</span><br /><br /> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">p</span> <span class="'varop'">~></span> <span class="'varid'">env</span><br /><br /><br /><span class="'comment'">--------------------------------------------------</span><br /><span class="'comment'">-- Towards a regexp pattern matching algorithm</span><br /><br /><br /><span class="'conid'">The</span> <span class="'varid'">key</span> <span class="'varid'">idea</span><span class="'conop'">:</span> <span class="'conid'">We</span> <span class="'varid'">apply</span> <span class="'varid'">the</span> <span class="'varid'">idea</span> <span class="'keyword'">of</span> <span class="'varid'">derivatives</span> <span class="'varid'">to</span> <span class="'varid'">pattern</span> <span class="'varid'">matching</span><br /><br /><br /><span class="'layout'">(</span><span class="'varid'">l</span><span class="'layout'">,</span><span class="'varid'">w</span><span class="'layout'">)</span> <span class="'varop'"><|</span> <span class="'varid'">p</span> <span class="'varop'">~></span> <span class="'varid'">env</span> <span class="'varid'">iff</span> <span class="'varid'">w</span> <span class="'varop'"><|</span> <span class="'varid'">pdPat</span> <span class="'varid'">p</span> <span class="'varid'">l</span> <span class="'varop'">~></span> <span class="'varid'">env</span><br /><br /><span class="'layout'">(</span><span class="'varid'">l</span><span class="'layout'">,</span><span class="'varid'">w</span><span class="'layout'">)</span> <span class="'varid'">matches</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">p</span> <span class="'varid'">and</span> <span class="'varid'">yields</span> <span class="'varid'">environment</span> <span class="'conid'">Env</span><br /><span class="'definition'">iff</span> <span class="'varid'">w</span> <span class="'varid'">matches</span> <span class="'varid'">the</span> <span class="'layout'">(</span><span class="'varid'">partial</span><span class="'layout'">)</span> <span class="'varid'">pattern</span> <span class="'varid'">derivative</span> <span class="'varid'">p</span> <span class="'varid'">wrt</span> <span class="'varid'">l</span><br /><br /><span class="'conid'">How</span> <span class="'varid'">is</span> <span class="'varid'">pdPat</span> <span class="'varid'">defined</span><span class="'varop'">?</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">easy</span> <span class="'keyword'">case</span> <span class="'varid'">first</span><span class="'varop'">.</span><br /><br /><span class="'definition'">pdPat</span> <span class="'layout'">(</span><span class="'varid'">p1</span> <span class="'keyglyph'">|</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p2</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /><br /><span class="'conid'">What</span> <span class="'varid'">about</span><br /><br /><span class="'definition'">pdPat</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'conop'">:</span><span class="'varid'">r</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'varop'">?</span><br /><br /><span class="'conid'">We</span> <span class="'varid'">can't</span> <span class="'varid'">simply</span> <span class="'varid'">replace</span> <span class="'varop'">?</span> <span class="'varid'">by</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'conop'">:</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><span class="'conid'">Here</span> <span class="'varid'">building</span> <span class="'varid'">the</span> <span class="'varid'">derivative</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">r</span> <span class="'keyword'">of</span> <span class="'varid'">r</span> <span class="'varid'">wrt</span> <span class="'varid'">l</span> <span class="'varid'">means</span> <span class="'varid'">that</span><br /><span class="'definition'">we</span> <span class="'varid'">have</span> <span class="'varid'">consumed</span> <span class="'varid'">the</span> <span class="'varid'">input</span> <span class="'varid'">symbol</span> <span class="'varid'">l</span><span class="'varop'">.</span> <span class="'conid'">But</span> <span class="'varid'">we</span> <span class="'varid'">must</span><br /><span class="'definition'">record</span> <span class="'varid'">somewhere</span> <span class="'varid'">that</span> <span class="'varid'">we</span> <span class="'varid'">have</span> <span class="'varid'">consumed</span> <span class="'varid'">l</span><span class="'varop'">.</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">easiest</span> <span class="'varid'">method</span> <span class="'varid'">is</span> <span class="'varid'">to</span> <span class="'varid'">record</span> <span class="'varid'">with</span> <span class="'varid'">each</span><br /><span class="'definition'">variable</span> <span class="'varid'">pattern</span> <span class="'varid'">the</span> <span class="'varid'">sequence</span> <span class="'keyword'">of</span> <span class="'varid'">symbols</span><br /><span class="'definition'">which</span> <span class="'varid'">have</span> <span class="'varid'">been</span> <span class="'varid'">consumed</span> <span class="'varid'">so</span> <span class="'varid'">far</span> <span class="'varid'">by</span> <span class="'varid'">that</span> <span class="'varid'">variable</span> <span class="'varid'">pattern</span><span class="'varop'">.</span><br /><br /><span class="'conid'">So</span><span class="'layout'">,</span><br /><br /><span class="'definition'">the</span> <span class="'varid'">variable</span> <span class="'varid'">pattern</span><br /><br /><span class="'varop'"><</span><span class="'varid'">w</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'varid'">r</span><br /><br /><span class="'definition'">says</span> <span class="'varid'">that</span> <span class="'varid'">we</span> <span class="'varid'">have</span> <span class="'varid'">consumed</span> <span class="'varid'">so</span> <span class="'varid'">far</span> <span class="'varid'">w</span><span class="'layout'">,</span> <span class="'varid'">hence</span><span class="'layout'">,</span><br /><span class="'definition'">any</span> <span class="'varid'">valid</span> <span class="'varid'">pattern</span> <span class="'varid'">binding</span> <span class="'varid'">will</span> <span class="'varid'">look</span> <span class="'varid'">like</span> <span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">w</span><span class="'varop'">...</span><span class="'layout'">)</span><span class="'layout'">,</span><br /><span class="'definition'">but</span> <span class="'varid'">we</span> <span class="'varid'">yet</span> <span class="'varid'">need</span> <span class="'varid'">to</span> <span class="'varid'">consume</span> <span class="'varid'">any</span> <span class="'varid'">word</span> <span class="'varid'">v</span> <span class="'varid'">which</span><br /><span class="'definition'">is</span> <span class="'varid'">accepted</span> <span class="'varid'">by</span> <span class="'varid'">r</span> <span class="'layout'">(</span><span class="'varid'">ie</span> <span class="'varid'">v</span> <span class="'keyword'">in</span> <span class="'conid'">L</span><span class="'layout'">(</span><span class="'varid'">r</span><span class="'layout'">)</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">derivative</span> <span class="'varid'">definition</span> <span class="'varid'">for</span> <span class="'varid'">variable</span> <span class="'varid'">patterns</span><br /><span class="'definition'">is</span> <span class="'keyword'">then</span> <span class="'varid'">straightforward</span><span class="'varop'">.</span><br /><br /><span class="'definition'">pdPat</span> <span class="'varid'">l</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'varid'">w</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varop'"><</span><span class="'varid'">w</span><span class="'layout'">,</span><span class="'varid'">l</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'varid'">r</span><span class="'keyglyph'">\</span><span class="'varid'">l</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">an</span> <span class="'varid'">example</span><span class="'varop'">.</span><br /><br /><span class="'conid'">AB</span> <span class="'varop'">|></span> <span class="'layout'">(</span><span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varop'">~></span> <span class="'varid'">env</span><br /><br /><span class="'conid'">Of</span> <span class="'varid'">course</span> <span class="'varid'">env</span> <span class="'keyglyph'">=</span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'conid'">AB</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><span class="'conid'">In</span> <span class="'varid'">some</span> <span class="'varid'">intermediate</span> <span class="'varid'">steps</span> <span class="'varid'">we</span> <span class="'varid'">find</span><br /><br /><span class="'definition'">pdPat</span> <span class="'layout'">(</span><span class="'varop'"><></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'conid'">A</span> <span class="'keyglyph'">=</span> <span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <br /> <span class="'comment'">-- shortcut see earlier calculation</span><br /> <span class="'comment'">-- and *remember* that we consumed A</span><br /><br /><span class="'varid'">pdPat</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'conid'">B</span> <span class="'keyglyph'">=</span> <span class="'varop'"><</span><span class="'conid'">AB</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><br /><br /><br /><span class="'conid'">What</span> <span class="'varid'">about</span> <span class="'varid'">pair</span> <span class="'varid'">patterns</span><span class="'varop'">?</span><br /><br /><br /><span class="'definition'">pdPat</span> <span class="'layout'">(</span><span class="'varid'">p1</span><span class="'layout'">,</span><span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'keyword'">if</span> <span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p1</span><span class="'layout'">)</span><br /> <span class="'keyword'">then</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">,</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'">??</span><span class="'layout'">,</span> <span class="'varid'">pdPat</span> <span class="'varid'">p2</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /> <span class="'keyword'">else</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">,</span> <span class="'varid'">p2</span><span class="'layout'">)</span><br /><br /><span class="'definition'">stip</span> <span class="'varid'">simply</span> <span class="'varid'">extracts</span> <span class="'varid'">the</span> <span class="'varid'">regular</span> <span class="'varid'">expression</span><span class="'varop'">.</span><br /><span class="'conid'">The</span> <span class="'varid'">question</span> <span class="'varid'">is</span> <span class="'varid'">what</span> <span class="'varid'">to</span> <span class="'varid'">replace</span> <span class="'varop'">??</span> <span class="'varid'">with</span> <span class="'varop'">?</span><br /><br /><span class="'conid'">If</span> <span class="'varid'">p1</span> <span class="'varid'">is</span> <span class="'varid'">empty</span> <span class="'varid'">this</span> <span class="'varid'">means</span> <span class="'varid'">that</span> <span class="'varid'">all</span> <span class="'varid'">further</span> <span class="'varid'">matching</span> <span class="'varid'">will</span> <span class="'varid'">helping</span> <span class="'keyword'">in</span> <span class="'varid'">p2</span><span class="'varop'">.</span><br /><span class="'conid'">But</span> <span class="'varid'">we</span> <span class="'varid'">simply</span> <span class="'varid'">can't</span> <span class="'varid'">throw</span> <span class="'varid'">away</span> <span class="'varid'">p1</span> <span class="'varid'">because</span> <span class="'varid'">we</span> <span class="'varid'">record</span> <span class="'varid'">the</span> <span class="'varid'">variable</span><br /><span class="'definition'">binding</span> <span class="'keyword'">in</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">itself</span><span class="'varop'">.</span><br /><span class="'conid'">We</span> <span class="'varid'">also</span> <span class="'varid'">can't</span> <span class="'varid'">simply</span> <span class="'varid'">keep</span> <span class="'varid'">p1</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">must</span> <span class="'varid'">indicate</span> <span class="'varid'">that</span> <span class="'varid'">the</span> <span class="'varid'">matching</span><br /><span class="'definition'">uing</span> <span class="'varid'">p1</span> <span class="'varid'">is</span> <span class="'varid'">finished</span><span class="'varop'">.</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">idea</span> <span class="'varid'">is</span> <span class="'varid'">to</span> <span class="'varid'">replace</span> <span class="'varop'">??</span> <span class="'varid'">by</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'keyword'">where</span> <span class="'varid'">we</span><br /><span class="'definition'">make</span> <span class="'varid'">all</span> <span class="'varid'">regular</span> <span class="'varid'">expresssions</span> <span class="'varid'">empty</span> <span class="'layout'">(</span><span class="'keyword'">if</span> <span class="'varid'">possibly</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /><span class="'conid'">For</span> <span class="'varid'">example</span><span class="'layout'">,</span> <span class="'varid'">consider</span> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <br /><br /><span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">AB</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varop'"><></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">C</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><span class="'keyword'">where</span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'varid'">has</span> <span class="'varid'">already</span> <span class="'varid'">consumed</span> <span class="'conid'">AB</span><br /><br /><span class="'definition'">and</span> <span class="'conid'">C</span> <span class="'varid'">is</span> <span class="'varid'">the</span> <span class="'varid'">remaining</span> <span class="'varid'">input</span><span class="'varop'">.</span><br /><br /><span class="'conid'">We</span> <span class="'varid'">expect</span><br /><br /> <span class="'varid'">pdPat</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">AB</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varop'"><></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">C</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'conid'">C</span><br /><span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">ABC</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Phi</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'varid'">y</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">C</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">AB</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">()</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'conid'">C</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">C</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'keyglyph'">\</span> <span class="'conid'">C</span> <span class="'keyglyph'">=</span> <span class="'conid'">Phi</span><br /><br /> <span class="'varid'">which</span> <span class="'varid'">shows</span> <span class="'varid'">that</span> <span class="'varid'">from</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">ABC</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Phi</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'varid'">y</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">C</span><span class="'varop'">*</span><span class="'layout'">)</span><br /> <span class="'varid'">we</span> <span class="'varid'">can't</span> <span class="'varid'">obtain</span> <span class="'varid'">any</span> <span class="'varid'">valid</span> <span class="'varid'">pattern</span> <span class="'varid'">binding</span><span class="'varop'">.</span><br /><br /> <span class="'conid'">But</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'varid'">is</span> <span class="'varid'">empty</span><span class="'varop'">.</span> <span class="'conid'">Hence</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">can</span> <span class="'varid'">stop</span> <span class="'varid'">matching</span><br /> <span class="'varid'">using</span> <span class="'varid'">the</span> <span class="'varid'">subpattern</span> <span class="'varop'"><</span><span class="'conid'">AB</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'varid'">which</span> <span class="'varid'">we</span> <span class="'varid'">indicate</span><br /> <span class="'varid'">by</span> <span class="'varid'">replacing</span> <span class="'layout'">(</span><span class="'conid'">A</span><span class="'keyglyph'">|</span><span class="'conid'">B</span><span class="'layout'">)</span><span class="'varop'">*</span> <span class="'varid'">with</span> <span class="'conid'">()</span> <span class="'layout'">(</span><span class="'varid'">the</span> <span class="'varid'">empty</span> <span class="'varid'">sequence</span><span class="'layout'">)</span><span class="'varop'">.</span><br /><br /> <span class="'conid'">In</span> <span class="'varid'">general</span><span class="'layout'">,</span> <span class="'varid'">to</span> <span class="'varid'">stop</span> <span class="'varid'">matching</span> <span class="'varid'">uinsg</span> <span class="'varid'">p1</span> <span class="'varid'">we</span> <span class="'varid'">need</span> <span class="'varid'">to</span> <span class="'varid'">make</span><br /> <span class="'varid'">the</span> <span class="'varid'">pattern</span> <span class="'varid'">p1</span> <span class="'varid'">empty</span> <span class="'varid'">by</span> <span class="'varid'">replacing</span> <span class="'varid'">all</span> <span class="'varid'">regular</span> <span class="'varid'">expressions</span><br /> <span class="'varid'">which</span> <span class="'varid'">contain</span> <span class="'conid'">()</span> <span class="'varid'">by</span> <span class="'conid'">()</span> <span class="'varid'">and</span> <span class="'varid'">all</span> <span class="'varid'">others</span> <span class="'varid'">we</span> <span class="'varid'">replace</span> <span class="'varid'">by</span> <span class="'conid'">Phi</span><span class="'varop'">.</span><br /><br /><span class="'conid'">Here's</span> <span class="'varid'">the</span> <span class="'varid'">implementation</span> <span class="'keyword'">of</span> <span class="'varid'">pattern</span> <span class="'varid'">derivatives</span> <span class="'keyword'">in</span> <span class="'conid'">Haskell</span><span class="'varop'">.</span><br /><br /><span class="'conid'">The</span> <span class="'varid'">pattern</span> <span class="'varid'">language</span><span class="'layout'">,</span> <span class="'varid'">we</span> <span class="'varid'">assume</span> <span class="'varid'">that</span> <span class="'varid'">patterns</span> <span class="'varid'">are</span> <span class="'varid'">linear</span><br /><br /><br /><span class="'varop'">></span> <span class="'keyword'">data</span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'conid'">PVar</span> <span class="'keyglyph'">::</span> <span class="'conid'">Int</span> <span class="'keyglyph'">-></span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span><span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'conid'">PPair</span> <span class="'keyglyph'">::</span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'conid'">PChoice</span> <span class="'keyglyph'">::</span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span><br /><br /> <span class="'comment'">-- PVar var w r</span><br /> <span class="'comment'">-- variables var are represented by Ints</span><br /> <span class="'comment'">-- w represents the part we have already seen</span><br /> <span class="'comment'">-- r represents the remaining part we yet have to match</span><br /><br /><br /><span class="'conid'">Combinators</span><br /><br /><span class="'varop'">></span> <span class="'varid'">pat_var</span> <span class="'varid'">n</span> <span class="'varid'">r</span> <span class="'keyglyph'">=</span> <span class="'conid'">PVar</span> <span class="'varid'">n</span> <span class="'conid'">[]</span> <span class="'varid'">r</span><br /><span class="'varop'">></span> <span class="'varid'">pat_pair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span> <span class="'keyglyph'">=</span> <span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><br /><span class="'varop'">></span> <span class="'varid'">pat_choice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span> <span class="'keyglyph'">=</span> <span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><br /><br /><span class="'definition'">pretty</span> <span class="'varid'">printing</span><br /><br /><span class="'varop'">></span> <span class="'keyword'">instance</span> <span class="'conid'">Show</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Show</span> <span class="'layout'">(</span><span class="'conid'">Pat</span> <span class="'varid'">a</span><span class="'layout'">)</span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">PVar</span> <span class="'varid'">i</span> <span class="'varid'">w</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'str'">"x"</span><span class="'varop'">++</span><span class="'varid'">show</span> <span class="'varid'">i</span> <span class="'varop'">++</span> <span class="'str'">"::"</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">r</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'layout'">(</span><span class="'str'">"<"</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">p1</span> <span class="'varop'">++</span> <span class="'str'">","</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">p2</span> <span class="'varop'">++</span> <span class="'str'">">"</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">show</span> <span class="'layout'">(</span><span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'str'">"("</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">p1</span> <span class="'varop'">++</span> <span class="'str'">"|"</span> <span class="'varop'">++</span> <span class="'varid'">show</span> <span class="'varid'">p2</span> <span class="'varop'">++</span> <span class="'str'">")"</span><br /><br /><br /><span class="'layout'">(</span><span class="'varid'">partial</span><span class="'layout'">)</span> <span class="'varid'">derivative</span> <span class="'keyword'">of</span> <span class="'varid'">patterns</span><br /><br /><span class="'varop'">></span> <span class="'varid'">pdPat</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'varid'">pdPat</span> <span class="'layout'">(</span><span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'varid'">w</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span> <span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'layout'">(</span><span class="'varid'">w</span> <span class="'varop'">++</span> <span class="'keyglyph'">[</span><span class="'varid'">l</span><span class="'keyglyph'">]</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">partDeriv</span> <span class="'varid'">r</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">pdPat</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'keyword'">if</span> <span class="'layout'">(</span><span class="'varid'">isEmpty</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p1</span><span class="'layout'">)</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyword'">then</span> <span class="'conid'">PChoice</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'layout'">(</span><span class="'varid'">mkEmpPat</span> <span class="'varid'">p1</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p2</span> <span class="'varid'">l</span><span class="'layout'">)</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyword'">else</span> <span class="'conid'">PPair</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">p2</span><br /><span class="'varop'">></span> <span class="'varid'">pdPat</span> <span class="'layout'">(</span><span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'varid'">l</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'conid'">PChoice</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p1</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p2</span> <span class="'varid'">l</span><span class="'layout'">)</span><br /><br /><span class="'varop'">></span> <span class="'varid'">strip</span> <span class="'keyglyph'">::</span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">RE</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'varid'">strip</span> <span class="'layout'">(</span><span class="'conid'">PVar</span> <span class="'keyword'">_</span> <span class="'varid'">w</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">r</span><br /><span class="'varop'">></span> <span class="'varid'">strip</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">Seq</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p1</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p2</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">strip</span> <span class="'layout'">(</span><span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">Choice</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p1</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">strip</span> <span class="'varid'">p2</span><span class="'layout'">)</span><br /><br /><span class="'definition'">replace</span> <span class="'varid'">all</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'varid'">w</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'varid'">by</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'varid'">w</span><span class="'varop'">></span> <span class="'varid'">x</span><span class="'conop'">:</span> <span class="'varop'"><></span><span class="'layout'">)</span> <span class="'keyword'">if</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r</span><br /><span class="'definition'">otherwise</span> <span class="'varid'">yield</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'varid'">w</span><span class="'varop'">></span> <span class="'varid'">x</span><span class="'conop'">:</span> <span class="'conid'">Phi</span><span class="'layout'">)</span><br /><br /><span class="'varop'">></span> <span class="'varid'">mkEmpPat</span> <span class="'keyglyph'">::</span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span><br /><span class="'varop'">></span> <span class="'varid'">mkEmpPat</span> <span class="'layout'">(</span><span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'varid'">w</span> <span class="'varid'">r</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyglyph'">|</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r</span> <span class="'keyglyph'">=</span> <span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'varid'">w</span> <span class="'conid'">Empty</span><br /><span class="'varop'">></span> <span class="'keyglyph'">|</span> <span class="'varid'">otherwise</span> <span class="'keyglyph'">=</span> <span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'varid'">w</span> <span class="'conid'">Phi</span><br /><span class="'varop'">></span> <span class="'varid'">mkEmpPat</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">PPair</span> <span class="'layout'">(</span><span class="'varid'">mkEmpPat</span> <span class="'varid'">p1</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">mkEmpPat</span> <span class="'varid'">p2</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">mkEmpPat</span> <span class="'layout'">(</span><span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'conid'">PChoice</span> <span class="'layout'">(</span><span class="'varid'">mkEmpPat</span> <span class="'varid'">p1</span><span class="'layout'">)</span> <span class="'layout'">(</span><span class="'varid'">mkEmpPat</span> <span class="'varid'">p2</span><span class="'layout'">)</span><br /><br /><span class="'conid'">An</span> <span class="'varid'">example</span> <span class="'varid'">to</span> <span class="'varid'">see</span> <span class="'varid'">the</span> <span class="'varid'">derivation</span> <span class="'varid'">operation</span> <span class="'varid'">on</span> <span class="'varid'">patterns</span> <span class="'keyword'">in</span> <span class="'varid'">action</span><br /><br /><span class="'layout'">(</span><span class="'varop'"><></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varop'"><></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'varid'">and</span> <span class="'varid'">input</span> <span class="'conid'">AA</span><br /><br /><span class="'varop'">--></span><span class="'conid'">A</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varop'"><></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'"><></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">()</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><span class="'varop'">--></span><span class="'conid'">A</span> <br /> <span class="'keyglyph'">|</span><br /> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">AA</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">,</span> <span class="'varop'"><></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">Phi</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">()</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'conid'">A</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span> <span class="'keyglyph'">|</span> <span class="'keyglyph'">|</span> <span class="'layout'">(</span><span class="'varop'"><></span> <span class="'varid'">x</span> <span class="'conop'">:</span> <span class="'conid'">()</span><span class="'layout'">,</span> <span class="'varop'"><</span><span class="'conid'">AA</span><span class="'varop'">></span> <span class="'varid'">y</span> <span class="'conop'">:</span> <span class="'conid'">A</span><span class="'varop'">*</span><span class="'layout'">)</span><br /><br /><br /><span class="'conid'">Observation</span><span class="'conop'">:</span> <span class="'conid'">We</span> <span class="'varid'">not</span> <span class="'varid'">only</span> <span class="'varid'">calculate</span> <span class="'varid'">one</span> <span class="'varid'">possible</span> <span class="'varid'">matching</span><span class="'layout'">,</span><br /> <span class="'varid'">we</span> <span class="'varid'">calculate</span> <span class="'varid'">all</span> <span class="'varid'">matchings</span><span class="'varop'">!</span><br /><br /><span class="'layout'">(</span><span class="'conid'">No</span> <span class="'varid'">performance</span> <span class="'varid'">penalty</span> <span class="'varid'">thanks</span> <span class="'varid'">to</span> <span class="'varid'">lazy</span> <span class="'varid'">evaluation</span><span class="'layout'">)</span><br /><br /><br /><span class="'conid'">The</span> <span class="'varid'">binding</span> <span class="'keyword'">of</span> <span class="'varid'">pattern</span> <span class="'varid'">variables</span> <span class="'varid'">to</span> <span class="'varid'">words</span><br /><br /><span class="'varop'">></span> <span class="'keyword'">type</span> <span class="'conid'">Env</span> <span class="'varid'">a</span> <span class="'keyglyph'">=</span> <span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'conid'">Int</span><span class="'layout'">,</span><span class="'conid'">Word</span> <span class="'varid'">a</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><br /><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'keyglyph'">[</span><span class="'conid'">Env</span> <span class="'varid'">a</span><span class="'keyglyph'">]</span><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'varid'">p</span> <span class="'layout'">(</span><span class="'varid'">l</span><span class="'conop'">:</span><span class="'varid'">w</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'layout'">(</span><span class="'varid'">pdPat</span> <span class="'varid'">p</span> <span class="'varid'">l</span><span class="'layout'">)</span> <span class="'varid'">w</span><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'layout'">(</span><span class="'conid'">PVar</span> <span class="'varid'">x</span> <span class="'varid'">w</span> <span class="'varid'">r</span><span class="'layout'">)</span> <span class="'conid'">[]</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'keyword'">if</span> <span class="'varid'">isEmpty</span> <span class="'varid'">r</span> <span class="'keyword'">then</span> <span class="'keyglyph'">[</span><span class="'keyglyph'">[</span><span class="'layout'">(</span><span class="'varid'">x</span><span class="'layout'">,</span><span class="'varid'">w</span><span class="'layout'">)</span><span class="'keyglyph'">]</span><span class="'keyglyph'">]</span> <span class="'keyword'">else</span> <span class="'conid'">[]</span><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'layout'">(</span><span class="'conid'">PChoice</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'conid'">[]</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p1</span> <span class="'conid'">[]</span><span class="'layout'">)</span> <span class="'varop'">++</span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p2</span> <span class="'conid'">[]</span><span class="'layout'">)</span> <br /><span class="'varop'">></span> <span class="'comment'">-- indet choice</span><br /><span class="'varop'">></span> <span class="'varid'">patMatch</span> <span class="'layout'">(</span><span class="'conid'">PPair</span> <span class="'varid'">p1</span> <span class="'varid'">p2</span><span class="'layout'">)</span> <span class="'conid'">[]</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p1</span> <span class="'conid'">[]</span><span class="'layout'">)</span> <span class="'varop'">`combine`</span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p2</span> <span class="'conid'">[]</span><span class="'layout'">)</span> <br /><span class="'varop'">></span> <span class="'comment'">-- build all possible combinations</span><br /><span class="'varop'">></span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'varid'">combine</span> <span class="'varid'">xss</span> <span class="'varid'">yss</span> <span class="'keyglyph'">=</span> <span class="'keyglyph'">[</span> <span class="'varid'">xs</span> <span class="'varop'">++</span> <span class="'varid'">ys</span> <span class="'keyglyph'">|</span> <span class="'varid'">xs</span> <span class="'keyglyph'"><-</span> <span class="'varid'">xss</span><span class="'layout'">,</span> <span class="'varid'">ys</span> <span class="'keyglyph'"><-</span> <span class="'varid'">yss</span><span class="'keyglyph'">]</span><br /><br /><span class="'varop'">></span> <span class="'varid'">longPatMatch</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Maybe</span> <span class="'layout'">(</span><span class="'conid'">Env</span> <span class="'varid'">a</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">longPatMatch</span> <span class="'varid'">p</span> <span class="'varid'">w</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'varid'">first</span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p</span> <span class="'varid'">w</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'varid'">first</span> <span class="'layout'">(</span><span class="'varid'">env</span><span class="'conop'">:</span><span class="'keyword'">_</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">return</span> <span class="'varid'">env</span><br /><span class="'varop'">></span> <span class="'varid'">first</span> <span class="'keyword'">_</span> <span class="'keyglyph'">=</span> <span class="'conid'">Nothing</span><br /><br /><br /><span class="'varop'">></span> <span class="'varid'">shortPatMatch</span> <span class="'keyglyph'">::</span> <span class="'conid'">Eq</span> <span class="'varid'">a</span> <span class="'keyglyph'">=></span> <span class="'conid'">Pat</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Word</span> <span class="'varid'">a</span> <span class="'keyglyph'">-></span> <span class="'conid'">Maybe</span> <span class="'layout'">(</span><span class="'conid'">Env</span> <span class="'varid'">a</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'varid'">shortPatMatch</span> <span class="'varid'">p</span> <span class="'varid'">w</span> <span class="'keyglyph'">=</span><br /><span class="'varop'">></span> <span class="'varid'">last</span> <span class="'layout'">(</span><span class="'varid'">patMatch</span> <span class="'varid'">p</span> <span class="'varid'">w</span><span class="'layout'">)</span><br /><span class="'varop'">></span> <span class="'keyword'">where</span><br /><span class="'varop'">></span> <span class="'varid'">last</span> <span class="'keyglyph'">[</span><span class="'varid'">env</span><span class="'keyglyph'">]</span> <span class="'keyglyph'">=</span> <span class="'varid'">return</span> <span class="'varid'">env</span><br /><span class="'varop'">></span> <span class="'varid'">last</span> <span class="'layout'">(</span><span class="'keyword'">_</span><span class="'conop'">:</span><span class="'varid'">xs</span><span class="'layout'">)</span> <span class="'keyglyph'">=</span> <span class="'varid'">last</span> <span class="'varid'">xs</span><br /><span class="'varop'">></span> <span class="'varid'">last</span> <span class="'keyword'">_</span> <span class="'keyglyph'">=</span> <span class="'conid'">Nothing</span></pre> Unknown noreply@blogger.com 0 tag:blogger.com,1999:blog-4642782805835050446.post-5759117651845406293 2008-04-12T11:48:00.000-07:00 2008-04-12T11:54:35.704-07:00 Martin Sulzmann has a blog This blog is mainly about my professional activaties in computer science. Check out my youtube account for what I'm up to in my spare time. Unknown noreply@blogger.com 0