# Purely Functional GTK+, Part 2: TodoMVC

In the last episode we built a "Hello, World" application using gi-gtk-declarative. It's now time to convert it into a to-do list application, in the style of TodoMVC.

To convert the “Hello, World!” application to a to-do list application, we begin by adjusting our data types. The Todo data type represents a single item, with a Text field for its name. We also need to import the Text type from Data.Text.

data Todo = Todo
{ name :: Text
}

Our state will no longer be (), but a data types holding Vector of Todo items. This means we also need to import Vector from Data.Vector.

data State = State
{ todos :: Vector Todo
}

As the run function returns the last state value of the state reducer loop, we need to discard that return value in main. We wrap the run action in void, imported from Control.Monad.

Let’s rewrite our view function. We change the title to “TodoGTK+” and replace the label with a todoList, which we’ll define in a where binding. We use container to declare a Gtk.Box, with vertical orientation, containing all the to-do items. Using fmap and a typed hole, we see that we need a function Todo -> BoxChild Event.

view' :: State -> AppView Gtk.Window Event
view' s = bin
Gtk.Window
[#title := "TodoGTK+", on #deleteEvent (const (True, Closed))]
todoList
where
todoList = container Gtk.Box
[#orientation := Gtk.OrientationVertical]
(fmap _ (todos s))

The todoItem will render a Todo value as a Gtk.Label displaying the name.

view' :: State -> AppView Gtk.Window Event
view' s = bin
Gtk.Window
[#title := "TodoGTK+", on #deleteEvent (const (True, Closed))]
todoList
where
todoList = container Gtk.Box
[#orientation := Gtk.OrientationVertical]
(fmap todoItem (todos s))
todoItem todo = widget Gtk.Label [#label := name todo]

Now, GHC tells us there’s a “non-type variable argument in the constraint”. The type of todoList requires us to add the FlexibleContexts language extension.

{-# LANGUAGE FlexibleContexts  #-}
module Main where

The remaining type error is in the definition of main, where the initial state cannot be a () value. We construct a State value with an empty vector.

main :: IO ()
main = void $run App { view = view' , update = update' , inputs = [] , initialState = State {todos = mempty} } ### Adding New To-Do Items While our application type-checks and runs, there are no to-do items to display, and there’s no way of adding new ones. We need to implement a form, where the user inserts text and hits the Enter key to add a new to-do item. To represent these events, we’ll add two new constructors to our Event type. data Event = TodoTextChanged Text | TodoSubmitted | Closed TodoTextChanged will be emitted each time the text in the form changes, carrying the current text value. The TodoSubmitted event will be emitted when the user hits Enter. When the to-do item is submitted, we need to know the current text to use, so we add a currentText field to the state type. data State = State { todos :: Vector Todo , currentText :: Text } We modify the initialState value to include an empty Text value. main :: IO () main = void$ run App
{ view         = view'
, update       = update'
, inputs       = []
, initialState = State {todos = mempty, currentText = mempty}
}

Now, let’s add the form. We wrap our todoList in a vertical box, containing the todoList and a newTodoForm widget.

view' :: State -> AppView Gtk.Window Event
view' s = bin
Gtk.Window
[#title := "TodoGTK+", on #deleteEvent (const (True, Closed))]
(container Gtk.Box
[#orientation := Gtk.OrientationVertical]
[todoList, newTodoForm]
)
where
...

The form consists of a Gtk.Entry widget, with the currentText of our state as its text value. The placeholder text will be shown when the entry isn’t focused. We use onM to attach an effectful event handler to the changed signal.

view' :: State -> AppView Gtk.Window Event
view' s = bin
Gtk.Window
[#title := "TodoGTK+", on #deleteEvent (const (True, Closed))]
(container Gtk.Box
[#orientation := Gtk.OrientationVertical]
[todoList, newTodoForm]
)
where
...
newTodoForm = widget
Gtk.Entry
[ #text := currentText s
, #placeholderText := "What needs to be done?"
, onM #changed _
]

The typed hole tells us we need a function Gtk.Entry -> IO Event. The reason we use onM is to have that IO action returning the event, instead of having a pure function. We need it to query the underlying GTK+ widget for it’s current text value. By using entryGetText, and mapping our event constructor over that IO action, we get a function of the correct type.

    ...
newTodoForm = widget
Gtk.Entry
[ #text := currentText s
, #placeholderText := "What needs to be done?"
, onM #changed (fmap TodoTextChanged . Gtk.entryGetText)
]

It is often necessary to use onM and effectful GTK+ operations in event handlers, as the callback type signatures rarely have enough information in their arguments. But for the next event, TodoSubmitted, we don’t need any more information, and we can use on to declare a pure event handler for the activated signal.

    ...
newTodoForm = widget
Gtk.Entry
[ #text := currentText s
, #placeholderText := "What needs to be done?"
, onM #changed (fmap TodoTextChanged . Gtk.entryGetText)
, on #activate TodoSubmitted
]

Moving to the next warning, we see that the update' function is no longer total. We are missing cases for our new events. Let’s give the arguments names and pattern match on the event. The case for Closed will be the same as before.

update' :: State -> Event -> Transition State Event
update' s e = case e of
Closed -> Exit

When the to-do text value changes, we’ll update the currentText state using a Transition. The first argument is the new state, and the second argument is an action of type IO (Maybe Event). We don’t want to emit any new event, so we use (pure Nothing).

update' :: State -> Event -> Transition State Event
update' s e = case e of
TodoTextChanged t -> Transition s { currentText = t } (pure Nothing)
Closed -> Exit

For the TodoSubmitted event, we define a newTodo value with the currentText as its name, and transition to a new state with the newTodo item appended to the todos vector. We also reset the currentText to be empty.

To use Vector.snoc, we need to add a qualified import.

import           Control.Monad                 (void)
import           Data.Text                     (Text)
import           Data.Vector                   (Vector)
import qualified Data.Vector                   as Vector
import qualified GI.Gtk                        as Gtk
import           GI.Gtk.Declarative
import           GI.Gtk.Declarative.App.Simple

Running the application, we can start adding to-do items.

## Improving the Layout

Our application doesn’t look very good yet, so let’s improve the layout a bit. We’ll begin by left-aligning the to-do items.

todoItem i todo =
widget
Gtk.Label
[#label := name todo, #halign := Gtk.AlignStart]

To push the form down to the bottom of the window, we’ll wrap the todoList in a BoxChild, and override the defaultBoxChildProperties to have the child widget expand and fill all the available space of the box.

todoList =
BoxChild defaultBoxChildProperties { expand = True, fill = True }
container Gtk.Box [#orientation := Gtk.OrientationVertical] (fmap todoItem (todos s)) We re-run the application, and see it has a nicer layout. ## Completing To-Do Items There’s one very important missing: being able to mark a to-do item as completed. We add a Bool field called completed to the Todo data type. data Todo = Todo { name :: Text , completed :: Bool } When creating new items, we set it to False. update' :: State -> Event -> Transition State Event update' s e = case e of ... TodoSubmitted -> let newTodo = Todo {name = currentText s, completed = False} in Transition s { todos = todos s Vector.snoc newTodo, currentText = mempty } (pure Nothing) ... Instead of simply rendering the name, we’ll use strike-through markup if the item is completed. We define completedMarkup, and using guards we’ll either render the new markup or render the plain name. To make it strike-through, we wrap the text value in <s> tags. widget Gtk.Label [ #label := completedMarkup todo , #halign := Gtk.AlignStart ] where completedMarkup todo | completed todo = "<s>" <> name todo <> "</s>" | otherwise = name todo For this to work, we need to enable markup for the label be setting #useMarkup to True. widget Gtk.Label [ #label := completedMarkup todo , #useMarkup := True , #halign := Gtk.AlignStart ] where completedMarkup todo | completed todo = "<s>" <> name todo <> "</s>" | otherwise = name todo In order for the user to be able to toggle the completed status, we wrap the label in a Gtk.CheckButton bin. The #active property will be set to the current completed status of the Todo value. When the check button is toggled, we want to emit a new event called TodoToggled. todoItem todo = bin Gtk.CheckButton [#active := completed todo, on #toggled (TodoToggled i)] widget
Gtk.Label
[ #label := completedMarkup todo
, #useMarkup := True
, #halign := Gtk.AlignStart
]

Let’s add the new constructor to the Event data type. It will carry the index of the to-do item.

data Event
= TodoTextChanged Text
| TodoSubmitted
| TodoToggled Int
| Closed

To get the corresponding index of each Todo value, we’ll iterate using Vector.imap instead of using fmap.

    todoList =
BoxChild defaultBoxChildProperties { expand = True, fill = True }
$container Gtk.Box [#orientation := Gtk.OrientationVertical] (Vector.imap todoItem (todos s)) todoItem i todo = ... The pattern match on events in the update' function is now missing a case for the new event constructor. Again, we’ll do a transition where we update the todos somehow. update' :: State -> Event -> Transition State Event update' s e = case e of ... TodoToggled i -> Transition s { todos = _ (todos s) } (pure Nothing) ... We need a function Vector Todo -> Vector Todo that modifies the value at the index i. There’s no handy function like that available in the vector package, so we’ll create our own. Let’s call it mapAt. update' :: State -> Event -> Transition State Event update' s e = case e of ... TodoToggled i -> Transition s { todos = mapAt i _ (todos s) } (pure Nothing) ... It will take as arguments the index, a mapping function, and a Vector a, and return a Vector a. mapAt :: Int -> (a -> a) -> Vector a -> Vector a We implement it using Vector.modify, and actions on the mutable representation of the vector. We overwrite the value at i with the result of mapping f over the existing value at i. mapAt :: Int -> (a -> a) -> Vector a -> Vector a mapAt i f = Vector.modify (\v -> MVector.write v i . f =<< MVector.read v i) To use mutable vector operations through the MVector name, we add the qualified import. import qualified Data.Vector.Mutable as MVector Finally, we implement the function to map, called toggleComplete. toggleCompleted :: Todo -> Todo toggleCompleted todo = todo { completed = not (completed todo) } update' :: State -> Event -> Transition State Event update' s e = case e of ... TodoToggled i -> Transition s { todos = mapAt i toggleComplete (todos s) } (pure Nothing) ... Now, we run our application, add some to-do items, and mark or unmark them as completed. We’re done! ## Learning More Building our to-do list application, we have learned the basics of gi-gtk-declarative and the “App.Simple” architecture. There’s more to learn, though, and I recommend checking out the project documentation. There are also a bunch of examples in the Git repository. Please note that this project is very young, and that APIs are not necessarily stable yet. I think, however, that it’s a much nicer way to build GTK+ applications using Haskell than the underlying APIs provided by the auto-generated bindings. Now, have fun building your own functional GTK+ applications! ## December 28, 2018 ### Oskar Wickström # Why I'm No Longer Taking Donations Haskell at Work, the screencast focused on Haskell in practice, is approaching its one year birthday. Today, I decided to stop taking donations through Patreon due to the negative stress I’ve been experiencing. ## The Beginning This journey started in January 2018. Having a wave of inspiration after watching some of Gary Bernhardt’s new videos, I decided to try making my own videos about practical Haskell programming. Not only producing high-quality content, but with high video and audio quality, was the goal. Haskell at Work was born, and the first video was surprisingly well-received by followers on Twitter. With the subsequent episodes being published in rapid succession, a follower base on YouTube grew quickly. A thousand or so followers might not be exceptional for a programming screencast channel on YouTube, but to me this was exciting and unexpected. To be honest, Haskell is not exactly a mainstream programming language. Early on, encouraged by some followers, and being eager to develop the concept, I decided to set up Patreon as a way of people to donate to Haskell at Work. Much like the follower count, the number of patrons and their monthly donations grew rapidly, beyond any hopes I had. ## Fatigue Kicks In The majority of screencasts were published between January and May. Then came the summer and my month-long vacation, in which I attended ZuriHac and spent three weeks in Bali with my wife and friends. Also, I had started getting side-tracked by my project to build a screencast video editor in Haskell. Working on Komposition also spawned the Haskell package gi-gtk-declarative, and my focus got swept away from screencasts. In all fairness, I’m not great at consistently doing one thing for an extended period. My creativity and energy comes in bursts, and it may not strike where and when I hope. Maybe this can be managed or controlled somehow, but I don’t know how. With the lower publishing pace over the summer, a vicious circle of anxiety and low productivity grew. I had thoughts about shutting down the Patreon back then, but decided to instead pause it for a few months. ## Regaining Energy By October, I had recovered some energy. I got very good feedback and lots of encouragement from people at Haskell eXchange, and decided to throw myself back into the game. I published one screencast in November, but something was still there nagging me. I felt pressure and guilt. That I had not delivered on the promise given. By this time, the Patreon donations had covered my recording equipment expenses, hosting costs over the year, and a few programming books I bought. The donations were still coming in, however, at around$160 per month, with me producing no obvious value for the patrons. The guilt was still there, even stronger than before.

I’m certain that this is all in my head. I do not blame any supporter for these feelings. You have all been great! With all the words of caution you hear about not reading the comments, having a YouTube channel filled with positive feedback, and almost exclusively thumbs-up ratings, I’m beyond thankful for the support I have received.

## Trying Something Else

After Christmas this year, I had planned to record and publish a new screencast. Various personal events got in the way, though, and I had very little time to spend on working with it, resulting in the same kind of stress. I took a step back and thought about it carefully, and I’ve realized that money is not a good driver for the free material and open-source code work that I do, and that it’s time for a change.

I want to make screencasts because I love doing it, and I will do so when I have time and energy.

From the remaining funds in my PayPal account, I have allocated enough to keep the domain name and hosting costs covered for another year, and I have donated the remaining amount (USD 450) to Haskell.org.

Please keep giving me feedback and suggestions for future episodes. Your ideas are great! I’m looking forward to making more Haskell at Work videos in the future, and I’m toying around with ideas on how to bring in guests, and possibly trying out new formats. Stay tuned, and thank you all for your support!

# Maybe

There are different approaches to the issue of not having a value to return. One idiom to deal with this in C++ is the use of boost::optional<T> or std::pair<bool, T>.
class boost::optional<T> //Discriminated-union wrapper for values.

Maybe is a polymorphic sum type with two constructors : Nothing or Just a.
Here's how Maybe is defined in Haskell.
  {- The Maybe type encapsulates an optional value. A value of type  Maybe a either contains a value of type a (represented as Just a), or  it is empty (represented as Nothing). Using Maybe is a good way to  deal with errors or exceptional cases without resorting to drastic  measures such as error.  The Maybe type is also a monad.  It is a simple kind of error monad, where all errors are  represented by Nothing. -}  data Maybe a = Nothing | Just a  {- The maybe function takes a default value, a function, and a Maybe  value. If the Maybe value is Nothing, the function returns the default  value. Otherwise, it applies the function to the value inside the Just  and returns the result. -}  maybe :: b -> (a -> b) -> Maybe a -> b  maybe n _ Nothing  = n  maybe _ f (Just x) = f x

I haven't tried to compile the following OCaml yet but I think it should be roughly OK.
 type 'a option = None | Some of 'a  ;;  let maybe n f a =    match a with      | None -> n      | Some x -> f x      ;;

Here's another variant on the Maybe monad this time in Felix. It is applied to the problem of "safe arithmetic" i.e. the usual integer arithmetic but with guards against under/overflow and division by zero.
  union success[T] =    | Success of T    | Failure of string    ;  fun str[T] (x:success[T]) =>    match x with      | Success ?t => "Success " + str(t)      | Failure ?s => "Failure " + s    endmatch    ;  typedef fun Fallible (t:TYPE) : TYPE => success[t] ;  instance Monad[Fallible]  {    fun bind[a, b] (x:Fallible a, f: a -> Fallible b) =>      match x with        | Success ?a => f a        | Failure[a] ?s => Failure[b] s      endmatch      ;    fun ret[a](x:a):Fallible a => Success x ;  }  //Safe arithmetic.  const INT_MAX:int requires Cxx_headers::cstdlib ;  const INT_MIN:int requires Cxx_headers::cstdlib ;  fun madd (x:int) (y:int) : success[int] =>    if x > 0 and y > (INT_MAX - x) then        Failure[int] "overflow"    else      Success (y + x)    endif    ;  fun msub (x:int) (y:int) : success[int] =>    if x > 0 and y < (INT_MIN + x) then      Failure[int] "underflow"    else      Success (y - x)    endif    ;  fun mmul (x:int) (y:int) : success[int] =>    if x != 0 and y > (INT_MAX / x) then      Failure[int] "overflow"    else      Success (y * x)    endif    ;  fun mdiv (x:int) (y:int) : success[int] =>      if (x == 0) then          Failure[int] "attempted division by zero"      else        Success (y / x)      endif      ;  //--  //  //Test.  open Monad[Fallible] ;  //Evalue some simple expressions.  val zero = ret 0 ;  val zero_over_one = bind ((Success 0), (mdiv 1)) ;  val undefined = bind ((Success 1),(mdiv 0)) ;  val two = bind((ret 1), (madd 1)) ;  val two_by_one_plus_one = bind (two , (mmul 2)) ;  println$"zero = " + str zero ; println$ "1 / 0 = " + str undefined ;  println$"0 / 1 = " + str zero_over_one ; println$ "1 + 1 = " + str two ;  println$"2 * (1 + 1) = " + str (bind (bind((ret 1), (madd 1)) , (mmul 2))) ; println$ "INT_MAX - 1 = " + str (bind ((ret INT_MAX), (msub 1))) ;  println$"INT_MAX + 1 = " + str (bind ((ret INT_MAX), (madd 1))) ; println$ "INT_MIN - 1 = " + str (bind ((ret INT_MIN), (msub 1))) ;  println$"INT_MIN + 1 = " + str (bind ((ret INT_MIN), (madd 1))) ; println$ "--" ;  //We do it again, this time using the "traditional" rshift-assign  //syntax.  syntax monad //Override the right shift assignment operator.  {    x[ssetunion_pri] := x[ssetunion_pri] ">>=" x[>ssetunion_pri] =># "(ast_apply ,_sr (bind (,_1 ,_3)))";  }  open syntax monad;  println$"zero = " + str (ret 0) ; println$ "1 / 0 = " + str (ret 1 >>= mdiv 0) ;  println$"0 / 1 = " + str (ret 0 >>= mdiv 1) ; println$ "1 + 1 = " + str (ret 1 >>= madd 1) ;  println$"2 * (1 + 1) = " + str (ret 1 >>= madd 1 >>= mmul 2) ; println$ "INT_MAX = " + str (INT_MAX) ;  println$"INT_MAX - 1 = " + str (ret INT_MAX >>= msub 1) ; println$ "INT_MAX + 1 = " + str (ret INT_MAX >>= madd 1) ;  println$"INT_MIN = " + str (INT_MIN) ; println$ "INT_MIN - 1 = " + str (ret INT_MIN >>= msub 1) ;  println$"INT_MIN + 1 = " + str (ret INT_MIN >>= madd 1) ; println$ "2 * (INT_MAX/2) = " + str (ret INT_MAX >>= mdiv 2 >>= mmul 2 >>= madd 1) ; //The last one since we know INT_MAX is odd and that division will truncate.  println$"2 * (INT_MAX/2 + 1) = " + str (ret INT_MAX >>= mdiv 2 >>= madd 1 >>= mmul 2) ; //-- That last block using the <<= syntax produces (in part) the following output (the last two print statments have been truncated away -- the very last one produces an expected overflow). ## November 04, 2013 ### Tim Docker # Cabal version consistency Thanks to some great work done over the google summer of code, the chart library has gained much new functionality over the last 6 months. A consequence of this is that it has gained plenty of dependencies on other software. Furthermore, where the library previously had 2 cabal files to build the system, it now has 4. It's important the the versioning of dependencies is consistent across these cabal files, but manually checking is tedious. As best I could tell there is not yet a tool to facilitate this. Hence, I spend a little time learning about the cabal API, and wrote a short script that: 1. reads several cabal files specified on the command line 2. merges these into one overall set of dependencies 3. displays the depencies in such a way that inconsistent version constrains are obvious Here's some example output: $ runghc ~/repos/merge-cabal-deps/mergeCabalDeps.hs find . -name '*.cabal'
Chart:
>=1.1 && <1.2 (Chart-cairo,Chart-diagrams,Chart-gtk,Chart-tests)
Chart-cairo:
>=1.1 && <1.2 (Chart-gtk,Chart-tests)
Chart-diagrams:
>=1.1 && <1.2 (Chart-tests)
Chart-gtk:
>=1.1 && <1.2 (Chart-tests)
SVGFonts:
>=1.4 && <1.5 (Chart-diagrams)
array:
-any (Chart,Chart-cairo,Chart-gtk,Chart-tests)
base:
>=3 && <5 (Chart,Chart-cairo,Chart-diagrams,Chart-gtk,Chart-tests)
blaze-svg:
>=0.3.3 (Chart-diagrams,Chart-tests)
bytestring:
>=0.9 && <1.0 (Chart-diagrams,Chart-tests)
cairo:
>=0.9.11 (Chart-cairo,Chart-gtk,Chart-tests)
colour:
>=2.2.0 (Chart-diagrams)
>=2.2.1 && <2.4 (Chart,Chart-cairo,Chart-gtk,Chart-tests)
containers:
>=0.4 && <0.6 (Chart-diagrams,Chart-tests)
data-default-class:
<0.1 (Chart,Chart-cairo,Chart-diagrams,Chart-tests)
diagrams-cairo:
>=0.7 && <0.8 (Chart-tests)
diagrams-core:
>=0.7 && <0.8 (Chart-diagrams,Chart-tests)
diagrams-lib:
>=0.7 && <0.8 (Chart-diagrams,Chart-tests)
...
...
r /\ s = And r s

As an example, we consider the intersection of two languages:

\begin{aligned} X &= \{ \rerestr{a}^n \rerestr{b}^n \rerestr{c}^m \mid n, m \in \mathbb{N} \} & Y &= \{ \rerestr{a}^m \rerestr{b}^n \rerestr{c}^n \mid n, m \in \mathbb{N} \} \end{aligned}

which is known to be not context-free:

L = X \cap Y = \{ \rerestr{a}^n \rerestr{b}^n \rerestr{c}^n \mid n \in \mathbb{N} \}

However, we can simply match with it:

\begin{reretrace} \reretraceline[]{\rerestr{aaabbbccc}}{\rereintersect{\rerestar{\rerelit{a}}(\rerefix{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}})}{(\rerefix{\rerevar{ab}}{\rerealt{\rereeps}{\rerelit{a}\rerevar{ab}\rerelit{b}}})\rerestar{\rerelit{c}}}} \reretraceline[]{\rerestr{aabbbccc}}{\rereletrecin{\rerevar{ab}}{\rerealt{\rereeps}{\rerelit{a}\rerevar{ab}\rerelit{b}}}{\rereintersect{\rerestar{\rerelit{a}}(\rerefix{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}})}{\rerevar{ab}\rerelit{b}\rerestar{\rerelit{c}}}}} \reretraceline[]{\rerestr{abbbccc}}{\begin{rerealignedlet}\rereletreceqn{\rerevar{ab}}{\rerealt{\rereeps}{\rerelit{a}\rerevar{ab}\rerelit{b}}}\rereleteqn{\rerevarsub{ab}{\rerestr{a}}}{\rerevar{ab}\rerelit{b}}\rereletbody{\rereintersect{\rerestar{\rerelit{a}}(\rerefix{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}})}{\rerevarsub{ab}{\rerestr{a}}\rerelit{b}\rerestar{\rerelit{c}}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{bbbccc}}{\begin{rerealignedlet}\rereletreceqn{\rerevar{ab}}{\rerealt{\rereeps}{\rerelit{a}\rerevar{ab}\rerelit{b}}}\rereleteqn{\rerevarsub{ab}{\rerestr{a}}}{\rerevar{ab}\rerelit{b}}\rereleteqn{\rerevarsub{ab}{\rerestr{aa}}}{\rerevarsub{ab}{\rerestr{a}}\rerelit{b}}\rereletbody{\rereintersect{\rerestar{\rerelit{a}}(\rerefix{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}})}{\rerevarsub{ab}{\rerestr{aa}}\rerelit{b}\rerestar{\rerelit{c}}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{bbccc}}{\rereletrecin{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}}{\rereintersect{\rerevar{bc}\rerelit{c}}{\rerelit{b}\rerelit{b}\rerestar{\rerelit{c}}}}} \reretraceline[]{\rerestr{bccc}}{\begin{rerealignedlet}\rereletreceqn{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}}\rereleteqn{\rerevarsub{bc}{\rerestr{b}}}{\rerevar{bc}\rerelit{c}}\rereletbody{\rereintersect{\rerevarsub{bc}{\rerestr{b}}\rerelit{c}}{\rerelit{b}\rerestar{\rerelit{c}}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{ccc}}{\begin{rerealignedlet}\rereletreceqn{\rerevar{bc}}{\rerealt{\rereeps}{\rerelit{b}\rerevar{bc}\rerelit{c}}}\rereleteqn{\rerevarsub{bc}{\rerestr{b}}}{\rerevar{bc}\rerelit{c}}\rereleteqn{\rerevarsub{bc}{\rerestr{bb}}}{\rerevarsub{bc}{\rerestr{b}}\rerelit{c}}\rereletbody{\rereintersect{\rerevarsub{bc}{\rerestr{bb}}\rerelit{c}}{\rerestar{\rerelit{c}}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{cc}}{\rereintersect{\rerelit{c}\rerelit{c}}{\rerestar{\rerelit{c}}}} \reretraceline[]{\rerestr{c}}{\rereintersect{\rerelit{c}}{\rerestar{\rerelit{c}}}} \reretraceline[]{\rereeps}{\rereeps} \end{reretrace}

This is of course cheating somewhat, as And / \cap occurs here only on the top-level, and not e.g. inside of Fix / \rereFIX . However, even then it wouldn’t pose problems for the algorithm, but it is difficult to come up with any meaningful examples. Also recall that we interpret \FIX as least fixed point, so for example, even though

\rerefix{\rerevar{x}}{\rereintersect{\rerevar{x}}{\rereeps}}

has \rereeps as a fixed point, we have \rerenull as another fixed point, and that is the least one. Therefore, the above expression works (and indeed is automatically simplified to) \rerenull .

However And / \cap adds expressive power to the language, so it cannot be omitted as in pure regular expressions (where it causes a combinatorial explosion of expression size, so it may not be a good idea there either).

There’s one clear problem with And however: languages defined using And cannot be easily generated. Assuming we can use the first branch of an intersection to generate the candidate, it must still also match the second branch. I don’t know whether the language inhabitation problem for this class of languages is decidable (for CFGs it is, but we’re now outside of CFGs). Consider the intersection of two simple regular expressions, strings of \rerestr{a} of odd and even length:

\exIX

Their intersection is empty, but it’s not structurally obvious. For example if we match on \rerestr{aaa} , the expression will stay in a single non-nullable state, but it won’t simplify to \rerenull :

\begin{reretrace} \reretraceline[]{\rerestr{aaa}}{\begin{rerealignedlet}\rereleteqn{\rerevar{odd}}{\rerelit{a}\rerestar{(\rerelit{a}\rerelit{a})}}\rereleteqn{\rerevar{even}}{\rerestar{(\rerelit{a}\rerelit{a})}}\rereletbody{\rereintersect{\rerevar{even}}{\rerevar{odd}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{aa}}{\begin{rerealignedlet}\rereleteqn{\rerevarsub{odd}{\rerestr{a}}}{\rerestar{(\rerelit{a}\rerelit{a})}}\rereleteqn{\rerevarsub{even}{\rerestr{a}}}{\rerelit{a}\rerevarsub{odd}{\rerestr{a}}}\rereletbody{\rereintersect{\rerevarsub{even}{\rerestr{a}}}{\rerevarsub{odd}{\rerestr{a}}}}\end{rerealignedlet}} \reretraceline[]{\rerestr{a}}{\begin{rerealignedlet}\rereleteqn{\rerevarsub{odd}{\rerestr{a}}}{\rerestar{(\rerelit{a}\rerelit{a})}}\rereleteqn{\rerevarsub{odd}{\rerestr{aa}}}{\rerelit{a}\rerevarsub{odd}{\rerestr{a}}}\rereletbody{\rereintersect{\rerevarsub{odd}{\rerestr{a}}}{\rerevarsub{odd}{\rerestr{aa}}}}\end{rerealignedlet}} \reretraceline[]{\rereeps}{\begin{rerealignedlet}\rereleteqn{\rerevarsub{odd}{\rerestr{a}}}{\rerestar{(\rerelit{a}\rerelit{a})}}\rereleteqn{\rerevarsub{odd}{\rerestr{aa}}}{\rerelit{a}\rerevarsub{odd}{\rerestr{a}}}\rereletbody{\rereintersect{\rerevarsub{odd}{\rerestr{aa}}}{\rerevarsub{odd}{\rerestr{a}}}}\end{rerealignedlet}} \end{reretrace}

### Conclusion

It was nice to combine known things in a new way, and the result is interesting.

We now know that we can add fixed points to regular expressions or recursive types to non-commutative intuitionistic linear logic. The systems are still well-behaved, but many problems become harder. As CFG equivalence is undecidable, so is term synthesis in NCILL with recursive types (as synthesizing a term would yield a proof of equivalence).

We can also use the recursive RE not only to match on strings, but also to generate them. Therefore we can use it to statistically determine grammar equivalence (which is not a new idea).

Finally, this is not only for fun. I’m trying to formalize the grammars of fields in .cabal files. The parsec parsers are the definition, but we now have more declarative definitions too and compare these two, using QuickCheck. Additionally we get nice-looking \text{\LaTeX} grammar definitions that are (hopefully) human-readable. If you ever wondered what the complete and precise syntax for version ranges in .cabal files is, here is what it looks like at the time of writing this post:

The notation is described in detail in the Cabal user manual, where you can also find more grammar definitions.

Code in the Cabal Parsec instances is accumulating history baggage, and is written to produce helpful error messages, not necessarily with clarity of the grammar in mind. However, we can compare it (and its companion Pretty instance) with its RE counterpart to find possible inconsistencies. Also, Cabal has a history of not handling whitespace well, either always requiring, completely forbidding, or allowing it where it shouldn’t be allowed. The RE-derived generator can be amended to produce slightly skewed strings, for example inserting or removing whitespace, to help identify and overcome such problems.

### References

[Bekic1984] Bekić, Hans: Definable operations in general algebras, and the theory of automata and flowcharts. In: Jones, C. B. (ed.): Programming languages and their definition: H. Bekič (1936–1982). Berlin, Heidelberg : Springer Berlin Heidelberg, 1984 — ISBN 978-3-540-38933-0, pp. 30–55. https://doi.org/10.1007/BFb0048939

[Might2011] Might, Matthew; Darais, David; Spiewak, Daniel: Parsing with derivatives: A functional pearl. In: Proceedings of the 16th ACM Sigplan International Conference on Functional Programming, ICFP ’11. New York, NY, USA : Association for Computing Machinery, 2011 — ISBN 9781450308656, pp. 189–195. https://doi.org/10.1145/2034773.2034801

[Owens2009] Owens, Scott; Reppy, John; Turon, Aaron: Regular-expression derivatives re-examined. In: Journal of Functional Programming vol. 19 (2). USA, Cambridge University Press (2009), pp. 173–190. https://doi.org/10.1017/S0956796808007090 https://www.ccs.neu.edu/home/turon/re-deriv.pdf

1. There is an implementation in the derp package, which uses Data.IORef and unsafePerformIO.↩︎

2. Using smart constructors in this approach, we obtain relatively small automata, but they are not minimal. To actually obtain minimal ones, kleene` can compare regular expressions for an equivalence, e.g. concluding that \rerestar{\rerelit{a}} and \rereconcat{\rerestar{\rerelit{a}}}{\rerestar{\rerelit{a}}} are in fact equivalent.↩︎

3. Miranda was first released in 1985, and in January 2020 also under BSD-2-Clause license. Now anyone can play with it. Lack of type classes makes the code a bit more explicit, but otherwise it doesn’t look much different.↩︎