Håkon Robbestad Gylterud — Articles

Applicative logic

2024-05-25T12:00:00Z

Note: You can find the functions below in the module Control.Applicative.Logic (GitHub, Hackage).

The following is an exploration of a few functions I found while writing various Haskell programs over the years. Their names collide with some standard function in Prelude, which is unfortunate, and while the new functions cannot be used as drop-in replacements of the prelude functions, they are morally generalisations. Also, note that the order I present my insights here are almost the exact opposite of the order in which I “discovered” them. I say “discovered” because I am presumably not the first one to discover these as they are very general. In fact, some of them are already in the standard library (albeit under a different name).

tl;dr: Many functions involving booleans can be generalised to involve (Alternative f, Monoid a) => f a instead.

A boolean is maybe true

We will start our exploration with a very inane observation. It is essentially the observation that 1+1=2, which every child discover some time before the age of five. As mentioned, this is the final “insight” I had, which tied all the pieces together.

Bool ≅ Maybe ()

There it is! The equality sign with the squiggle over it means “isomorphic” which is a fancy way of saying “is essentially the same as” which for Haskell types mean that there are translation functions back and forth which are mutual inverses. So, in theory, any place you use a Bool you can use a Maybe () value. Just replace True with Just () and False with Nothing.

Digression: “Well, actually…” Alright, you clever little imp! I know what you want to say. Haskell semantics is Complicated™. And there are in fact differences between Bool and Maybe (). For instance, Just undefined does not really have a counterpart in Bool. An “isomorphism” could map it to either undefined :: Bool or True :: Bool, but they are both in a sense taken. But if your program depends on the exact structure of non-total elements of Bool, you deserve to live in the purgatory you have created.

But why?

Bool is a fine type. Very useful. In fact, it gets special treatment in by the compiler. Only Bools can be used in if-expressions and guards. So, this is not a suggestion to replace Bool with Maybe () if your program works well with Bool. The purpose is rather to recognise that some of the things done to booleans can be done to other structures as well. And the core of this stems from how Maybe () consists of two parts: Maybe which is an Applicative, Alternative functor and () which is a (admittedly trivial) Monoid. We wil now take some of the well-known functions involving Bool and bring them to this level of generality. Then by replacing Maybe and () with other Applicative, Alternative functors and Monoids, these functions will find new use cases.

Disjunction

Let us start by talking about disjunction, usually conceived as (||) :: Bool -> Bool -> Bool. But there is a typeclass called Alternative with an operator (<|>) :: (Alternative f) => f a -> f a -> f a which works like disjunction when we apply it to Maybe (): We get Just () <|> _ = Just () (true or anything is true) and likewise _ <|> Just () = Just () and finally Nothing <|> Nothing = Nothing (False or false is false). But the operator has many uses. For lists it is simply concatenation, and the operator is essential when writing parsers. The disjunctive unit (i.e. false) is called empty :: (Alternative f) => f a.

This is well-trodden stuff. But I think it is nice to highlight. For instance, if you have something where you get a lot of Maybe-values, perhaps in a list, and you just want to pick the first just value, you can use or = foldr (<|>) empty to convert [Maybe a] -> Maybe a.

or :: (Foldable t, Alternative f) => t (f a) -> f a
or = foldr (<|>) empty

This is clearly a generalisation of or :: (Foldable t) => t Bool -> Bool, but it is also a generalisation of concat :: [[a]] -> [a]. In Control.Applicative you will find this under the name asum and it is very useful!

`any`

While disjunction is useful, the reason I often end up using or to flatten something of type t (f b) to f b is because I first had t a and a predicate a -> f b. So, let us combine those two steps into a single, beautiful function:

any :: (Alternative f, Foldable t) => (a -> f b) -> t a -> f b
any = ($ empty) . foldr . ((<|>) .)

A very simple usage of this function is to convert from any foldable structure to any alternative functor using any pure. For instance a x <- any pure (Map.lookup i m) in a do-block will lookup a value in a map and rewrap it into your current monad (as long as it is Alternative). In fact any pure is a general conversion function which can convert from any of these:

Set a
Map k a
[a]
Maybe a
Either e a
(w,a)

to any of these:

IO a
[a]
Maybe a
Either e a (for e a Monoid)
STM a
Parser a (For some reasonable Parser monad)

Apropos the last entry in that list, any string ["foo","bar","bat"] is a parser which matches any of the words in the list. Over in ConcurrencyLand, any readTChan [chan0,chan1,chan2] will read the first value arriving in any of the three channels.

ghci> import Control.Applicative.Logic (any)
ghci> import Control.Monad (forever)
ghci> import Control.Concurrent (forkIO)
ghci> import Control.Concurrent.STM
ghci> import Control.Concurrent.STM.TChan

ghci> -- Create the channels
ghci> chan0 <- newTChanIO :: IO (TChan String)
ghci> chan1 <- newTChanIO :: IO (TChan String)
ghci> chan2 <- newTChanIO :: IO (TChan String)
ghci>
ghci> -- Create a thread reading from any chan:
ghci> forkIO $ forever
             $ atomically (readTChan `any` [chan0,chan1,chan2])
                 >>= putStrLn
ThreadId 689

ghci> -- Now we can write to any of the channels:
ghci> atomically $ writeTChan chan1 "Foo"
Foo
ghci> atomically $ writeTChan chan0 "Bar"
Bar
ghci> atomically $ writeTChan chan2 "Baz"
Baz

The moral is that you can use this generalised any in many places where the word any would fall natural to use informally.

Conjunction

Having gone on and on about disjuntion, I should talk about conjunction. There might some wiggle room for what notion of conjunction best fits, but my experience from a lot of examples suggest that the following is practical:

(&&) :: (Applicative f, Monoid a)
     => f a -> f a -> f a
(&&) = liftA2 (<>)

Why Monoid? The idea is that && combines two generalised truth values. The a argument to f represents evidence of truth (say, a set of solutions, or results from a search or something). Thus, if a conjunction is true we must take into account the evidence from both sides. One option would be to instead use liftA2 (,) :: f a -> f b -> f (a,b), in a kind I-know-Curry–Howard way. But that will not really generalise to a function similar to any, where we collect evidence from a whole structure of elements. Thus, the Monoid alternative seems more useful in practice.

You can probably imagine uses for && yourself, so let us get off the ground by defining and:

and :: (Foldable t, Applicative f, Monoid a)
    => t (f a) -> f a
and = foldr (&&) (pure mempty)

As you can see pure mempty is the new True, otherwise only the type signature changed from the Bool definition. But what can we do with it? Let us start with a combinatorics example: Say we want to generate all sentences of the form “Harry/Sue loves/hates kale/honey”. Here is a solution:

ghci> all putStrLn $ and [["Harry","Sue"],  [" "]
                         ,["loves","hates"],[" "]
                         ,["kale","honey"], ["."]]
Harry loves kale.
Harry loves honey.
Harry hates kale.
Harry hates honey.
Sue loves kale.
Sue loves honey.
Sue hates kale.
Sue hates honey.

Alright, I could not resist sneaking in an early “all”s in that. Stay tuned for it the next subsection, but ignore it for the moment, and let us focus on “and”. This example is standard list monad stuff, but the and function lets us easily generate combinations from lists of alternatives.

`all`

We have already seen one use of the generalised all, namely applying an IO function to every element of a list: all print [1..10]. But there already exists plenty of functions doing that. Can we do something else? Just pick your faviourite Applicative and start experimenting. Picking STM for instance, we can wait until a moment when all channels have something ready and get that using all ((singleton <$>) . readTChan) [chan0,chan1,chan2] :: STM [a]. Or for IO one can all readFile :: [FilePath] -> IO String to read list of files into a single string.

all :: (Applicative f, Monoid b, Foldable t)
    => (a -> f b) -> t a -> f b
all = ($ pure mempty) . foldr . ((&&) .)

Notice that guard :: (Alternative f) => Bool -> f () converts a standard bool to an applicative truth value. Hence all guard :: (Alternative f, Foldable t) => t Bool -> f () can be used where one would use and normally. For instance, here is a function which checks if a list is sorted:

ascending :: (Alternative f, Ord b) => [b] -> f ()
ascending l = all guard $ zipWith (<=) l (tail l)

Extended example

Here is a simple example where you can see a few usages of the applicative logic functions in context. It is simply a game of tic-tac-toe, but it demonstrates a few usages and the general intuition of any, or, all, and and convert.

import Control.Monad (guard)
import Control.Applicative
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Functor (($>))

import System.Random (randomRIO)

import Prelude hiding (any, all, or)
import Control.Applicative.Logic (any, all, or, convert)

-- Game data
data Mark = X | O
  deriving (Eq,Show)

type Position = (Integer,Integer)

type Board = Map Position Mark

isValidMove :: Board -> Position -> Bool
isValidMove board (x,y) =  0 <= x && x <= 2
                        && 0 <= y && y <= 2
                        && null (Map.lookup (x,y) board)

-- All positions on the board
allPositions :: [Position]
allPositions = liftA2 (,) [0..2] [0..2]

-- Make a move on the board
move :: Board -> Position -> Mark -> Maybe Board
move board pos m = guard (isValidMove board pos)
                $> Map.insert pos m board

-- Verify who has won
won :: Board -> Maybe Mark
won board = any filled streaks where
    -- Generate all streaks
    streaks = do
          x <- allPositions
          y <- filter (x<) allPositions
          z <- filter (y<) allPositions
          check [x,y,z]
          pure [x,y,z]
    -- Check that three positions form a streak
    check l = do
              guard (mod (sum (fst <$> l)) 3 == 0)
              guard (mod (sum (snd <$> l)) 3 == 0)
              ascending (snd <$> l) <|> decending (snd <$> l)
    -- Verify that a player has filled a streak
    filled streak = do
        marks <- traverse (`Map.lookup` board) streak
        m <- any pure marks
        all (guard . (==m)) marks
        pure m
    -- Utility functions
    ascending l = all guard $ zipWith (<=) l (tail l)
    decending l = all guard $ zipWith (>=) l (tail l)

-- Game playing logic

main :: IO ()
main = gameLoop X (Map.empty :: Board)

gameLoop :: Mark -> Board -> IO ()
gameLoop currentMark board = do
    putStrLn "Current board:"
    printBoard board
    or
      [ do mark <- convert (won board)
           putStrLn $ "Player " ++ show mark ++ " wins!"
      , guard (Map.size board == 9) *> putStrLn "It's a draw!"
      , guard (currentMark == X)    *> moveIO board X userMove
                                   >>= gameLoop O
      , guard (currentMark == O)    *> moveIO board O computerMove
                                   >>= gameLoop X ]

moveIO :: Board -> Mark -> (Board -> IO Position) -> IO Board
moveIO board mark play = do
   pos <- play board
   convert (move board pos mark)
       <|> (do putStrLn "Position not in range!"
               moveIO board mark play)

userMove :: Board -> IO Position
userMove board = do
    putStrLn "Enter your move (row column):"
    input <- getLine
    case words input >>= reads :: [(Integer,String)] of
       [(x,""),(y,"")] -> pure (x,y)
       _ -> do
              putStrLn "Invalid input, please use the format 'row column'."
              userMove board

randomValidMove :: Board -> IO Position
randomValidMove board = do
    let validMoves = filter (isValidMove board) allPositions
    idx <- randomRIO (0, length validMoves - 1)
    pure $ validMoves !! idx

computerMove :: Board -> IO Position
computerMove board = do
    pos <- randomValidMove board
    putStrLn $ "Computer places " ++ show O ++ " at " ++ show pos
    pure pos

printBoard :: Board -> IO ()
printBoard board
  = all putStrLn [ unwords [ maybe "." show
                                   $ Map.lookup (x,y) board
                   | y <- [0..2]]
                   | x <- [0..2]]

Highlights of the extended example

Let me highlight a few usages of applicative logical function in the above code. The first and most striking part is the check-if-board-is-won function:

won :: Board -> Maybe Mark
won board = any filled streaks

This uses Maybe Mark as a proof-relevant truth value for any. Instead of just True when the board is won we get Just X or Just O, depending on which player won. And the code simply says that the board is won if there are any filled streaks (of three board positions in a row).

filled :: [Position] -> Maybe Mark
filled streak = do
    marks <- traverse (`Map.lookup` board) streak
    m <- any pure marks
    all (guard . (==m)) marks
    pure m

The filled function uses both any and and to check that a list of board possitions are filled with the same mark. First it uses traverse to check that all the positions of streak are filled with something on the current boar and collects them in a list. Then m <- any pure marks picks out the first mark of the streak and all (guard . (==m)) marks verifies that the remaining marks of the streak are all the same.

While it does not use any of the applicative logic functions directly, the code for generating all streaks is a nice example of thinking of applicative values as propositions:

streaks :: [[Position]]
streaks = do
        x <- allPositions
        y <- filter (x<) allPositions
        z <- filter (y<) allPositions
        check [x,y,z]
        pure [x,y,z]

This all happens in do-syntax for lists, and the first three lines are self-explanatory. The check function however is a predicate which checks if three positions form a streak (are in a row on the board). It is converted from Bool with heavy usage of guards:

check l = do
            guard (mod (sum (fst <$> l)) 3 == 0)
            guard (mod (sum (snd <$> l)) 3 == 0)
            ascending (snd <$> l) <|> decending (snd <$> l)

Over in the IO part of the program, there is an interesting pattern:

gameLoop :: Mark -> Board -> IO ()
gameLoop currentMark board = do
    putStrLn "Current board:"
    printBoard board
    or
      [ do mark <- convert (won board)
           putStrLn $ "Player " ++ show mark ++ " wins!"
      , guard (Map.size board == 9) *> putStrLn "It's a draw!"
      , guard (currentMark == X)    *> moveIO board X userMove
                                   >>= gameLoop O
      , guard (currentMark == O)    *> moveIO board O computerMove
                                   >>= gameLoop X ]

I am not sure this is actually a sane way do conditionals in IO, but it works. The or [⋯] part is interesting because it attempts to execute the elements of the list in order and stops once one of the steps succeeds. So, for instance:

do mark <- convert (won board)
   putStrLn $ "Player " ++ show mark ++ " wins!"

Will fail if no player has won yet. The Applicative.Logic.convert function converts the Maybe Mark into IO Mark, throwing an exception on Nothing, so the putStrLn part will only run if someone actually won. Otherwise, it will continue with checking for a draw, or letting one of the players move.

The move :: Board -> Position -> Mark -> Maybe Board function integrates the check of validity with the updating of the board. In the IO part again we use convert (aka any pure) to get an IO value of the updated board, and use disjunction for error handling:

moveIO :: Board -> Mark -> (Board -> IO Position) -> IO Board
moveIO board mark play = do
   pos <- play board
   convert (move board pos mark)
       <|> (do putStrLn "Position not in range!"
               moveIO board mark play)

The final little bit of niceness is to use all instead of mapM_ to print each row of the board on a separate line:

printBoard :: Board -> IO ()
printBoard board
  = all putStrLn [ unwords [ maybe "." show
                                   $ Map.lookup (x,y) board
                   | y <- [0..2]]
                   | x <- [0..2]]

Setting up a basic website

2022-05-17T12:00:00Z

There are lot of different ways to make a website. You can write your own HTML code (the code your web-browser reads when it draws a webpage), use a WYSIWYG editor or install Wordpress… This guide is for those who wish to focus on the textual content of their site, and keep the number of distractions down. The following are the key points, each of which might warrant further explainations.

Keep the barrier for writing and editing the webpages low.
Do the editing on a local machine.
Make it easy to deploy changes to the server.

Now let us discuss the technical tools I have chosen to implement these key points. They are each in them selves quite simple, but might take a bit of effort to get comfortable with¹. Here is the list.

Write the content in Markdown.
Use a version control system such as darcs.
Automate your operations using mk or make.
Mount the server file system locally using sshfs.

We will go through all these. At the end there is a worked example, and a discussion. Before you get started, you need some hosting for your web page. If you can have a machine running at all times, I recommend hosting your own web site, but any hosting which allows you to upload simple html files will work for this tutorial.

Markdown and Pandoc

Writing your own HTML code need not be very stressful, and gives complete flexibility — but with this flexibility comes distractions. If you are a perfectionist you easily get caught up in the struggle of making your page look perfect on every browser. HTML is growing bigger and bigger with new standards popping up every year. Markdown however lets you write your page in a text file, and just slightly hint at the markup — using newlines to separate paragraphs, and #s to mark headings, for example. After writing the text you can convert the file to HTML and put it online.

You can use any text editor to write your markdown files. I recommend any text editor which allows you to write without too many distractions. This page was written in Acme from Plan9Port on Linux.

Pandoc is the document format swiss-army knife. It converts text documents between a lot of formats, including Markdown and HTML. This document is written in Markdown, but you are reading it as a HTML page. The following command was used to convert it:

pandoc --standalone --smart -T '' -f markdown -t html5 --css /markdown.css\
 -o tutorials/basic-website.html tutorials/basic-website

The --standalone gives the html file a header, so that it can stand on its own. The --smart tag corrects some typographical quirks. Finally the -T '' gives the page an automatic title header. As you can see from the command, I have specified a custom css file to be used. The CSS file I use for Markdown can be found here.

Darcs

A version control system is a program which keeps track of a collection of files and revisions there of. Typically all versions previous versions are preserved, so that you can go back to an earlier revision, or keep update several, independent versions of your files².

Use a version contol system. I recomend darcs, but there are other alternatives. A quick introduction to darcs is found here.

For the purpose of making a web-page the advantage of using a version control system is that one can keep track of all revisions one made. Also, being able to have separate branches means that you can work on bigger changes while at the same time keeping the old version up to date. It also allows undoing changes more easily and cleanly.

One can of course setup a darcs repository where the site is deployed to. This has the advantage of being able to use “darcs push” to update the web-page. There are a couple of reasons why I do not do it this way. The most basic one is that since it is really just the generated HTML we need to put on the server and revision control is only needed for the Markdown-files, we might as well just copy the HTML-files once they are generated.

mk

Once you have started writing your website you might get tired of typing that long pandoc command every time. Also, you might grow tired of copying the HTML files to the server every time you made a minor edit. This is when writing a mkfile (or makefile) is useful. A mkfile contains the commands needed to build a given set of files. Once the mkfile is written, you call on the command mk to build them.

I have written a small mkfile which takes care of these things. It uses the Plan 9 from User Space userland (rc and mk to be precise), so be sure to have those installed.

It depends on having a file called deployment-index which lists all the HTML- and CSS files and all directories you want to deploy. Just write a list of the files and make sure that directories end with /.

Here is my mkfile:

MKSHELL=$PLAN9/bin/rc

# This names a file which we read as index.
index='deployment-index'

# Generate HTML-files from markdown

%.html: %
   pandoc --standalone --smart -T '' -f markdown\
    -t html5 --css /markdown.css -o $stem.html $stem

# Virtual targets

all:QV: `{grep -v '/$' $index}
    

# Deploy all files in $index to $destination

deploy:QV: `{grep -v '/$' $index}
  for (f in `{grep '/$' $index})
    mkdir $destination/$f >[2] /dev/null \
     || echo $destination/$f exists. Omitting .
  for(i in `{grep -v '/$' $index})
    cp -v $i $destination/$i

Then the following command:

mk deploy 'destination=/path/to/deployed-site'

will deploy all the files in deployment-index to /path/to/deployed-site.

sshfs

When deploying the site can be useful to mount the server using sshfs.

rsync

Alternatively, you can use rsync(1) to copy the files to a remote server. The following mk rule assumes you have set the host and destination enviromentvariables:


rsyncdeploy:QV: all
  time -f 'Total deployment time: %e seconds' rc -c '
    build=`{mktemp}
    destination=$build mk deploy
    echo ''Synchronising remote copy.''
    rsync -rcvz $build/ $host:$destination
    echo ''Removing local copy.''
    rm -r $build'

A word on backup

Keep backups of your files! Use an online service or keep your own backup disks. If you loose the markdown files, you can convert the HTML files back to markdown, but you will loose earlier revisions, and work-in-process. If the host of your web-site has some space for you which do not end up on the internet, it might be a good place to keep the backup.

Having our files managed by Darcs makes it easy to push the current state to a backup — so there are no excuses for not making frequent backups.

Extra credits

Test suite

One thing you can do for extra credits is to add a test suite to your web-page. We do not have any «dynamic content» or fancy programming on the web page, so a test suite might sound unnessesairy. However, you could make a test suite looking for anti-patterns in your writing. Or maybe you want to spell check your writing before publishing?

As a useful example, the following mk rule will look for dead links:

links-check:QV: `{grep -v '/$' $index | grep '\.html$'}
  if (~ $base '')
     base=`{pwd}
# Get the absolute path for base
  wd=`{pwd}
  cd $base
  base=`{pwd}
  cd $wd
# Get the search and replace string for absolute server links
  ss='s/^\//'`{echo $base | ssam -e 's/\//\\\//g'}^'\//g'
# Iterate through html files and check remote links with curl
  for(i in `{grep -v '/$' $index | grep '\.html$'}) {
     cd $base
     newdir=`{echo $i | ssam -e 'x/[^\/]*$/ d'}
     if (! ~ $newdir '')
        cd $newdir
     for (u in `{ssam -e 'y/href\=\"[^"]*\"/ d' < $base/$i \
               | ssam -e 'x/href=/ d' \
	       | ssam -e 'x/\"[^\"]*\"/ y/[^\"]*/ c/\n/' \
	       | grep -v '^$' | grep -v '^#' | grep -o '^[^#]*' \
	       | ssam -e $ss } ) {
        if (! test -e $u)
           if (! curl -k -s -r 0-255 -o /dev/null $u) {
              echo $u is invalid in $i
              cd $base
              exit 1}
         }
     cd $base }

Darcs can be made aware that we have tests we want to perform by running the following command:

 % darcs setpref test 'mk links-check'

Exercise: Add a test which checks spelling of documents.

Generating other formats

Pandoc can generate many formats. One of the formats it generates is Latex, a powerful document markup language, from which we can generate PDFs. Assuming you have a LaTeX distribution installed, extending the mkfile with the following lines will add PDF-targets.

# Generate PDF-files via tex files.

TEXINPUTS=.:`{grep '/$' $index \
  | ssam -e 'x/\n/ c/:/' }

%.tex: %
   pandoc --standalone --smart -T '' -f markdown\
    -t latex -o $stem.tex $stem

%.pdf: %.tex
   pdflatex -output-directory `{echo $stem |\
    ssam 'x/\/[^\/]*$/ d'} $stem.tex

Just mk your-file.pdf and a PDF-file will be constructed from the your-file markdown. Remember to add the pdf to the deployment index!

You can read this tutorial as a PDF here — it was generated in the way outlined above.

Exercise: Read the pandoc documentation, find another useful format to convert a webpage to and add an mk-target for it.

Disussion

This above technique will produce a website which might strike the reader as a primitive web page — limited in its technical abilities compared to the modern interactive ideals in which every page at least has a comment section. This guide is to be to taken as the tiniest grain of sand, put on the other side of the scale — my tiny contribution to the counter-weight of this ideal.

Why do I believe such a counter-weight is needed? It is not because I think that user-interaction is not valuable. If webpages can facilitate fruitful discussions between people who would otherwise remain unconfronted with each other it contributes something valuable to the world. However, contributions by the user is always at the mercy of the administrator and the moderator. What can appear as a free discussion is in reality only as free as the moderator is benevolent. In the best case the moderator is the same as the website author, whose agenda is transparent — at the worst it is a corporation or the state. The worst case seems by far the most common, as many sites, such as blogs, Facebook pages and Twitter accounts, are hosted as ready-made services, where the author is merely a slightly priviledged user.

A simple website, such as one constructed in the manner described here, can even be hosted on an outdated home computer. To censor it would involve blocking Internet access or physically confiscate the computer, an effort much bigger than the button-click of a moderator of Facebook. Not to mention that it can be restored by simply moving to a new host, given that a backup is availble.

A page without a «like counter» is also not susceptible to the tyranny of the local majority we see so many places. On say, Reddit, your «contribution» is immediately evaluated by other users. The resulting grade colours the way the reader receives your words — the resulting fragmentation into cliques clearly expected by the founders by the facility of «sub-reddits».

The central tension of a dynamic discussion forum is the need for moderators (lest the site becomes infected by spam) and the need for freedom from moderators (lest the site becomes infected by moderator power games and censorship).

How then to facilitate discussion, if not by atomated discussion services? My guess is that a partial solution to this question lies in the realisation that what is called a «static webpage» (for lack of «dynamic» content), need not be static in the real sense of the word, as it can be changed by the owner — and new content and pages may be added. If making your own site is simple, each can have his own to publish his arguments to a discussion. Links between sites enables the reader to pass from one side of the argument to the other.

I work a lot with the command line, which for many people seems like an odd instrument from a forgotten past, but it has the advantage that I can completely write down my actions, which would be impossible if I used some graphical application.↩︎
Or, rather, several dependent versions of your files — since darcs makes it easy to selectively import changes from one version to another — which is far more useful.↩︎

Moog Mother-32

2019-04-01T12:00:00Z

While I was in Stockholm giving a talk before Easter, I bought my first analogue synthesiser: a Moog Mother-32.

Until recently I thought I would save up a bit (eh, a lot) more money and buy a fully modular synth, but then just before going to Stockholm I decided to bet on a semi-modular instead. Thus, I wanted to write down my initial conclusions about that decision after playing with thing for a few days.

What is it?

The Mother-32 is a semi-modular analogue syntesiser. “A what?”, you say. Well, in short (skip this if you know, or do not care, how a synthesiser works):

Synthesiser – it synthesises sound. It generates electric signals which you can send to speakers (or head phones), so that they will make sound. The process of generating is by feeding signals through various components of the synthesiser. Each component has various parameters which can be controlled to generate different sounds. Here are some components of the Mother-32:
- Oscillator: Generates signal (square or saw-tooth waves) with varying frequency. Since the oscillator is controlled by an electic signal, it is called a voltage-controlled oscillator (VCO).
- Filter: Dampens the signal’s content of frequencies above or below a certain cut-off frequency.
- Envelope generator: Generates the volume shape of individual notes. A note does not have constant volume, but rather starts, low goes up to a high, then descends again. The steepness of the going-up and the going-down are called attack and decay.
- Low-frequency oscillator (LFO): A second oscillator with a lower frequency range. Can be used to modulate the parameters of other components, or as a second sound source.
Analogue synthesiser – the sound is transmitted as an analogue signal (not digital) through the components. In particular the oscillator is an analogue electronic component.
Semi-modular synthesiser – While some of the components are hard-wired to each other, there are patch points (mono mini-jack connectors) where the user can connect inputs to outputs in new ways. The Mother has thirty-two patch points (visible on the left side of the picture above).

Does it sound good?

Yes! The sound is really above expectations. While it might look like a cute little machine it produces really powerful sounds. Especially is has some beautiful bass sounds easily available by just playing with the knobs. And you find easily recognisable transitions, such as slowly opening the filter, by fiddling the knobs.

Ofcourse it matters what kind of speakers or head-set you connect it to. The first time I connected it to my stereo I was awestruck by the awesomeness. Also, if your stereo has an equaliser or even just a low-pass filter (labeled “bass” in many cases), it can be used as an extension of the instrument.

A straight forward patch sounds can reasonable on all eight octaves, but I find that most complicated configurations have a range about three to five octaves where they sound pleasant. If you go outside that range some of the musicality is lost.

Is it fun?

My biggest fear before buying the Mother-32 was that it would be no fun. Before this I have been playing with software modular synth, and usually my patches begin with putting up three different VCOs with a quantiser each and start feeding them signals from an array of at least four LFOs. So I was afraid that I would just not be able to produce anything interesting on this single VCO single LFO thingie.

However, the Mother proved my fears unfounded, I have been having a blast playing it so far. The limitations are definitely there , but there are both less and more possibilities than I imagined. And the result is that I am having a lot of fun exploring the space of sounds on the Mother.

First of all, there are actually four sound sources: the VCO, the noise generator, the LFO and the self-resonating filter. But there is this interesting trade-off between using more sound sources and constraining the choices you have. For instance, to play the filter you regulate frequency through the cut-off – but this constrains your ability to modulate the filter for other purposes. Similarily, if you use the LFO as a sound source, you have limited ability to use it to modulate the VCO.

Secondly, I find that there is a lot of fun to be had on each patch. For each patch, there are many ways to play it. You can play on the keyboard, or fire up a simple sequence, or try to generate something. What I tend to do is to let the sequence contain only beat info, and improvise melodies on top of the beat. Then I find some cool transitions and put together piece from that.

Some fun things I have tried with the patching, thus far:

Using the noise generator as a snare-drum, controlled by the accent on the sequencer. I think this came from the manual. I found that routing the accent through the mult to both cut-off and mix CV gave the best result.
Using the random-on-step mode to control the LFO-frequency. Depending on what is modulated by the LFO this introduces some funky randomness to the playing.
Using the LFO as a tempo clock for more variable tempo.
Switch the VCF modulation polarity and turn up the modulation so that the filter becomes like an inverted VCA, with attack and decay switching roles.

How modular is it?

So, from my perspective of wanting to get into hardware modular synths, where is the Mother-32? Is it a true modular or is it just a synth? I will say it is 40–60. Fourty percent of modular and sixty percent of a synth. However, to expand it I am definitely getting it some modular friends.

YouTube self-defence

2019-03-21T12:00:00Z

YouTube is Google’s¹ huge video streaming site. It has a large number of creators who upload their content there². Some video content is good, most of it is bad – and some of it directly harmful. Google is intent upon steering YouTube viewers³ to bad and harmful content. Therefore I have composed a list of defence strategies for YouTube viewers.

Blocking ads

The most obvious attack vector on YouTube is ads trying to manipulate you while you are watching the good content.

The most reliable way to block ads right now is to use Firefox with the uBlock Origin plugin (which is also available for Android and other platforms).

Hiding suggestions

The next attack vector is located on the right hand side of the screen:

In addition to taking up space which could be used for the video, this space is often filled with bad video suggestions.

First, install uBlock Origin.

The feature of uBlock Origin we are going to use can actually, be used for blocking parts of any page, and is a useful way to get rid of clutter on pages you visit often.

Right click on the white space close to the suggestions:

Select the uBlock origin block option

Check that the red area covers the suggestion section.

Currently this page-element is called ###secondary. You can use the mouse to select the correct region if you right-clicked in the wrong place.

Click Create to create the filter, removing the suggestions.

While you are at it, you could create another filter to block the comment section YouTube.

Downloading YouTube videos

Sometimes the best way to protect yourself is to avoid the fight entirely. There are tools available which will allow you to download a video from YouTube, without visiting the site yourself.

If you are comfortable in a command line, the youtube-dl is straight forward to use:

youtube-dl <link-to-video>

Actually, youtube-dl will download videos and music from a lot of different sites – not just YouTube!

Blocking auto-play

One of the ways YouTube controls what you watch is by automatically playing a new video just after the one you were watching finished. As a user you have no control over what video YouTube choses for you to see next. There is a button to disable auto-playing, but it is completely under YouTube’s control. In order to take back control, you can disable autoplaying video content.

Firefox allows you to change your autoplay settings by going to the special page about:config.

In recent versions, the main option is called media.autoplay.default and can have one of three values (See table below).

To block autoplay completely, set the value to 1.

`media.autoplay.default` value	Effect
Value: 0	Autoplay allowed.
Value: 1	Autoplay blocked.
Value: 2	Prompt the user.

There are more option related to autoplay, such as media.autoplay.allow-muted, and I wish it was easier to find their documentation from Firefox’s GUI. But usually, a bit of searching will give a hint.

Surf in a private window

If you are logged-in with a Google Account while watching YouTube, Google will remember what you have been watching and use this information for whatever it wants. Google has privacy options, but they are completely under Google’s control and therefore we cannot trust them.

Even if you do not have a Google Account, Youtube contains other tracking mechanisms which allow them to collect data about your viewing.

Therefore, always open YouTube in a private window.⁴ You should also be using tracker protecting software such as Privacy Badger.

Channel RSS feeds

Feeds (RSS or Atom) are way to get updates on a particular site. There are a lot of different RSS readers to be found⁵, for instance as Firefox plugins. If you use a feed reader, you can get updates from the channels you are interested directly in the FeedReader. The advantage is that you do not need a Google Account to read the feed.

Currently, you can get a feed URL for a channel in YouTube, in the following way:

Take the address of the channel.
- Example: https://www.youtube.com/channel/UCzLl8NF-hiP2HMq5dL2NQOQ
Copy the code at the end (after channel/).
- Example: UCzLl8NF-hiP2HMq5dL2NQOQ
Paste it at the end of this address: https://www.youtube.com/feeds/videos.xml?channel_id=
- Example: https://www.youtube.com/feeds/videos.xml?channel_id=UCzLl8NF-hiP2HMq5dL2NQOQ

Now you have a feed address which you can give you any RSS feed-reader, to receive updates when the channel releases new videos.

Some feed readers will do this conversion for you automatically if you give them the channel url.

Google did not create YouTube, but bought it in 2006, after it became popular.↩︎
If you are creating a video which you want to release upon the public, consider putting it somewhere more friendly to your viewers.↩︎
Your children included!↩︎
I have actually just turned off all history and stored data in Firefox, except for bookmarks. I aggressively bookmark and tag pages I visit, so that I still get a useful auto-completion in the address bar on stuff I have visited before.↩︎
Personally, I use newsboat, because I can then have it running in tmux on my server.↩︎

The anti-pattern game

2019-03-04T12:00:00Z

Here is a small game I though of when taking a course on modal logic. It is a bit too tedious to be played by humans, but I had great fun finding a winning stategy for it – and there are still simple questions about this game I cannot answer.

The rules

The anti-pattern game is a two-player game. It is played using black and white pebbles (like Go). These pebbles are placed in sequence on a line. On their turn the player has a simple choice: to continue the sequence with a white or a black pebble.

A player looses if they put down a pebble such that the sequence contains a pattern. A pattern is a sequence of pebbles repeated three times in a row.

A player wins if the other player looses.

Example

Here is a simlpe game won by player 1:

● ● ○ ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ○ ● ● ○ ○ ● ● ○ ○ ●
1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2 1 2

Player two lost because after their final turn, the sequence ended with the pattern: ● ○ ○ ● repeated trice.

Player two could have chosen to play ○ instead on the final turn, but that would also be a loosing move since then ○ would have been repeated trice. So if player two could have won, it must have changed its course several moves ago.

A winning strategy `– READY PLAYER 1`

The obvious question about any such two-player game is weather any player has a winning strategy. Often this can be determined by a finiteness condition, but here we could at least imagine that the game could go on to generate an infinitely long sequence.

To solve this question I wrote a short Haskell program which does a brute force search to find a winning strategy. Actually, the Haskell program wasn’t that short – because I wanted to apply modal logic to formulate the winning strategy condition and had to make appropriate definitions.

As it turns out, there is a winning strategy for player 1, and they can win the game inn less than twenty-two moves. The Haskell program finds the solution represented as a finite tree, which decides the moves of player 1 given any possible move of player 2.

Generalisations

Even though the game is solved, there are more questions we could pose if we make small adjustments to the game. Some of these questions I do not yet know the answer to.

Cooperating players

This question is simple to formulate: If the palyers were cooperating, could the game go on for ever? Put more precisely:

Is there an infinite binary sequence where no contigous subsequence is of the form σσσ for some sequence σ of non-zero length?

First off, it is clear that this game can continue for a long time. Here is a game with a thousand played moves:

● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ●
○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ○ ○ ● ● ○ ● ● ○
● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ●
● ○ ● ● ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○
○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ○
● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ●
○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○
● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○
● ● ○ ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ●
● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ○ ● ●
○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ●
○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○
● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○
● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ●
● ○ ● ● ○ ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ●
○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ○
● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ●
○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○
● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○
● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ●
● ○ ● ○ ● ● ○ ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○
● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ●
○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○
● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ○ ● ● ○ ● ● ○ ● ○ ●
● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ●
● ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ●
○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ○ ● ● ○
● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ●
○ ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○
● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ○ ● ● ○ ●
● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ●
○ ● ● ○ ● ● ○ ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ●
○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○
● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ●
● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ○ ● ● ○ ● ● ○
○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ●
● ○ ● ● ○ ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ●
○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○
○ ● ● ○ ● ● ○ ● ○ ● ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ●
● ○ ● ● ○ ○ ● ● ○ ● ● ○ ● ○ ● ● ○ ○ ● ● ○ ● ● ○ ●

At first sight this might seem disorderly, but there is a lot of repetition here:

The sequence of the first three pebbles ● ● ○ covers most of the game:
- Image
The entire first line (25 pebbles) occurs several times (even at the 25 character line offset):
- Image

The fact that ● ● ○ is so prominent in this example, suggest a way to generate an infinite game sequence:

data Colour = Black | White
 deriving (Eq, Ord, Show)

instance Show Colour where
  show Black = "●"
  show White = "○"

generate :: [Colour] -> [Colour]
generate p = [Black,Black,White]
  ++ (case p of
       (Black : cs) -> White : generate cs
       (White : cs) -> [Black,White] ++ generate cs )

stream :: [Colour]
stream = generate stream

This makes stream an inductively defined stream of pebbles, which makes up an infinitely long game. An interesting question is then: Can player 1 force the game to go on idefinitely (assuming player 2 will not loose if avoidable)?

As an aside: This stream, while devoid of direct repetition is very compressible. It is also an example of data which responds well to being compressed several times. Here are the first 1 million moves of the stream compressed twice. The file is a mere 512 bytes, and unpacks to a 26kb file, which again unpacks to 3Mb. That’s a compression factor of almost 6000!¹

More colours

What if the game had more colours? What if there were three colours of pebbles, not just two?

More repetition allowed

The choice that three repetitions form a pattern is arbitrary. What if we allowed three repetitions, but prohibited four? Clearly the games would be longer, but would it make an essential difference to wether a player has a winning strategy?

More players

What if there are more players? This could influence the dynamics, and I do not know of a winning strategy for the three player variant. Since the game could go on for ever, it is not obvious that there is a winning strategy for any player when he controls only a third of the moves.

There is also a question of who winns in a three player game. Below is a record of one, where player 1 places the loosing pebble. But did player 2 or player 3 win?

● ○ ● ○ ● ● ○ ● ○ ● ○ ○ ● ○ ● ○ ○ ● ○ ● ○ ○
1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 1 2 3 1

Different winning conditions would give different incentives. Here are two possible winning conditions:

Cooperative victory: If a player looses the other two win.
Exclusive victory: If player n looses, then player n + 1 (mod 3) wins.

In the cooperative variant it is clear that any two players could cooperate to win – basically because they out-number the third. But in a neurtal setting, who could cooperate? Player 1’s first move has no effect, but player 2 could play the same colour as Player 1, in order to open up for a cooperation with player 1. Then player 3 has a forced move, and when Player 1 is ready to make his move again, the board looks as follows:

● ● ○ ?
1 2 3 1

If player 1 plays ● now, he and player 2 can force player 3 to loose:

● ● ○ ● ● ○ ● ● ○ 
1 2 3 1 2 3 1 2 3

If player 1 instead plays ○ the playing field is more open, and player 3 gets to chose his move:

● ● ○ ○ ● ?
1 2 3 1 2 3

But even though player 2 and player 3 can cooperate to force player 1’s moves in this setup, player 3 would loose the sequence:

● ● ○ ○ ● ● ○ ● ● ○ ● ●
1 2 3 1 2 3 1 2 3 1 2 3

Thus, for the cooperative variant, the question is: Can either player 1 or player 2 choose to cooperate with player 3 instead? The answer remains elusive for the time being.

In the exclusive variant the player 2 does not want to help player 1 win, so

● ● ○ ● ● ○ ● ● ○ 
1 2 3 1 2 3 1 2 3

is not acceptable to player 2. However, it now unclear if any player has a winning strategy, or if given perfect play from each player the game would go on idefinitely.

The factor gets better as the stream progresses: the first 100 million moves can be compressed to a small 7.2kb file — unpacking it completely you might find that your text editor will struggle while opening the resulting file.↩︎

Writing Agda Code in Another Edtior

2019-01-02T12:00:00Z

Officially the only editor supported by the Agda-community is Emacs, through the Agda Emacs Mode. It is true that one forsakes many features by using another editor, but I want to convey my experience of using Acme for editing Agda code, and say something in general about editing Agda code without agda-mode.

Writing Agda without the training wheels?

Writing Agda-code can be seen as a very interactive process. You say where you want to go, give a partial solution containing one or more holes, and Agda will inform you what goals you have to reach in order to fill the gaps of your reasoning. The ability to leave holes is one of Agda’s greatest features, and if you have never tried programming like this — you should!

However, I often find the code which comes out of this process is not always the best. Some times I leave a hole, but the bits I wrote around the hole are not really helping. As I chase down the hole, I find my self adding more and more code to make the essence of the proof fit the oddly shaped hole I made. Of course I might realise my mistake, but if I first manage to get the hole filled then the motivation to start refactoring stuff to make it beautiful is low.

How to avoid this? I am not sure. In the course of solving a difficult problem one is bound to take detours and one will be lucky to arrive at an optimal solution at the first attempt. This seems inherent to the way we humans solve problems. I think that relying a less on the guidance of agda-mode, one can develop a better understanding of the matter at hand — that is the type checker, and the reduction of expressions.

Case study: Agda in Acme

Acme is a fantastic programming environment — a true pearl from forgotten times. Acme was designed with Unicode editing in mind. It makes very few assumptions about the nature of what you are editing, but rather integrates it self to the other tools on the system. So what happened when I tried to use it to write Agda code?

First thing one notices is that there is no syntax highlighting for Agda. Actually Acme has no syntax highlighting what-so-ever! However strange as it may sound, once you are used to living without, you do not miss it. In stead of a circus of colours on your screen, you get to focus on the beauty of the code itself. One effect of this is that I become less tolerant to clutter in the code, especially in the form of commented out code.

Next thing I did was to write a small script which runs a specific command periodically and monitors the output in an Acme window. Running the type checker in this way gives instant feedback on the status of my code every time I save the file — which I do often. One of the strengths of Acme is that the plumber — a complementary program working in sync with Acme — understands the kind of file-line-column adresses a compiler error comes with. So without any extra efforts I can right click the errors from agda to jump to the right place in the code.

Even without the interactive mode, making holes is useful, but I found that I more often would factor out the holes to a lemma with a type declaration — usually using where — and just letting the definition be ?. This would make it clear from just looking at the code what is missing. It also gave time to stop and think about the structure of the proof.

After writing like this for a while, I started having the deprecated Agda Interactive Mode running in an Acme window. Mostly just to evaluate expressions in the context of a hole, or check the odd type. I would also use this space as a scratch pad, writing down the types of various expressions currently under consideration.

To replace the jumping to the definition of a term functionality, I keep the following grep in my tagline:

> rc -c 'echo -n ''^''; cat ; echo '' ''' | grep -rn -f - $AGDA_STD

Certainly there is room for improvement on this one. I only spent one minute on the problem. However, even this simple solution allows me to mark a term with the mouse then middle-click the tag to get the type declaratation and definition of the term pop up in a window. This also prints the file and line number of the definition, so I can right click on that to open the file. Additional directories, such as the current project are simply added to the end of this command, and it will search those as well.

The AGDA_STD variable you see above is just an environment variable with the path to the agda standard library. To compile Agda-code I just use an mkfile with the following pattern:

%.agdai: %.agda
    agda -i . -i $AGDA_STD $stem.agda

Conclusions and the future

What I hope this shows is that Agda only works in Emacs is a truth with modificaions. Certainly some features of Agda are only available through the emacs mode, but these features are not essential to writing Agda code. Indeed showing some restriction as to which features one uses may improve overall code quality and readability.

Unicode for mathematics symbols in LaTeX

2019-01-02T12:00:00Z

We know how to input all the fancy Unicode mathematics symbols, but a simple text file in markdown still does not have nearly the sophistication of a Latex document — and for the most part that is a good thing. When complexity is not needed, it is nice to keep it at a safe distance. Sometimes, however, you really need to typeset some complicated equation; with sums indexing over uncountable sets and beautiful fractions whose denominator tend to zero. Or maybe you have a killer, commutative diagram which you have to typeset in xypic?

In any case you might happen to be typing and by new habit you happen to type the unicode character ℝ in stead of \mathbb{R}. What happens next is that your latex compiler starts yelling at you.

! Package inputenc Error: Unicode char \u8:ℝ not set up for use with LaTeX.

Why is this? You dutyfully had \usepackage[utf8]{inputenc}. Is that not enough? Clearly, not.

Turns out, this is a call for action. If you want to use fancy UTF-8 symbols in Latex, you must configure how they are interpreted. This is a good thing, because you can let your own personal preferences decide how it should work.

WikiBooks helpfully explains how this is done. All you need to do is to declare each symbol you want to use at the top of your document. The declations look like this:

\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}

The 211D is the Unicode code point of ℝ.

Notice that we use \ensuremath{} in order to make sure that the symbol is used in math mode. This allows us to type a naked ℝ in the middle of the text without surrounding it with dollar signs.

What? Is your preamble already too crowded to find your \author declaration? Then better put all the symbol declarations in a .sty file and include it as a package.

\usepackage{utf8-symbols}

To make life easier for myself, I wrote this little ten-line rc-script to add new entries in such a sty-file. Just run it, type your symbol and the associated Latex command, and it will generate an entry as described in the wikibook. The script uses the XCompose file from this article to look up the code of the symbol you typed, so make sure to have it before running the script.

You can download my current utf8-symbols.sty if you want a starting point for your own.

Here is an example latex file which uses it:

\documentclass[a4paper,12pt]{article}

\usepackage[utf8]{inputenc}
\usepackage{utf8-symbols}

\usepackage{amsmath}
\usepackage{amssymb}

\title{Lorem ip-∑}

\begin{document}
Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod
tempor, π, incididunt ut labore $2^n = ∑_{0 ≤ i < n} 2^i + 1 $ et dolore
magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation
ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute
irure dolor in reprehenderit in voluptate velit esse cillum dolore eu
fugiat nulla pariatur $0 = 1 + e^{π i}$. Excepteur sint occaecat 
cupidatat non proident, sunt in culpa qui officia deserunt mollit anim
id est laborum.

\begin{align}
 &f : ℝ → ℝ² \\
 &f(x) ≔ (x² , \lim_{a → x⁺} e^{-\frac 1 a})
\end{align}

\end{document}

Reading it still takes a bit of Latex knowledge. However, it makes it a bit easier to skim a formula.

Exercise: Write a script that reads the assignments in utf8-symbols.sty and automatically replaces the latex commands with the corresponding Unicode symbols. This is useful for updating old files.

Every-day Unicode

2019-01-01T12:00:00Z

This document is a short guide to writing unicode on systems with Xorg X11, such as Linux or *BSD.

Unicode is a systematisation of symbols, and contains just about any symbol you can imagine. The most common encoding of Unicode on computers is called UTF8, which overlaps with ASCII on the first 7 bits.

XCompose

Xorg has allow configuration of a compose key for mapping sequences of keystrokes to characters. For example, on my current setup i can type the greek letter π (pi), using the keystroke sequnce <RWIN> * p. That is first pressing once on the menu-button, then typing *, followed by p. Notice that these keys are pressend in sequence, not simultaneously.

The XCompose file

You can replace the default sequence mapping with a costom one, by writing it to the file ~/.XCompose. I use an XCompose file which derives from the Plan 9 keyboard file. It contains the complete cyrillic and greek alphabets, along with a lot of mathematical notation and useful everyday symbols. The following command gets the file, and you can inspect it.

curl -o ~/.XCompose https://hakon.gylterud.net/tutorials/XCompose

The lines of the XCompose file, each one giving a way to input a symbol, looks like:

<Multi_key> <minus> <greater> : "→" U2192

The <Multi_key> <minus> <greater> part tells you which sequence of keys to enter to produce the symbol. The sign in question is “→”, which happens to be unicode character with code U2192.

Setting the compose key

To specify which key shall be the compose key, one can use the command setxkbmap. For example the following command makes the «menu»-key the compose key.

setxkbmap -option "compose:menu"

I have this command in my .xinitrc so that it is run every time I start XOrg.

Another good choice may be right «windows»-button, rwin.

Note: If you want the right shift button to be your multikey, you need to use xmodmap to remap it:

xmodmap -e "keysym Shift_R = Multi_key"

GTK and QT applications

The following environment variable assignments hint GTK and QT applications to use the same compose settings as the rest of Xorg. Put them somewhere they will be exported to the relevant programs — I have mine in .xinitrc.

export GTK_IM_MODULE=xim
export QT_IM_MODULE=xim

What unicode characters are useful?

Accents

Accents are often used in names, and being able to correctly write some ones name shows respect and care for that person.

Here is an small selection from the XCompose file, to give you an idea of how the various accents are constructed.

<Multi_key> <apostrophe> <e> : "é" U00E9
<Multi_key> <a> <e> : "æ" U00E6
<Multi_key> <o> <a> : "å" U00E5
<Multi_key> <slash> <o> : "ø" U00F8
<Multi_key> <quotedbl> <a> : "ä" U00E4
<Multi_key> <v> <g> : "ǧ" U01E7
<Multi_key> <asciicircum> <e> : "ê" U00EA
<Multi_key> <underscore> <o> : "ō" U014D
<Multi_key> <comma> <c> : "ç" U00E7

Smileys

Textual communication can be difficult to master, and perhaps the most difficult things to convey are humour and sarcasm. If you want to make sure the reader understands that you are not completely serious you can include a smiley.

<Multi_key> <colon> <parenleft> : "☹" U2639
<Multi_key> <colon> <parenright> : "☺" U263A

The «em» dash & the «en» dash

Correct usage of dashes can be confusing, but a first step to mastering this art is to recognise that there are more than one. The key which is usually presented on the key board is not a dash, but rather a hyphen.

My personal favorite dash is the em dash, which is one «em» wide — that is the width of the m character. In my native Norwegian it is called “tankestrek” (literally “thinking dash”), and is used to set off parenthetical statements. It is also used when writing quotes such as:

The ideally non-violent state will be an ordered anarchy. That State is the best governed which is governed the least. —Mahatma Gandhi

Another dash is the «en»-dash, the width of an n, it is used They are both easily input using the below XCompose entries.

<Multi_key> <e> <m> : "—" U2014
<Multi_key> <e> <n> : "–" U2013

Read more about dashes at Butterick’s Practical Typography.

The ellipsis

A popular symbol often written on computers using three separate punctation marks, the ellipsis “…” is present in Unicode.

<Multi_key> <3> <period> : "…" U2026

Mathematical symbols

I love mathematics, but even if you don’t you might need a couple of mathematical symbools from time to time. The XCompose file mentioned ealier comtains really a lot of mathematical notation, and it is worth scrolling through the relevant sections of it. Below is a tiny selection.

<Multi_key> <d> <e> : "°" U00B0
<Multi_key> <i> <s> : "∫" U222B
<Multi_key> <m> <o> : "∈" U2208
<Multi_key> <m> <u> : "×" U00D7
<Multi_key> <s> <r> : "√" U221A
<Multi_key> <minus> <colon> : "÷" U00F7
<Multi_key> <period> <period> : "·" U00B7
<Multi_key> <f> <a> : "∀" U2200
<Multi_key> <t> <e> : "∃" U2203
<Multi_key> <t> <f> : "∴" U2234
<Multi_key> <t> <u> : "⊢" U22A2
<Multi_key> <asciitilde> <minus> : "≃" U2243
<Multi_key> <asciitilde> <equal> : "≅" U2245
<Multi_key> <N> <N> : "ℕ" U2115
<Multi_key> <O> <plus> : "⊕" U2295
<Multi_key> <P> <P> : "ℙ" U2119
<Multi_key> <Q> <Q> : "ℚ" U211A
<Multi_key> <R> <R> : "ℝ" U211D
<Multi_key> <s> <0> : "⁰" U2070
<Multi_key> <s> <1> : "¹" U00B9
<Multi_key> <s> <2> : "²" U00B2
<Multi_key> <s> <o> : "º" U00BA

Greek letters

The Greek alphabet is used frequently in science and mathematics, and is also useful for writing Greek. Below are the XCompose entries for the lower case Greek alphavet. They all start with *, so they are quite easy to guess.

<Multi_key> <asterisk> <a> : "α" U03B1
<Multi_key> <asterisk> <b> : "β" U03B2
<Multi_key> <asterisk> <c> : "ξ" U03BE
<Multi_key> <asterisk> <d> : "δ" U03B4
<Multi_key> <asterisk> <e> : "ε" U03B5
<Multi_key> <asterisk> <f> : "φ" U03C6
<Multi_key> <asterisk> <g> : "γ" U03B3
<Multi_key> <asterisk> <h> : "θ" U03B8
<Multi_key> <asterisk> <i> : "ι" U03B9
<Multi_key> <asterisk> <k> : "κ" U03BA
<Multi_key> <asterisk> <l> : "λ" U03BB
<Multi_key> <asterisk> <m> : "μ" U03BC
<Multi_key> <asterisk> <n> : "ν" U03BD
<Multi_key> <asterisk> <o> : "ο" U03BF
<Multi_key> <asterisk> <p> : "π" U03C0
<Multi_key> <asterisk> <q> : "ψ" U03C8
<Multi_key> <asterisk> <r> : "ρ" U03C1
<Multi_key> <asterisk> <s> : "σ" U03C3
<Multi_key> <asterisk> <t> : "τ" U03C4
<Multi_key> <asterisk> <u> : "υ" U03C5
<Multi_key> <asterisk> <w> : "ω" U03C9
<Multi_key> <asterisk> <x> : "χ" U03C7
<Multi_key> <asterisk> <y> : "η" U03B7
<Multi_key> <asterisk> <z> : "ζ" U03B6

Cyrillic letters

The Cyrillic letters are written starting with @.

<Multi_key> <at> <apostrophe> <apostrophe> : "ъ" U044A
<Multi_key> <at> <at> <apostrophe> : "ь" U044C
<Multi_key> <at> <at> <E> : "Е" U0415
<Multi_key> <at> <at> <K> : "К" U041A
<Multi_key> <at> <at> <S> : "С" U0421
<Multi_key> <at> <at> <T> : "Т" U0422
<Multi_key> <at> <at> <Y> : "Ы" U042B
<Multi_key> <at> <at> <Z> : "З" U0417
<Multi_key> <at> <at> <e> : "е" U0435
<Multi_key> <at> <at> <k> : "к" U043A
<Multi_key> <at> <at> <s> : "с" U0441
<Multi_key> <at> <at> <t> : "т" U0442
<Multi_key> <at> <at> <y> : "ы" U044B
<Multi_key> <at> <at> <z> : "з" U0437
<Multi_key> <at> <C> <H> : "Ч" U0427
<Multi_key> <at> <C> <h> : "Ч" U0427
<Multi_key> <at> <E> <H> : "Э" U042D
<Multi_key> <at> <E> <h> : "Э" U042D
<Multi_key> <at> <K> <H> : "Х" U0425
<Multi_key> <at> <K> <h> : "Х" U0425
<Multi_key> <at> <S> <C> : "Щ" U0429
<Multi_key> <at> <S> <H> : "Ш" U0428
<Multi_key> <at> <S> <c> : "Щ" U0429
<Multi_key> <at> <S> <h> : "Ш" U0428
<Multi_key> <at> <T> <S> : "Ц" U0426
<Multi_key> <at> <T> <s> : "Ц" U0426
<Multi_key> <at> <Y> <A> : "Я" U042F
<Multi_key> <at> <Y> <E> : "Е" U0415
<Multi_key> <at> <Y> <O> : "Ё" U0401
<Multi_key> <at> <Y> <U> : "Ю" U042E
<Multi_key> <at> <Y> <a> : "Я" U042F
<Multi_key> <at> <Y> <e> : "Е" U0415
<Multi_key> <at> <Y> <o> : "Ё" U0401
<Multi_key> <at> <Y> <u> : "Ю" U042E
<Multi_key> <at> <Z> <H> : "Ж" U0416
<Multi_key> <at> <Z> <h> : "Ж" U0416
<Multi_key> <at> <c> <h> : "ч" U0447
<Multi_key> <at> <e> <h> : "э" U044D
<Multi_key> <at> <k> <h> : "х" U0445
<Multi_key> <at> <s> <c> : "щ" U0449
<Multi_key> <at> <s> <h> : "ш" U0448
<Multi_key> <at> <t> <s> : "ц" U0446
<Multi_key> <at> <y> <a> : "я" U044F
<Multi_key> <at> <y> <e> : "е" U0435
<Multi_key> <at> <y> <o> : "ё" U0451
<Multi_key> <at> <y> <u> : "ю" U044E
<Multi_key> <at> <z> <h> : "ж" U0436
<Multi_key> <at> <A> : "А" U0410
<Multi_key> <at> <B> : "Б" U0411
<Multi_key> <at> <D> : "Д" U0414
<Multi_key> <at> <F> : "Ф" U0424
<Multi_key> <at> <G> : "Г" U0413
<Multi_key> <at> <I> : "И" U0418
<Multi_key> <at> <J> : "Й" U0419
<Multi_key> <at> <L> : "Л" U041B
<Multi_key> <at> <M> : "М" U041C
<Multi_key> <at> <N> : "Н" U041D
<Multi_key> <at> <O> : "О" U041E
<Multi_key> <at> <P> : "П" U041F
<Multi_key> <at> <R> : "Р" U0420
<Multi_key> <at> <U> : "У" U0423
<Multi_key> <at> <V> : "В" U0412
<Multi_key> <at> <X> : "Х" U0425
<Multi_key> <at> <a> : "а" U0430
<Multi_key> <at> <b> : "б" U0431
<Multi_key> <at> <d> : "д" U0434
<Multi_key> <at> <f> : "ф" U0444
<Multi_key> <at> <g> : "г" U0433
<Multi_key> <at> <i> : "и" U0438
<Multi_key> <at> <j> : "й" U0439
<Multi_key> <at> <l> : "л" U043B
<Multi_key> <at> <m> : "м" U043C
<Multi_key> <at> <n> : "н" U043D
<Multi_key> <at> <o> : "о" U043E
<Multi_key> <at> <p> : "п" U043F
<Multi_key> <at> <r> : "р" U0440
<Multi_key> <at> <u> : "у" U0443
<Multi_key> <at> <v> : "в" U0432
<Multi_key> <at> <x> : "х" U0445

A beginner’s guide to Darcs

2018-10-01T12:00:00Z

This document is intended as a quick guide to using darcs. It also also gives some example usage patterns.

This tutorial is available as

PDF
HTML

What is darcs?

darcs is a version control system, based on patches. A patch represents some change in the files, and the total collection of changes constitutes the repository.

When working on the files, one has a local copy of the repository. One can work on the files in the local copy as one normally would. After doing some changes, one records them to make a patch. After the patches are made they can shared with others, who can incorporate the changes into their repositories.

Why use darcs?

The motivation for using darcs is that it makes it easier for more than one person to work on a set of files simultaneously. One does not need to manually stitch together the changes made. It also gives a backup of everything, and records the history of the development.

Darcs works best with text files, such as source code, markup (such as HTML, or markdown), or plain text files.

Common commands

The following are the basic commands needed in order to use darcs.

darcs init

Create a new, empty repository in the current directory.

darcs get

Creates a copy of a repository. This is only done once to set up the local copy on your machine.

darcs add [FILE]

Tell darcs to add the [FILE] to the repository.

darcs record

Create a patch from the changes made to the local copy. This is done every time you have done some change which could be considered a logical unit.

darcs pull

Get patches from another repository.

darcs push

Push your patches to another repository.

Example of using darcs

Say I would like to work on my Agda computation library. The task at hand is to add a todo file with my current goals. At the moment there is no todo list, so when the file is created we need to alert darcs attension to it by use of darcs add.

$ darcs get ichor@hub.darcs.net:computation
Copying patches, to get lazy repository hit ctrl-C...
Finished getting.
$ cd computation
$ ls
Computation.agda	Predicate.agda		_darcs/				old/
mkfile
$ cat todo
# TODO
 - Fill out list of things todo
[EOF]
$ darcs add todo
$ darcs record
addfile ./todo
Shall I record this change? (1/2)  [ynW...], or ? for more options: y
hunk ./todo 1
+# TODO
+ - Fill out list of things todo
Shall I record this change? (2/2)  [ynW...], or ? for more options: y
What is the patch name? Added todo file.
Do you want to add a long comment? [yn]n
Finished recording patch 'Added todo file.'
$ darcs push
Pushing to "ichor@hub.darcs.net:computation"...
Thu May  7 08:39:34 CEST 2015  Ichor <ichor@Xishan>
  * Added todo file.
Shall I push this patch? (1/1)  [ynW...], or ? for more options: y
Finished applying.
Push successful.

More about the basic commands

To find out more about how each of these commands work, run

darcs help [COMMAND]

Or read the relevant sections of the manual.

Using darcs

We will now review typical uses of darcs.

File manipulation

Files managed by darcs can be edited in any editor. Darcs will automatically detect changes in the files which are under its supervision when you do darcs record. Some file manipulations can be done by darcs, which means that it can gracefully apply these changes in different contexts. For example moving a file can be done by darcs so that if another patch changes the same file, before it was moved, the changes will be applied to the file where it was moved.

Another useful file operation is replacing a string with another. This can for example be used to change the name of a function across an entire project, so that even parallel developments using the old name will be gracefully changed to the new name when the patch is applied.

A good practise is to use replace to change the occurences of a file name in other files when moving the file.

File manipulation commands

darcs move [FILE] [DEST]`

Move file to destination

darcs replace [OLD] [NEW] [FILE]

Replace the [OLD] with [NEW] in [FILE]

Patch dependencies

When creating a patch darcs determins which other patches needed to be in place for the changes to make sense. These patches are the implicit dependencies of a patch. There are also explicit dependencies, which you can specify using the flag --ask-deps when running darcs record.

When pulling or pushing a patch, darcs will pull/push all its dependencies.

Example: Using explicit dependencies.

Branches

Repositories which share some patches (but not all) are called branches. It is often practical to have several branches for each project — each with a different purpose.

Examples of branches

Some different use cases for branches:

The trunk. A centrally located repository, representing the current state of development. In coding projects it is good practise to keep the code in the trunk compiling at all times.
Working copy. A copy where one is performing current work.
Feature branch. A branch dedicated to devoping a specific feature. Once the feature is done and tested, it is pushed to other branches and can be deleted.
Version branch. A branch dedicated to a specific version of the files, for example targetting a public release.
Fork. A branch of a project intended to be an independent development.

These are all fairly long-lived branches. It is also useful to create one-off branches for various tasks.

Going back in time

Darcs allow you to create branches which contain any subset of patches, as long as they are closed under dependencies. This means that you can go back to an earlier state of the repository. For example when programming, this allows new work patterns and there are obvious benefits when trying to locate the source of a regression.

You can also roll back previous patches by constructing an inverse patch. An inverse of a patch is a patch which has the effect of undoing the changes made by the patch. This is useful of if you have revised some parts of your files, and later find out that the old version was better. The newer version is still kept in the history of the repository, so you can continuing your experimentation later, by rolling back the rolling back.

Finally, you can obliterate a patch. Obliterating a patch completely removes it from the current repository. It is recommended to exercise caution when obliterating patches, as you can loose important work. Obliterating can for the most part be avoided by using other techniques.

Commands for time traveling

darcs get --tag [TAG] [REPOSITORY]

This branches [REPOSITORY] and fetches the patches up to [TAG].

darcs pull [REPOSITORY]

When pulling [REPOSITORY], darcs will ask you which patches you want to pull, allowing you to choose the subset you are after.

darcs rollback

Lets you specified a set of patches, and constructs an inverse patch for them.

Example of cloning a repository up to a tag.

We can get version 1.0.0 of darcs.

 $ darcs get --lazy --tag 1.0.0 darcs.net
   (…)

Example of pulling only the desired patches

Say I would like to get a copy of my Agda computation project and check that it will compile without the old files.

 $ mkdir computation.no-old
 $ cd computation.no-old/
 $ darcs init
 $ darcs pull ichor@hub.darcs.net:ichor/computation
Tue Apr 28 09:26:29 CEST 2015  Ichor <ichor@Xishan>
  * Added computation module.
Shall I pull this patch? (1/4)  [ynW...], or ? for more options: y
Tue Apr 28 09:27:19 CEST 2015  Ichor <ichor@Xishan>
  * Added old computation things.
Shall I pull this patch? (2/4)  [ynW...], or ? for more options: n
Tue Apr 28 09:28:05 CEST 2015  Ichor <ichor@Xishan>
  * Added minimal mkfile
Shall I pull this patch? (3/4)  [ynW...], or ? for more options: y
Thu May  7 08:39:34 CEST 2015  Ichor <ichor@Xishan>
  * Added predicate logic lib.
Shall I pull this patch? (4/4)  [ynW...], or ? for more options: y
Finished pulling and applying.
 $ ls
Computation.agda  _darcs  mkfile  Predicate.agda
 $ mk all
(…)
Finished Computation.

Example of rolling back a patch

Example of locating a regression

Amending

Conflicts

Testing

Signing

Logic and creativity

2018-09-30T12:00:00Z

Recently I filled in a survey about the shape I see the the year as when imagining it. This is a topic I find interesting since my own experience when asking people this question is that it never fails to give interesting answers and usually an interesting discussion afterwards. I therefore took care to give detailed answers, and filled out the various other questions of the survey as well as I could. The final question, “Do you consider yourself more logically or creatively thinking?”, made me sigh, however.

The question was answerable with a five point scale reaching from “Logical” to ”Creative”, as if these two properties were somehow mutually exclusive, or at least that excellling in one of them would hamper the other. I believe this oft repeated dichotomy is false, and I would like to elaborate a bit on why I think it is so.

First of all, the two concepts “being logical” and “being creative” do not immediately contradict each other by any definition of terms. For instance, we could define “being creative“ loosely as “being able to come up with novel, and interesting or useful, things” — be they physical objects or ideas. And then let “being logical” mean “being able to understand a system and follow its rules”. A toy example would be that a creative person can craft a table, while a logical one would be able to follow IKEA’s instructions for assembling a table. There is ofcourse no reason a person cannot do both. But can anything more meaningful be said about the connection between these two properties?

One thing one could say, with reasonable certainty, is that these two properties are fundamental characterstics of human beings. Our whole society is steaming with new ideas, new craftings, and as far as we can tell, it has been like this for our entire history. At the same time, we find that people quickly understand the rules of their environment and adapt to these. In fact, it seems hard to imagine our species would have reached its dominance, for better or worse, without it.

Another thing, on which I am sure most would agree, is that most humans thrive both when they can creative and when they can be logical. Remark that I am not claiming that any person would enjoy any creative endeavour, or to follow any system. Just that there for any person are creative endeavours they would enjoy undertaking, and that there are systems they would enjoy following. Creativity seem for instance to be essential to humour, as jokes easily get old. While following rules is key to most peoples wellbeing, as it gives them some measure of predictability of their existence.

This brings us the the interaction between the two notions. Because, one of the ultimate creative endeavours is the construction of new systems of rules to follow. This is a creative undertaking which has being logical is a prerequisite, but which is the exact oposite of stereo types of both properties.

One the one hand, constructing the rules is the oposite of the idea that creativity is about not following rules. Not only do you have to follow the rules to understand the system you are constructing, but you also, implicitly follow the laws of logic when constructing your rules. On the other hand, this defies the idea that “being logical” implies following any rules blindly, since by creating new rules you have to take back and reason about consequences of the rules.

Mathematics is good example of an activity which essentially uses both our creativity and ability to be logical. It is easy to see how the latter plays a part, since mathematicians all play by the rules of mathematical reasoning. But built in to that system is the ability to define new concepts¹, and finding new mathematical objects² fitting into those concepts — a process which is extremely creative. Mathematical creativiy is an extreme example of an effect that is noticed also in art, namely that limitations, that is rules, induce creativity.

The final claim I want to make, which I find the most likely to be controversial, is that when given the freedom humans will tend to maximise both their creativity and ability to act logically, and that reductions in either is indicative of a lack of freedom. For instance, in a totalitarian society a person might simultaneously believe that he lives in a great society, while at the same time being aware of the suffering of the people in it, including him own — a clear logical fallacy. In contrast, a person who has secured his basic needs, and still has time to spare, will often take up a creative activity in this time.

In conclusion, we see that to put up a dichotomy between logical and creative ability, like this survey did, does little service to either, and that they are best seen as complementary, and fundamental, abilties of human beings.

Say, structures or theorems.↩︎
Say, instances of structures or proofs of theorems.↩︎

How I program without syntax highlighting

2018-09-30T12:00:00Z

For more than a year I have been without syntax highlighting. My editor of choice, acme, simply does not have it and I actually prefer it that way. Some would explain this as an instance of the Stockholm syndrome, or some strange form of hipsterism. However, I think there are some valid advantages to not colouring our texts, and so I will put them forth.

What syntax highlighting is good for

Some people perceive numbers and letters as coloured, and can use this ability to solve some tasks quicker. So initially, giving everyone synesthesia for free using syntax highlighting seems like it should improve our ability to understand code quickly. I do think it does give some speedup in checking wether there are syntax mistakes in the code. The classic example is some sneaky comment errors like this one:

  // Initialise
  for (i=0;i<3;++i) {
    /* Do initialisation here!
    niftyConfig = 1;
    funkyValue = 2;
  }

  // Run forever
  for (;;) {
   /* So, this is where we do stuff! */
  ...
  }

Syntax highlighting is not the only way of telling that your parenthesis, quotes and comments are matched up. In Acme I double click on the outmost marker to check that it has a match. This gives the added benefit that the region is selected if I wish to make edits to it. This is an active action on my part, because usually I know where my parentheisis go and do not need any help.¹

For most part syntax is not the most challenging part of programming, and I have yet to run into troubles where I could not spot my syntax errors. I usually program in a tight loop of writing, compiling and testing, meaning that any syntax related mistakes are probably in the most recently edited region and are easy to spot.

The beauty of code

The first thing one thinks when going from highlighted to unhighlighted code might be «This code is just a grey mash of symbols». Though, this sensation quickly fades as one gets engaged in the code. This “getting in to the groove”-part of the programming session is remarkably short, and afterwards code is more readable than English.

If the code is neatly organised, the «grey mash» quickly crystalises into a beautiful little universe of logically connected parts; each standing by it self, on its own line or in its own scope, but referencing each other in clear and beautiful ways. However, if the code is disorganised, with commented-out code, overly long lines and all, then the «grey mash» shape-shifts to a minefield in rough terrain, with craters and rocks obscruing the view.

What I am saying is that, coding without the syntax highlighting makes me much more sensitive to code “beauty”. This means that I avoid anti-patterns like having too long lines, or commenting out code. When my syntax highligher would make comments grey, I would frequently have two or three versions of a function in the comments while writing, and have to remind my self go clean the mess up. Now, I much rather copy the old version to a scratch file or buffer before making revisions. This keeps the code beautiful and easy to read.

Supports all languages

Once syntax highlighting is gone, you no longer priviledge the class of languages for which there exists a syntax highlighting. As a programmer you will not spend time looking for a highlighter, and configuring it for your preferences. Since I work a lot in a language called Agda, which is a language with absent support in most editors, this is important to me.

Editors in general suffer from over-configurability. Humans in general, and programmers in particular, like to tinker. Once you start tinkering on the configuration file of your editor, it easily gets in the way of what you actually were supposed to do. Syntax highlighting especially invites to these distractions as it is in your face while programming. If something about it annoys you, you are bound to notice while programming.

Supporting all languages equally future-proves the editor, because who knows which language we will use in ten years? Not to mention that syntax in a given language changes between version: new keywords added, new function syntax, and λ-abstractions added.

This also clears the distinction between the editor and other tools. The editor lets you edit code, it does not parse it and check its syntax. If it does, it is bound to do it wrong when the language changes, and require continual maintainance.

Other people have written about this before

Some programming languages, such as Agda, has comment nesting as part of their syntax and thus examples similar to the above would not be valid syntax. This is arguably the sane approach.↩︎

TaskWarrior

2018-05-01T12:00:00Z

While the name sounds agressive, the program itself is actually quite pleasant and useful. TaskWarrior is a todo-list manager with a command line interface. The command itself is just task, so even pacifists can use it.

Metadata is where TaskWarrior has its strength. If you take the time to type in a bit of meta-data on each task, there is much you can do with it in TaskWarrior. For instance, based on information such as tags and due dates, it computes the urgency of each task to help the user chosing what to do next.

The online documentation of TaskWarrior is very readable, and they have a lot of examples. The man page is a convenient refence, but not really suited for learning how to use it. So you need to go online to get started.

Ontology

TaskWarrior is not minimalistic, but its ontology is not very difficult: There are tasks and they have attributes, such as tags, due dates or priority. The tasks are presented in reports, which show a selection of attributes for a selected set of tasks. For instance, task ready shows tasks which are currently scheduled to be done, sorted by urgency. Another important attribute is depend which allows you to express dendencies

There is also support for user defined attributes (in the documentation often hidden behind the acronym UDA). This means that you can assign more semantics to your tasks, and possibly write your own scripts which interact with TaskWarrior.

Pitfalls

While TaskWarrior is not very difficult to learn, it might be difficult to use effectively. Here are some of the pitfals.

The first pitfall with any todo-list is just forgetting about it. Taskwarrior lives on the command line and will not pop up in your face every time you open the computer. It mighth therefore be easy to forget about it completely.

One way to avoid forgetting about it is to make a cronjob which e-mails you, say every workday, a list of remaining tasks. This makes TaskWarrior into a kind of personal assistant who every morning recites the tasks you have planned for the day.

Aother pitfall is the snowball effect. It is easy to get carried away with planning lots of activities, thinking that just because you can write it all on a list, you will be able to complete it all. Then you notice there are a few things you are not do in time for the deadline you set. Then you postpone it, start the next batch of tasks, again not completing everything. And suddenly there is an avalanche of things on your todo-lists, and you become demotivated by the sight of the list.

TaskWarrior has some features to remidy this. The attributes wait and schedule allows you to keep tasks which you do not have to do right now out of view. Taking schedule as an example: You can schedule a task (e.g. task add Do something. schedule:tuesday) and it will not appear in the task ready report until Tuesday. This helps reduce clutter. Tasks which you think “Oh, I should do that… someday.” you can actually schedule:someday and it will be kept, but not be in your face while you are doing more urgent things.

Håkon Robbestad Gylterud — Articles

Applicative logic

A boolean is maybe true

But why?

Disjunction

any

Conjunction

all

Extended example

Highlights of the extended example

Setting up a basic website

Markdown and Pandoc

Darcs

mk

sshfs

rsync

A word on backup

Extra credits

Test suite

Generating other formats

Disussion

Moog Mother-32

What is it?

Does it sound good?

Is it fun?

How modular is it?

YouTube self-defence

Blocking ads

Hiding suggestions

Downloading YouTube videos

Blocking auto-play

Surf in a private window

Channel RSS feeds

The anti-pattern game

The rules

Example

A winning strategy – READY PLAYER 1

Generalisations

Cooperating players

More colours

More repetition allowed

More players

Writing Agda Code in Another Edtior

Writing Agda without the training wheels?

Case study: Agda in Acme

Conclusions and the future

Unicode for mathematics symbols in LaTeX

Every-day Unicode

XCompose

The XCompose file

Setting the compose key

GTK and QT applications

What unicode characters are useful?

Accents

Smileys

The «em» dash & the «en» dash

The ellipsis

Mathematical symbols

Greek letters

Cyrillic letters

A beginner’s guide to Darcs

What is darcs?

Why use darcs?

Common commands

Example of using darcs

More about the basic commands

Using darcs

File manipulation

File manipulation commands

Patch dependencies

Example: Using explicit dependencies.

Tags

Tag commands

Branches

Examples of branches

Going back in time

Commands for time traveling

Example of cloning a repository up to a tag.

Example of pulling only the desired patches

Example of rolling back a patch

`any`

`all`

A winning strategy `– READY PLAYER 1`