Kenny's microblog

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

Running the miniDSP kit

miniDSP 2x4

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)

A macro pad

Unikeyboard Felix

... 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

Raspberry Pi as a 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 breadboard amp

Amp on a breadboard

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

Kinesis with XDA keycaps

Kinesis keyboard 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

case for hasu's tmk usb to usb converter case for hasu's tmk usb to usb 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

hasu's tmk usb to usb converter

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

planck with alps switches

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.

kinesis palm mod


lcd display

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

Hot evenings

temperature and humidity sensor

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.

Reading Dijkstra

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.

machined brass feet

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\)

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')
      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.


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 $
      (compare `on` fst)
      (zip indices
        (transposeAfterApply (M.setSize BS.empty rows cols) contents))