29 September, 2017

Infrared Raspberry Pi

When I ordered my Pi Zero W with a no-IR-filter camera, I also ordered a single infrared LED. This was enough to prove that I could illuminate things with IR, but not really good enough for more than a small dot of light.

So, then I ordered 50 x £0.04 infrared LEDs from RS (which arrived overnight!) and wired them up yesterday onto a single breadboard powered by a regular USB 5v power supply. You can see the layout in the first picture.

Here's a scene: the first with natural light showing the LEDs on a board, and the next two with infrared illumination. The two infrared scenes appeared almost pitch black to a human eye.

And then I set it up overnight, with a timelapse video of myself sleeping:

10 September, 2017

Unix exit codes as an indicator of tooling (im)maturity.

If your compiler for your new language, or your test running, or whatever, doesn't return a unix exit code when it exits with an error - that's something that annoys me - and it's an indicator that no one is using your tool for serious - for example in an automated build system.

I've hit this a couple of times at least in the last year. grr.

01 September, 2017

Pattern matching in Idris `do` notation has surprising reliance on type checking the action.

Idris is syntactically quite Haskell-like, and especially it has do notation for sequencing "actions".

Like (traditional) Haskell, do blocks are desugared to a sequence of >>= (bind) operators. But, unlike (traditional) Haskell, that >>= is not always the monadic >>= : m a -> (a -> m b) -> m b. (This can also happen in Haskell using rebindable syntax)

In Idris, you can use different "better-than-monad" types to statically (at compile time) reason about a computation beyond using the monad laws. For example, an effect system might track which effects are in scope.

Total parsing

In the case of Text.Parser (in the Idris contrib/ package) the type signature of actions (Grammar _ _ _ indicates whether a parser consumes any characters so that the compiler can tell if a parser might loop forever. (see http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.html)

I was trying to write a new JSON parser for idris-todaybot using Text.Parser. Previously JSON was parsed using lightyear, but Text.Parser has more gratuitous dependent types so was an obvious way to proceed.

A problem.

I ran into a surprising compile error which initially made no sense to me at all.

This code compiles:

objectValuePair : Grammar Char True (List Char, ())
-- definition elided

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  llll <- objectValuePair
  pure llll

where llll is a tuple; but the following version of jsonObject, which desconstructs that tuple and reassembles it, does not compile:

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  (k,v) <- objectValuePair
  pure (k,v)

It gives this error:

When checking right hand side of Main.case block
in jsonObject at bug-bind.idr:55:14 with expected type
        Grammar Char c2 (List Char, ())

Type mismatch between
        Grammar Char False (List Char, ()) (Type of pure (k, v))
and
        Grammar Char c2 (List Char, ()) (Expected type)

Specifically:
        Type mismatch between
                False
        and
                c2

Another attempt to deconstruct llll also fails:

  jsonObject : Grammar Char True (List Char, ())
  jsonObject = do
    llll <- objectValuePair
    let (k,v) = llll
    pure (k,v)

but the following deconstruction by function application rather than pattern matching succeeds:

jsonObject : Grammar Char True (List Char, ())
  jsonObject = do
    llll <- objectValuePair
    let k = fst llll
    let v = snd llll
    pure (k,v)

That type error

Let's dig into that type error:

Type mismatch between
        Grammar Char False (List Char, ()) (Type of pure (k, v))
and
        Grammar Char c2 (List Char, ()) (Expected type)

Grammer _ _ _ is the type of parser actions, where the first parameter Char is the type of symbols we're consuming, the final parameter (List Char, ()) is the type that the parser will return on success, and the middle parameter (False or c2) represents whether the parser will definitely consume input (True) or might succeed without consuming anything (False - for example, a parser which removes whitespace, or pure which never even looks at the input stream).

This "consumes" parameter contains the main novelty in Text.Parser beyond monadic parser combinators: Text.Parser combinators manipulate and use this value at compile time to help check that parsers really will consume things: for example, a parser that definitely consumes followed by a parser that might not, results in a parser that definitely consumes; while sequencing two parsers that might not consume results in a parser that might not consume. (See: the source)

So what on earth has this parameter, manipulated by >>=, got to do with pattern matching pure values after they've already been returned by an action?

Desugaring

It turns out we can forget that our troublesome tuple is being returned from an action; let (a,b) = (1,2) breaks in the same way when run inside a Text.Parser do block.

Let's (very roughly) desugar some of the examples above, and then look at the types involved:

jsonObject : Grammar Char True (List Char, ())
jsonObject = do
  llll <- objectValuePair
  pure llll

-- becomes:
jsonObject = objectValuePair >>= (\v => pure v)

jsonObject = do
  (k,v) <- objectValuePair
-- becomes: 
    objectValuePair >>= (\(k,v) => pure (k,v))
-- becomes: 
    objectValuePair >>= (\llll => case llll of
      (k,v) => pure (k,v)
     )

So in the second fragment, there's an extra case expression in there to deconstruct llll using pattern matching.

Apparently that gets in the way of type inference/checking:

  • On the one hand, that pure has type: Grammar Char False (List Char, ()) - false because it may (actually, will always) succeed without consuming input.
  • On the other hand, >>= doesn't care whether the right hand side consumes or not - it will take either, as shown by the compile time variable c2 appearing in the error message.
Idris doesn't manage to unify c2 = False.

With further pinning of types using the, an uglier form of pattern matching does work:


export jsonObject : Grammar Char True (List Char, ())
  jsonObject = 
   do
    llll <- objectValuePair
    the (Grammar Char False (List Char, ())) $ do
        let (k,v) = llll
        pure (k, v)

Ugh

Thanks

Thanks to Melvar on #idris for explaining this.

highlight.js in blogger

Syntax highlighting is pretty. highlight.js can do it in a browser. I just added it to this blog.

  1. In Blogger, click "Theme" then "Edit HTML"
  2. Find the <head> section of the theme.
  3. Insert the following at the end, before the closing <head> tag:
    <link href='//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/styles/default.min.css' rel='stylesheet'/>
    <script src='//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/highlight.min.js'/>
    <script src='https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.12.0/languages/haskell.min.js'/>
    
  4. Add as many copies of the third line as you want, modifying haskell to the additional languages that you want to be able to highglight.
  5. When writing code, wrap it in <pre><code class="haskell"> YOUR CODE </code><pre>

31 August, 2017

Raspberry Pi Zero W + cam timelapse

I got a Raspberry Pi Zero W and a camera module.

I wanted a timelapse video.

This is how I did it:

Capture a sequence of image frames

This will capture a sequence of images (forever) approximately every minute, with the filename being a unix timestamp.

while true; do raspi-still -o $(date +%s).jpeg ; sleep 60s; done

Leave this to run for as long as you want to collect frames, and you'll end up with a bunch of numerically named files, like this:

$ ls
1504014800.jpeg
1504014866.jpeg
1504014931.jpeg
...

Combine the sequence of image frames into a jpeg

After you've got all the frames you want, use ffmpeg to join the frames together. I do this on a different Linux box (my laptop) but you should be able to do it on the Pi too.

First make a command file listing all the jpeg files:

ls *jpeg | while read a ; do echo file $a; done > e.cmd

Next, feed that command file into ffmpeg to generate a video:

ffmpeg -f concat -i e.cmd -b:v 1500000 -r 24 -c:v libx264 e8.mp4

As a result, the output video should be in e8.mpg which is in a form suitable for playing with vlc or uploading to YouTube.

20 August, 2017

An income tax explorer, using R and Shiny

I got carried away with my R code for plotting income tax rates, and now it is an interactive webapp https://benc.shinyapps.io/r-income-tax/ using Shiny, a web framework for turning your R code into a website. Thanks Tom Nielsen for convincing me (in this talk about making a Haskell port of Shiny) to try it out.

18 August, 2017

A first project in R / UK income tax graphs

The UK income tax system has a progressive tax rate that gets higher as your income is higher. However it has a few quirks. I've been meaning to graph the effective rates, and today I felt like learning a bit more R to do it. I've included income related student loan repayments and National Insurance because they are, to some extent, income-tax-like.

The code at https://github.com/benclifford/r-income-tax can generate the following three graphs:

Marginal income tax rates, coloured by component, for varying income:

Total tax, for varying income:

Fraction of income taken as tax, for varying income:

24 July, 2017

WinTec GRays 2 GPS device feeding to NTP

USB driver

When I got a wintec g-rays2, it didn't work on USB out of the box with whatever laptop I had (probably a macbook), but was OK on Bluetooth, so that's what I stuck with.

Now, eight years later, I plugged it into one of my Raspberry Pis and it appears as /dev/ttyUSB1 by magic!

Getting NMEA sentences in minicom

minicom --device=/dev/ttyUSB1 --baud=4800 gives some garbled stuff every second, so I'm receiving the NMEA sentences but at the wrong serial port settings.

The manual didn't give any help but a bit of fiddling reveals sensible looking output at 57600 baud, 8N1 (here you can see where I live).

$GPRMC,121815.000,A,5130.3697,N,00003.7216,W,0.00,148.43,240717,,,A*72     
$GPGGA,121815.000,5130.3697,N,00003.7216,W,1,05,2.9,46.2,M,47.0,M,,0000*70 
$GPGSA,A,3,21,26,31,27,16,,,,,,,,4.3,2.9,3.2*38                            
$GPGSV,3,1,12,05,03,021,28,10,08,157,19,21,67,086,34,26,69,175,39*7C       
$GPGSV,3,2,12,29,12,083,,07,08,333,,31,06,193,26,20,27,059,24*72           
$GPGSV,3,3,12,49,,,35,27,43,274,31,16,72,283,39,18,26,132,23*4D 

These lines are spewed out once a second without needing to send any start command to the GPS unit.

Getting ntpd to pay attention

$GPRMC and $GPGGA are the relevant sentences for ntpd, according to the manual.

I already have ntpd runnning on this Pi, with an MSF receiver configured already.

This gives a /dev/gps0 (at least until reboot):

cd /dev
sudo ln -s ttyUSB1 gps0

and this line in /etc/ntpd.conf makes ntpd look for NMEA time sentences on /dev/gps0:

server 127.127.20.0 mode 67

The mode, decimal 67, means hexadecimal 0x43: 0x01 listen for GPRMC, 0x02 listen for GPGGA, 0x40 use 57600 baud.

And after a restart, tada! (although apparently a 160ms delay compared to all my other time sources. ick)

pi@faeroe /dev $ ntpq --peers
     remote           refid      st t when poll reach   delay   offset  jitter
==============================================================================
 2001:8b0:1638:9 81.2.122.172     2 u   39   64   17    0.952  157.794   0.783
 ntp2.aa.net.uk  195.66.241.2     2 u   41   64   17   14.923  162.505   0.671
 SHM(2)          .MSF.            0 l    -   64    0    0.000    0.000   0.000
*GPS_NMEA(0)     .GPS.            0 l   55   64    7    0.000   -5.660   0.819
 tyne.cqx.ltd.uk 81.2.122.172     2 u   46   64   17    0.674  157.858   0.759

03 July, 2017

/etc/hosts - the gift that keeps on giving

/etc/hosts

The gift that keeps on giving, when you're paid on an hourly rate to do tech support. It is like the regexps of DNS: "I know, I'll modify /etc/hosts" ... now you have two problems.

  • You modify /etc/hosts because you want to override the global DNS view of name N.
  • Things works!
  • Because things work, you don't undo your change in /etc/hosts. After all, things work.
  • A year passes.
  • You forget that you made the change.
  • Suddenly on your machine only, but no one else's, you can't access the website at N any more.
  • Hours of debugging!

Why modify /etc/hosts? Testing a new version of a site under real name (only on your own machines though), or because DNS is broken and you don't know why, or because you didn't plan your DNS change so now the caches are not updating fast enough and you are impatient.

/etc/hosts doesn't have an "eventual consistency" mehanism in place - DNS caches eventually expire and at least give vaguely consistent behaviour across the whole internet over a long enough period of time. /etc/hosts will never converge.

26 June, 2017

ffmpeg animated gif custom palettes

I used ffmpeg to make the animated gifs for my gallery of NeoPixel goggles patterns.

In the process I discovered that as well as the expected fairly straightforward conversion mode, ffmpeg -i mymovie.mov mymovie.gif, there is another mode which can generate a custom palette. Because apparently by default, a default palette is used.

That is a slightly more awkward two step process, described for example here, but at least for my goggles GIFs looks way better (to me) although turning out to be four times the size: