The one advantage dynamic typing pundits seem to bat around with little resistance is that types get in the way of their prototyping, or deciding how they plan to write a program. This cannot be true after the first handful of functions have been written; it is simply impossible for humans to track the explosion of possible function bodies dynamic typing allows.

I was fleshing out these ideas with my friend Louis van der Stam. We found the final numbers somewhat impressive…

Let’s first quickly brush over cardinality: let’s consider the type `Boolean`

has cardinality `2`

and that the type `Byte`

has cardinality `256`

. This is because there are `256`

possible elements of type Byte… We will use the vertical bars like | to show this: `|Byte| = 256`

. But in an dynamic languages values have no clear type and lets use say any variable has an infinite possibility of values so it can hold `|var| = ⍵`

. …

Software Architecture is getting too complicated…

It is easy to look at all those design pattern books, and online articles about hexagonal architectures, or the cake pattern, or the onion architecture and get lost on how you are best able to design applications and services in a world driven by docker containers, edge computing and serverless architectures.

There must be a way to cut through all the noise and get to some core principles that have a more rigorous mathematical defense…

This article is the introduction in a three part series about algebra and software development.

Why don’t we just go back to basics for a minute and talk about algebra. The very same topic we all took in high-school where we were first presented with the notion of variables and factoring expressions out thanks to known properties on the operations we were doing. …

I want to chime in on the sleeping Giant that are Lenses and Prisms in software development:

They are probably the most powerful unused tool in our arsenal!

Optics can be the perfect bridge from Algebraic Data Types to the Functor hierarchies and beyond. They can the prism (could not resist the pun) through which you can peek into useful and concrete applications of more abstract ideas; once you understand the connection between:

- tuples and functions
- products and powers
- conjunction and implication

Optics is a very concrete and visceral connection between computation and logic. …

In functional programming, and fervent advocates of strongly typed languages it is common to hear phrases like: “It compiles; ship it!” or “I don’t need to run it, I already know it compiles”, referring to this notion of being able to write code that gets formally verified by the compiler’s type system. …

Type systems, and more importantly, type checkers, are invaluable to how someone could go through understanding how any given codebase works. They might consider typing errors as guard rails as they start wrapping their mind around the expected computational outcomes of any given code block they are examining.

It is a stark contrast to the proposition of working without any obvious contracts, expectations, or local invariants as is more common in un-typed scenarios like javascript, ruby or pearl.

The explorations done under these guard rails, when computation can be cleanly connected to category theory, different type theories, and certain logics, gives predictive power beyond a few trial runs in someone’s head or on a typical repl session. …

About