Kenny's microblog

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

Novar on a table

Novar Spud amplifier on a table

So the transformers arrived today. I have to wait a while for the chassis, but nothing's stopping me from setting her up... on a table. Did my readings (safely from a distance) - all checks out, so I hooked her up to the speakers and played a song or two. My first tube amplifier build!

Amp gone bad

Tube amplifier fixing

I bought this tube amplifier off a local guy (assembled from one of those Chinese eBay kits I believe) and it lasted about a month before going dead one day with my right speaker "crackling" and the output tube glowing bright. Turns out you should not run a capacitor at its max rating. Plug in a pair of 400V caps and it's working again.

JFET matcher

Objective 2 amplifier

I'm going to have to start matching my JFETs at some point. I found a great "helper" for this - the PCBs were printed by OshPark, and I have enough spare materials lying around. JFET matching here I come!

NwAvGuy's O2 amplifier

Objective 2 amplifier

Finished this O2 amplifier. It was quite fun getting a bag of materials with no labels - I learned how to read off the tiny numbers on ceramic capacitors. For about $25, one can get a quiet, well performing desktop/portable amplifier that drives almost all headphones. The solder pads are really thin on this PCB though, so making sure the joints are well soldered took me about 3 hours. Thanks NwAvGuy!

DIY front panel

Homemade panel for the Objective 2 amp

Work's been keeping me busy, but I still got to stash some time for them audio projects. I'm in the midst of building a couple of the O2s, and it just happens there's a piece of aluminium sheet I found in my room. So here's a first attempt at making a front panel.

PassDIY B1 Buffer

Nelson Pass B1 Buffer

Finally the audio caps arrive in the mail. Sitting this between the Raspberry Pi and the EL84 amplifier driving the Betsy's. I can drive the amplifier up without breaking the windows. Lovely.

Spud board arrives

Tube sockets soldered to the boarTube sockets soldered to the board

The board for the Spud amplifier arrived! The tube socket pins have to be teased out a bit with a plier, but after that the soldering was easy. I also finished adding the PCB mounting holes to the panel designs after taking measurements.

Designing panels

Laying out top panel for my Spud amplifier

I love it that making stuff always leads one down to learn stuff that might have never crossed my mind. This week, I'm learning the ropes of LibreCAD and putting down my first draft of the panels for my (soon to be built) Spud amp.

A buffer for the Betsy's

B1 buffer work in progress

Attempting the well-acclaimed B1 Buffer by Pass Labs. Keeping costs low as usual, here's the board half assembled on a plank.

Building the NuHybrid Amplifier

NuHybrid amplifier powered up

The parts arrived today, so I sat down for an hour of soldering fumes after dinner. I didn't want to wait for a backorder so I got a relay that doesn't quite fit the PCB, but nothing a bit of wiring and data sheet reading can't fix. Powered her up and yes, we have sound! (Quite nice actually)

Adding capacitors to the PSU

Wiring up the capacitors to the PSU

Time to hook up the capacitors. I need to get some nuts and bolts for the terminal strips, then I'll solder these down. Getting close to the last stage - a regulator power circuit.

Visualizing AC rectification

Oscilloscope showing DC current

As my friend says, the "grandfather of data visualisation". I passed the trafo secondaries to a bridge rectifier and then connected this up to the scope.

Trafo and lug mounted

Mounted ground and transformer

A bit more drilling and progress - mounted the transformer and chassis lug. Now we have the desired 48V out on the secondaries.

Trafo test

Testing the voltages across the secondaries on the transformers

Did a power up test. Tripped the house circuit breaker. Fixed problem. Measure and found out I actually didn't needed 2 trafos. AHHH...

Fuse and cord

Installing fuse and cord on chassis

Making some slow progress on the power supply project. After some hand drilling, here's the fuse and cord installed.

Assembled power board

Power supply board for amplifier

Onto the next project: a solid state amplifier. Here's the power board assembled.

That sound upgrade

OB speakers with Volt+ amplifier and Raspberry Pi/DAC

Being my first pair of open baffles, I had no idea what to expect. But once I hooked up the amplifier and started them up, I didn't want to leave the workshop... (yes, my ears are really happy) - Jolie Holland never sounded this good.

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