PatternMatchable, Yoneda Embedding, and Adjunction

-- Note: BlockArguments & LambdaCase extensions used

-- Pattern match @pat@ of two cases, and recreate the pattern @pat'@
pat' = match pat \case
  Maybe a -> be (Maybe a)
  Nothing -> be Nothing

match :: ∀ m p c b. m p -> (c -> m b) -> m b
be :: ∀ m p c. c -> m p

class PatternMatchable m k p c | m -> k, m p -> c, c -> m p where
  match :: ∀ b. k b => m p -> (c -> m b) -> m b
  be :: ∀ . c -> m p

-- Pattern matching of Maybe values
instance PatternMatchable (YulCat eff r) YulCatObj (Maybe (INTx s n)) (Maybe (YulCat eff r (INTx s n)))
-- Pattern matching of Solo tuple
instance PatternMatchable (YulCat eff r) YulCatObj (Solo a) (YulCat eff r a)
-- Pattern matching of tuple
PatternMatchable (YulCat eff r) YulCatObj (a1, a2) (YulCat eff r a1, YulCat eff r a2)

∀ x. (a -> x) -> (b -> x) ≅ b -> a

Adjunction Between Hask and Your DSL

Here is another observation of how match function is also an adjunction.

Again, I will refer you to Bartosz' article about adjunctions, for more about the topic.

Let's say your eDSL program m a is of category D. Additionally, we can also view Haskell types as objects in the category of Hask. Technically, as an deep embedded DSL, all objects in D is also in Hask. However, as a DSL, there should be no morphism from object in D to ones outside of D. For this reason, we illustrate the match function as an adjunction that depicts D and Hask not overlapped for better visuals.

What Is Principle and Can We Know It?

The opening chapter in the same-title book of Leonard Peikoff's "Why Act on Principle?" - a collection of his best articles and talks - starts with paying attention to the most commonly observed intuition of our world today: we live in a "complex" world. As the author then points out, the utterance of this observation is used as an argument for a methodology that goes unchecked in today's society, which is called pragmatism.

So, what is wrong with pragmatism? Is it not a reasonable thing to do for any well-educated man?

The world is complex, and man's life is inherently complex. "He has countless choices to make, he has the whole world spread before him, he must continually make decisions and weigh results keeping in mind a multiplicity of factors." Facing the complexity, the most fundamental methodological choice man must make is whether he can find a generalization over concrete, and if so, how can he find such a generalization?

As a pragmatist, the answer is no. Instead of looking for generalizations, a pragmatist deals with the particular. "Well, it depends on the situation." says a pragmatist. You then press him further, "Had we studied as much of the situations as possible, is it possible for us to come up with a generalization that says something about this situation?" "But who could have?" The pragmatist deflects. "A principle is a basic generalization. We have learned principles suited for many situations from the vast wealth of human knowledge." You should now strike straight into the heart of the issue. "You are just being simple-minded." The pragmatist inevitably resorts to ad hominem. That's when you know that's where the "Big Lie" is.

It cannot be further from the truth to say that a rational thinker who acts on principle is being "simple." Contrarily, he engages in a complex mental activity that condenses information he has gathered and retained. "Concepts are man's means of condensing information," and the conceptual faculty in humans is called "reason."

With reason, a man can fully grasp new principles from experiencing reality. And a man does not need to do it alone. Experiences gathered from other men and principles reasoned by other men can all be a man's source of new knowledge. To say a man acting on principle is simple is a grotesque defamation, and we must be ready to rebuke it immediately.

Of course, that is not to say a man is not fallible. After all, man and all men's experience is expanding, thanks to our growing wealth of knowledge. Newton's law of gravity was not wrong, in the face of the theory of general relativity, but a knowledge applicable under a specific context that men had not known otherwise. It is not a repudiation of man's capability of reason but an endorsement of men's ability to continually expand our understanding of reality.

So, a principle is a basic generalization, and can men know it? Absolutely.

Goodbye, the Waystation Crypto Libertarians!

It is Stephan Kinsella, one of the authoritative living minds in libertarian legal theory, who coined the term "waystation libertarians" as "Someone who was only 'passing through' libertarianism on their meandering, endless journey through ideologies and faddish, dilettantish interests."

As someone who has been in the libertarian movement actively for almost a decade and is currently retreating to a side project named "Mission: Liberty" due to time conflicts, I should like to have something to say about it.

Considering all other waystation libertarian movements during my time, Ron Paul libertarians, Sound Money (Goldgug or Bitcoin) libertarians, NatCon/Trump libertarians, Crypto libertarians, Covid libertarians, and now Milei libertarians, what I have been entangling my life the most is the sound money and crypto libertarians, where my startup is a business that surviving the post-SBF crypto winter. I have a growing grudge against the crypto libertarians, which I will explain in a moment. But similar to Mr. Kinsella's realization, I really should not.

I will put out my conclusion: the crypto libertarian movement is dead. If it's comforting to hear in a somewhat perverse way, its predecessor, the Sound Money/Bitcoin libertarians movement, is barely limping along, where the biggest hopes are that Blackrock can create an ETF and buy their digital gold! What an abomination!

In fairness, for the libertarian meetups I organize or go to, the Bitcoin movement remains the most activism-oriented and keeps bringing in new energy. Undoubtedly, Saifedean Ammous's works "The Bitcoin Standard" and "Principles of Economics" have inspired young minds to get into the idea of sound money, the Austrian school of thought in economics, and rational individualism.

But crypto libertarians, with its ever-moving targets (and some comical sagas along its way) - from native internet of money to stablecoins backed by fiat; from crowdfunding to VC-backed; from fully decentralized to sufficiently decentralized; from lemonade coin to decentralized physical infrastructure (DePIN!); from peer-to-peer decentralized operating systems (e.g. Urbit) to decentralized social (DeSo!); the list goes on - it is a rather elusive term that after a while, just like other waystation movements, it might have never existed!

So it is perhaps instead, the hope that it ever can exist is dead. In the face of this, anyone can justify their emotion. Anger: how we end up here where no one cares to promote our ideas. Sad and self-pity: how we didn't know better when we brought in detractors and fraudsters. Cynical: libertarian objectives will forever remain fringe. Jealous: look at the ones who joined and made the money; if I had the money, I should fund a movement myself!

There can be an indifferent emotion: it is just what it is. But it is a nonproductive emotion. While I believe the most practical and positive emotion and attitude to the matter is a subtle one. That is a skillful play between a rational acceptance and a wise realization of the libertarian movement under the historical context. Understanding the waystation phenomenon of movement is essential for anyone to come to this realization.

It is a relieving realization and practical attitude:

• If you are still deep in the crypto industry like me, stop thinking about it still being part of the libertarian movement anymore, focus on what is in it for you, and get the job done.
• Think of the whole libertarian movement as a non-stopping train to a destination in which we all share the same faith. Let's welcome the passengers along the waystations we pass through and wish them all good fortune after they hop off.
• To quote a motto of mine from an ancient book of wisdom: "I have fought a good fight, I have finished my course, I have kept the faith."

P.S.

Congrats to Milei, and let us wholeheartedly welcome the upcoming Milei libertarians at our next stop!

A Solidity Compilers Collection in Nix

I have written solc.nix for a while, this article is a summary of it.

It is a collection of solidity compilers as nix expressions. While most solidity development toolchains (foundry, truffle, hardhat, etc.) have their bespoke mechanisms of downloading solidity compiler (solc) binaries, there are situations you would want not to rely on them:

• In a CI environment, you provide the compiler during setup instead of letting toolchains download them again.
• You have a development process that does not have the solc resolution mechanism.
• You are juggling with multiple versions of solidity compilers.
• You are using NixOS or the "Nix package manager".

If any of these cases apply to you, you should consider using solc.nix. Here are some tips on how.

$ nix shell github:hellwolf/solc.nix#solc_0_4_26 github:hellwolf/solc.nix#solc_0_8_19

$ solc-0.4.26 --version
solc, the solidity compiler commandline interface
Version: 0.4.26+commit.4563c3fc.Linux.g++

$ solc-0.8.19 --version
solc, the solidity compiler commandline interface
Version: 0.8.19+commit.7dd6d404.Linux.g++

{
  inputs = {
    solc = {
      url = "github:hellwolf/solc.nix";
      inputs.nixpkgs.follows = "nixpkgs";
    };
  };

  outputs = { self, nixpkgs, solc }: let
    pkgs = import nixpkgs {
      system = "x86_64-linux";
      overlays = [
        solc.overlay
      ];
    };
  in {
    devShell.x86_64-linux = with pkgs; mkShell {
      buildInputs = [
        solc_0_4_26
        solc_0_7_6
        solc_0_8_19
        (solc.mkDefault pkgs solc_0_8_19)
      ];
    };
  };
}

My Haskell Tiny Game Jam Submissions: Othello & Lol

This post is a last-minute write-up for my participation in the Haskell Tiny Game Jam. The goal was to implement a game that fits into 10 lines of 80 characters. I have submitted two entries: one is a mini-othello game, the other is a meta game called "lol".

Mini Othello

It is a minimum Othello game implementation with MiniMax "AI" opponent using GHC 9.X with only the "prelude" module allowed.

The rule of the game is: "There are sixty-four identical game pieces called disks, which are light on one side and dark on the other. Players take turns placing disks on the board with their assigned color facing up. During a play, any disks of the opponent's color that are in a straight line and bounded by the disk just placed and another disk of the current player's color are turned over to the current player's color. The objective of the game is to have the majority of disks turned to display one's color when the last playable empty square is filled." (https://en.wikipedia.org/wiki/Reversi)

To play the game, checkout the tiny game repository and type ./play mini-othello:

I implemented the game entirely in minified code, so the variable and function names will be pretty cryptic!

Functions Overview

First, I represent the game state with a product type of Board and Side (only conceptually, but without actual code):

type Side = Black | White | None
type Coordinate = (Int, Int) -- from (0,0) to (7,7)
type Board = [Char] -- 64 of them!
-- | Game state type alias
type GameState = (Board, Side)

n = "_XO" -- visually they are reprensed these chars.

Then I implemented a helper function v for checking the number of flips per each line. There are 8 different directions the line can go, they are all enumerable by a StepCoordinate type.

-- number of steps (-1,0 or 1) in each direction to represent 8 different directions.
type StepCoordinate = (Int, Int)

-- | Check number of flips for one single direction
v :: GameState -> (GameState, Int) -> Coordinate -> StepCoordinate -> State
  -> (GameState, Int)
v savedGameState (currentGameState, nFlips) cor stepCor state
  -> (newGameState, nFlips)

Then the % operator for trial plays. Because this is used so often, the usage of this binary operator saves a lot of spaces!

(%) :: GameState -> Coordinate -> (GameState, Int)
(%) inGameState -> cor -> (outGameState, nFlips)

The q function moves the game state to the next round.

-- | Play and move to next round
q :: GameState -> Coordinate -> GameState
q currentGameState -> cor -> nextRoundGameState

The z function starts the game in the IO monad.

-- | Start game
z :: Side -> GameState -> IO ()
z humanSide (initialBoard,currentSide)

The e function is the game strategy for the AI:

-- | Strategy function!
e :: GameState -> GameState

It should use the q function to move the game state forward.

There are three game strategies attempted during the code jam:

1. A naive strategy that finds the first possible move.
2. A greedy strategy that finds the immediate move that flips the most pieces.
3. A MiniMax strategy that tries to play the game with a few levels of depth with MiniMax decision rules.

I will enlist the code of (3) here. And because of its minified nature, it looks pretty hideous, I admit:

g h a=f(\c e->i e>i c?e$c)(-65*h,(0,0))$
        (\((b,p),d)->(h*(h*p==0?j a`c`i b$i$g(div h(-2))b),d))&
        (((,)=<<(a%))&k r);
e a=q a.j$g 4a

Here g 4a is a recursive function starting with 4, and it oscillates between positive ("max" stage) and negative ("min" stage) and halves at the same time (g -2a, then g 0a). This is a trick to use a single number to represent the stage and depth limit of the minimax process.

The evaluation function is kept simple; the more flips, the better. In a better strategy, certain pieces are worth more (at the corner or at the side).

Code Golfing Tricks

Compact Ternary Operator (Prelude)

If you use a lot of if then else, use this test?yes$no to save a lot of spaces:

infixr 1?;(b?x)y|b=x|0<3=y;

If you are not limited to using only "prelude" module, you might also use bool :: a -> a -> Bool -> a in base.

Shortest Function for "Other Side"

o=1:2:o, so that o 1=2 and o 2=1. Any other output is uninteresting!

This is a funny function enabled by Haskell's lazy evaluation semantics.

Shortest Cross Product Function

k=(<*>)=<<((,)<$>), so that:

1. k[-1..1] is for interacting through all 8 directions ([1,1],[1,0],[1,-1],[0,1],[0,-1][-1,-1],[-1,1],[-1,0]), the 9th direction [0,0] is uninteresting and doesn't create trouble fur us.
2. k[0..7] generates all 64 positions on the board for iterating through them.

The alternative would be using twice List applicative; this version saves spaces!

Make a move

This bizarre ternary function put a piece "w" at position "i" on the board "b":

(w^i)b=take i b++w:drop (i+1)b;

Other Ad-hoc One-Letter Functions

More tips about minifying and unminifying techniques can be found at: https://github.com/haskell-game/tiny-games-hs/issues/52

Lol - The Meta Game

My second submission to the game jam is less serious. In fact, it is a knock-off of the lolcat program! But it is tightly integrated with the game itself, hence a meta game!

The idea of it is straightforward: it pipes the "play" command to colorize its output and add additional text effects depending on how many "lols" you have inserted in the command line, e.g.:

./play lol lol lol lol lol ski would give you a rather trippy ski trip:

The trick of using the applicative list to generate an infinite list of variations:

(,,)<$>[1..]<*>s[38,48]<*>s[0,4,5]

The first parameter is the frequency of the rainbow color effects; the second one is the anis-terminal color code choice for foreground or background; the third one is additional text effects such as underlined texts and blinking texts.