# Kenny's microblog

Brain dump
/math, logic, beauty
/functional programming
/software craftsmanship
/diy audio
/keyboards, typing
/ ...etc.

## Running the miniDSP kit

The software for the miniDSP kits are available for only MacOS or Windows. I took the chance and tried running it on Wine, which didn't quite work (Wine doesn't support USB interfaces). In the end, I rummaged through my old laptops, found a Windows XP key and tried it in Virtualbox, which did the trick, assuming one did the following:

1. Install Windows XP, Virtualbox guest additions and USB interface extension...
2. Install Dotnet SP1 (just Google)

... And this came in the mailbox today. I forgot that I had ordered this back in July to practice soldering. Well, I'm pretty good at it now, but the surface mount MOSFET was quite the challenge without any flux on hand. Smack on my spare XDA keys, added some layers (vim macros, hotkeys for the browser and a classic numpad) and now it's ready to go!

## My new DAC

I finally got my hands on a Raspberry Pi. After playing with it for a bit - surfing the Web, running Tiny Yolo on the camera module etc, I killed the Raspbian image and loaded in Volumio. Hooked it up to my Valhalla and sat down to listen - love it!

## OB speakers: Baffle assembly

Baffles assembled. Waiting on the drivers...

A working amplifier on a breadboard (hooked up to my FiiO X1).

## Kinesis with XDA keycaps

These XDA keycaps finally arrived and they feel great - these raised the height of the keys overall and are easier to reach than the stock keycaps.

And that marks the end of my short journey with keyboards! Time to move on to other projects next.

## Case for converter

Took an afternoon one weekend and thought maybe I can give 3D printing a go. After an hour of OpenSCAD tutorials, I managed a case for the converter and send it off for printing. The shop delivered this today - I'm quite pleased with it!

## Portable firmware

I had been setting my keyboards to Colemak in the OS settings, which works alright most of the time. There are some exceptions, such as when the password prompt to decrypt the drives before the OS kicks in (which means I have to remember to type in Qwerty) ... So this converter is an awesome stand-in until I work on a more ambitious attempt to replace the onboard controllers. Plus I have layers! Which is something that I've been meaning to add to my typing-fu.

## More keyboard fun

Assembled a Planck for my friend (speed soldering practice?)

Adding a LED to my Kinesis for vanity (just so that Defender keycap shines!)

## Kinesis palm mod

I type on a Kinesis Advantage at home, with foot pedals. So when I go to work standing most of the time, I really didn't like having to stretch my pinkie out for the shift keys. This is one of the more popular mods I've seen, so I bought some arcade buttons and got to work.

## LCD

... and here's the sensor hooked up to a LCD.

## Hot evenings

The weather sites keep saying the temperature at night was 28°C, which felt really suspect as I sit there sweating. The readings from this simple sensor was more agreeable - 31°C.

One of my goals for the year was resuming reading some beaten copies of Dijkstra's books that I gotten off eBay some time ago. I'm loving this paragraph that I read on the way home:

Programming is as much a mathematical discipline as an engineering discipline; correctness is as much our concern as, say, efficiency... The effort to make our program more time-efficient, however, should never be an excuse to make a mess of it.

A Discipline of Programming by Edsger W Dijkstra.

## Machined brass feet

The rubber feet came off on my Kinesis, so I decided to machine replacements. It's good to have some stock brass lying around.

## MaybeT and <|>

-- Given 2 I/O actions that return some Maybe a,
-- I want to "chain" them within a Servant handler
foo :: IO (Maybe a)
bar :: IO (Maybe a)

myHandler :: Handler Foo
myHandler = do
result <- liftIO $runMaybeT (MaybeT foo <|> MaybeT bar) case result of Just x -> -- rest of code... ## Fundamental functions of propositions The introduction of Principia M. begins with these primitives, $$\neg p$$ $$p \lor q$$ $$\vdash$$ and these definitions, $$p \land q \cdot = \cdot \neg(\neg p \lor \neg q)$$ $$p \supset q \cdot = \cdot \neg p \lor q$$ $$p \equiv q \cdot = \cdot p \supset q \land q \supset p$$ ## Abstract refinement example {-@ type Even = {v:Int | v mod 2 = 0} @-} {-@ type NEList a = {v:[a] | len v > 0} @-} {-@ max :: {v:Int | v mod 2 = 0} -> {v:Int | v mod 2 = 0} -> {v:Int | v mod 2 = 0} @-} max :: Int -> Int -> Int max x y = if x <= y then y else x {-@ maximum :: NEList ({v:Int | v mod 2 = 0}) -> {v:Int | v mod 2 = 0} @-} maximum :: [Int] -> Int maximum (x : xs) = foldr max' x xs {-@ maxEvens :: [Int] -> Even @-} maxEvens :: [Int] -> Int maxEvens xs = maximum (0 : xs') where xs' = [x | x <- xs, x mod 2 == 0] ## Refining types with Liquid Haskell I like the idea of Liquid Haskell - you can establish some invariants quickly by adding a predicate over existing types via annotation. (that I also finally get to use Z3 to verify code is pretty rad). For example, {-@ data Foo = Foo {t :: {v:ByteString | bslen v > 0} } @-} newtype Foo = Foo ByteString causes Liquid to complain that a function using the datatype didn't respect the invariant - even though it type checks. Liquid can also check for totality and non-termination. Definitely adding this to my existing toolchain. ## Presets TIL: Without an equivalence relation, "types" used in programming are more accurately thought of as presets, rather than an analog of types as defined in mathematics. For practical purposes, we just can't compare everything, e.g. extensional equality on functions renders type checking undecidable. In Haskell we can compare functions if we impose restrictions - finite domain/codomains, as demonstrated in this post. ## Church Numerals {-# LANGUAGE RankNTypes #-} module ChurchNum where zero :: (a -> a) -> a -> a zero _ z = z one :: (a -> a) -> a -> a one s z = s z two :: (a -> a) -> a -> a two s z = s (s z) three :: (a -> a) -> a -> a three s z = s (s (s z)) -- etc scc :: ((a -> a) -> a -> a) -> (a -> a) -> a -> a scc n s z = s (n s z) plus :: ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a plus m n s z = m s (n s z) mult :: (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> ((a -> a) -> a -> a) mult m n = m (plus n) zero -- without using plus mult' :: (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> ((a -> a) -> a -> a) mult' m n = m . n -- raise x to the power of y pow :: (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> ((a -> a) -> a -> a) pow x y = y x ## Church Pairs {-# LANGUAGE RankNTypes #-} module ChurchPairs where import ChurchBool pair :: a -> a -> (forall a. a -> a -> a) -> a pair f s b = b f s fst' :: ((forall a. (a -> a -> a)) -> a) -> a fst' p = p tru snd' :: ((forall a. (a -> a -> a)) -> a) -> a snd' p = p fls ## Church Booleans {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-} module ChurchBool where tru :: a -> a -> a tru t _ = t fls :: a -> a -> a fls _ f = f and' :: (forall a. a -> a -> a) -> (forall a. a -> a -> a) -> a -> a -> a and' b c = b c b or' :: (forall a. a -> a -> a) -> (forall a. a -> a -> a) -> a -> a -> a or' b c = b b c not' :: (a -> a -> a) -> a -> a -> a not' b = flip b ## Trying out Colemak I've been trying to correct my typing recently and when I learnt about Colemak, I decided to get on the bandwagon. Now my productivity is about 10 WPM! Rewiring is tough! Update: A week plus in, at 25-28 WPM now. Looking to double this before I make the transition to the Kinesis Advantage. ## Euclid's proof This proof of primes being infinite is simple that it's beautiful: Let $$P$$ be the set of primes. Suppose $$Q =\{q_1, ..., q_n\} \subset P, Q \neq \emptyset$$. Let $$m = 1 + q_1...q_n \neq \pm 1$$. There is a prime $$p$$ that divides $$m$$ (fundamental theory of arithmetic). Since no $$q_i$$ divides $$m, p \notin Q$$. That is, $$Q \neq P, P$$ is infinite. ## Davis-Putnam procedure Rewrite statements into conjunctive normal form (in practice this seems to blow up quickly). Then we can apply resolution: $$L \in C_1 L' \in C_2, C_new = C_1/L \cup C_2/L'$$. Adding to this strategies such as elimination (tautology, subsumption, pure literal), we then enumerate down the clauses to arrive either at the empty clause (unsat) or $$\emptyset$$ (sat). After each step, the pivot is removed, i.e. $$P_t \not\in S_t$$; it will terminate. ## Reliabilty drives value Over coffee with Y, talked about how reliability drives value, especially when it comes to complex systems. How can reliability be had? For one, writing tests. Use a language with type checking. Purity is good - being able to reason about your programs etc. Test often, refactor often, simplify often - until it's simple, but no simpler. ## Matrices and csv data I have to post processing some data encoded to CSV: client required that the submitted file must adhere to some format (position of columns, additional k empty columns). Well, legacy/enterprise systems, gotta love those. In Haskell, I simply decoded the CSV generically, then converted it to a matrix. Taking the list difference of my data against the client's template, we obtain indices by to tack against the transposed matrix (after extending the matrix) and then transposing it back once more. contents' = transposeAfterApply id . map snd$
sortBy
(compare on fst)
(zip indices
(transposeAfterApply (M.setSize BS.empty rows cols) contents))