# Kenny's microblog

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

## Novar 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!

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

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!

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 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 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 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 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 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 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 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 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 A bit more drilling and progress - mounted the transformer and chassis lug. Now we have the desired 48V out on the secondaries. ## Trafo test 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 Making some slow progress on the power supply project. After some hand drilling, here's the fuse and cord installed. ## Assembled power board Onto the next project: a solid state amplifier. Here's the power board assembled. ## That sound upgrade 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 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 ... 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 breadboard amp 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. ## 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. ## 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))