Trail cams

Dan has edited together the trailcam video from Monday. There are associated photos too, including a psychedelic one with the stag poking his tongue out.

Other than that, there's not so much from the deer this time, besides the stag showing off how his antlers are coming along and some rain-blurred video of the fawn(s). There's some lovely early-morning and late-evening scenes in there, clear shots of the badgers and foxes, some clear birdsong, and of course so many rabbits, hares and squirrels.

As social contact becomes more and more possible, we made a small change to allow camera checks to take place only once per week. The Campark camera (flawed operation, poor infra-red, battery-guzzling) has been moved to 'the den', from wich we get relatively few videos. In its place, looking downstream, is the Victure it replaced. Now there are two cameras in the stream location where we get some of the nicest stuff, only Victure cameras seem to last on eight batteries for months and fill up SD cards slower.

A trip to Bristol

I ventured to Bristol on Saturday to see Jonny P and Pinny K. The original plan was to visit Chew Moo's for ice cream, but it didn't seem like suitable weather, given the yellow rain warning the Met Office were issuing. Instead we sat in the heavy rain at the Bridge Inn and visited the market to eat filled Kurdish naan breads at Matina. As well as this, I also managed to injure my ankle on the way. Over the day, it got progressively more and more painful, and I ended up having to rest it.

Resting up with Agda

With all the rest time on Sunday, I thought I'd begin to explore dependent types on my computer. I've mentioned The Little Typer here before. It's a tour of dependent types, building understanding of them with the help of examples expressed in a small Scheme-like language.

Haskell is another good starting point for this kind of exploration, with two onward possibilites being Agda and Idris. Remarks on #haskell about the difference between these suggested that Agda contains a wider and more interesting range of type-theoretic features, offering full support for dependent types via its expressive type system. Idris has a similar syntax to Haskell and is considered to be generally more performant. It's also named after Idris the dragon from Ivor the Engine. I hope to give both a try over the next few weeks, but it appears Agda is more suitable for my 'learning by doing' goals right now.

So, I started out with the book Programming Language Foundations in Agda and the tutorial Programming and Proving in Agda. There are many other options: A List of Agda Tutorials gives some. (I also looked at Learn You an Agda And Achieve Enlightenment solely because of the title and because I enjoyed Learn You A Haskell For Great Good!) Anyway, or a quick play with Adga without having to install it on your computer, there's the Agda Pad, which presents a VNC session to an GNU Emacs editor set up for Adga. This is really handy if you aren't ready (or willing) to install Emacs, or interactive support for your favourite editor. The commands in Agda Pad are the Agda Emacs commands and seem to be the same as described for Visual Studio Code in Programming and Proving in Agda (so far).

Of course there's a lot more to explore here than is possible to do in a single day, but a few things stick out. Whereas partial functions are allowed in Haskell, total functions are required in Agda. Throwing errors is just not done in Agda, but instead dependent types are used to encode invariants of programs into the types, such as bounds on the sizes of data structures. These properties can then be checked by the type checker, enabling it to catch a much wider class of errors. Of course it requires a new level of deliberate rigour, but brings about a new level of safety.

But we can go beyond this. There's a famous, surprising and direct link between computer programs and mathematical proofs! By using the Curry-Howard correspondence, we can take any formula in propositional logic, turn it into a type in Agda (the type whose elements are valid proofs of that proposition), and prove that formula by defining a function of that type. Logical proofs can be written as functional programs, and people who are into functional programming can use it to prove statements formally. Proof systems and models of computations are the same kind of mathematical object. That is: a proof is a program. For each simplification of a proof, there's a way to evaluate the program.

Checks concerning the bounds of data structures improves type-safety, but it would be even better to establish and prove propositions about the values and functions in programs. Under the Curry-Howard correspondence, propositions are dependent types, and we can construct a new type for the property we're interested in. Case analysis shows up as pattern matching, induction shows up as recursive functions, and more. And while Haskell Curry made the original observations relating to the correspondence (for Hilbert systems and typed combinatory logic) in 1934 and 1958, William Howard extended it (to natural deduction and the lambda calculus) in 1969. This extension brought in the familiar quantifiers 'for all' and 'there exists' . Thanks to this extension, we can use the dependent function type and the dependent pair type for these, both of them intuitive ingredients of Agda's type system. We now have a strong correspondence between first-order logic and a dependent type system.

So, with all this established, we can arrive at proofs about properties of our programs for the type checker to verify. Often this is done via arriving at a chain of equations which, taken together, show that one expression is equivalent to another. When we optimise or otherwise transform a function, we can be certain it still works, or we can be sure that the algebraic laws of a typeclass are kept to, or a bunch of other applications. I have some ideas for where I'd like to take this with my own projects, but for now there's a ton more to explore.

Also this week

Godspeed You! Black Emperor; Codenames Duet with Chris B; Maisel's Weisse Alkoholfrei beer; Space Ghost Coast to Coast; the mononoki font; Haskell's string-interpolate quasiquoter; Freespin by Reflex, the first demoscene production for a Commodore 1541 floppy drive (a '1541tro').