Recent content on Mathematics and Machines
Futamura Projections are usually described with a lot of words, but they are much simpler to understand in types. There are Interpreters, Compilers, and Specializers: a -> b -- Specialized Machine (a -> b)' -> a -> b -- Interpreter (a -> b)' -> (a -> b) -- Compiler (a -> b -> c)' -> a -> (b -> c) -- Specializer Futamura 1: Specializing an Interpreter at a Program results in an Executable
Here is a fun little exercise: show that any two perfectly correlated Bernoulli random variables \(X\) and \(Y\) must be equal. Proof: The assumption can be stated as $$\frac{Cov(X, Y)}{\sigma_X \cdot \sigma_Y} = 1$$ Let \(Z_X = (X - \mu_X) / \sigma_X\), \(Z_Y = (Y - \mu_Y) / \sigma_Y\) be the standardizations so that \(\mathbb{E}(Z_X) = 0\), \(Var(Z_X) = 1\), and similarly for \(Z_Y\). Then we…
The phrase “Make Illegal States Unrepresentable” has caught fire in the functional programming world after being coined by Yaron Minsky in 2011. It’s clear enough how to accomplish this for individual subsystems: given a component \(C\) with state \(C_S\), it’s just a matter of defining \(C_S\) so that illegal states literally cannot be represented by its type. This could…
The comonad reader has a lovely article about the proper definition of free monoids in the category of Haskell types. By thinking about universal properties in category theory, it is easy to see that the proper type for \(f a\), the free monoid on any type “a”, is given by $$f a = \forall m. \textrm{Monoid } m \Rightarrow (a \to m) \to m.$$ This definition is obviously implicit: the…
Currently, most popular approaches to software testing used by developers consist of unit-testing frameworks such as NUnit/JUnit and the like. Putting the debate between mockist and classicist testing aside for the moment, I think it’s useful to step back and ask ourselves what tests are, and why we have evolved into these testing patterns. To me, a test consists of an evaluation of a system…
The other day I was trying to find if joining two Map k structures together fell under a suitable abstraction. Following Conal Elliott, we start from the fact that every Map k a can be regarded as a partial function k -> a determined by a list of pairs (k_i, a_i), and therefore as a total function k -> Maybe a. But Maybe a is a monad and k-> is a monad transformer to a Reader, so certainly…
I’ve been doing some coding in Scala just to get some experience with functional programming on the JVM, and part of this has involved bringing in useful abstractions from Haskell as I needed them (scalaz notwithstanding). Lately I ran into a pattern where the initial versions of some of my functions returned something of type Maybe [a], only to apply the mapping Nothing -> [] and Just xs ->…
Michael Snoyman has observed that Set is not a functor. This is kind of surprising if your initial hope is that Set is a Monad! To the mathematically inclined: Set in Haskell represents not a category but rather a type constructor of kind * -> *. At a type a, Set a is the type of sets of elements all of type a. So, given a map f: a -> b, why can’t we get an induced map fmap f: Set a -> Set…
The polymorphic list type [a] can be modeled as List a = Empty | Cons a (List a) which looks an awfully lot like \(L = 1 + X\cdot L\). The corresponding geometric series yields a closed form expresssion \(L = \frac{1}{1-X}\) and the derivative with respect to \(X\) is $$L’ = -\frac{1}{(1-X)^2}\cdot(-1) = \frac{1}{(1-X)^2} = L^2$$ Thus the derivative of \(L\) can be modeled as a list of all…
Just recently I discovered a simple solution to an issue I encountered when developing parts of my directed-cubical library. A very common pattern in the code was to apply a function f: a -> a repeatedly to an initial value x until the value stabilized, or in other words to find a fixed point. The type signature of such a function looks something like stabilize :: (Eq a) => (a -> a) -> a -> a…
If you import Data.Function, you’ll find that the function fix has a funny type: fix :: (a -> a) -> a Given a function f, the value fix f will be “the” fixed point of f. I think this means the least fixed point, which for some reason is supposed to correspond to the greatest fixed point in Haskell, but I’ve still not quite understood enough domain theory to explain why.
If we think of a “personName” as a possible name for a person, then semantically it carries more information than just being an arbitrary String. Arbitrary strings are, well, arbitrary! Even if we really thought that people could have arbitrary strings as their names, the fact that they are names (meaning that they are intended to be used as names) means that they should have a type…
We are told by the documentation of Data.Foldable that, at a minimum, a foldable instance must implement the foldMap function, whose signature is foldMap :: Monoid m => (a -> m) -> t a -> m The fact that m is an arbitrary monoid allows us to determine the underlying order in which elements are combined. To wit, consider the following perfectly good foldable instances on lists: newtype FoldList a =…
An aperiodic semigroup is a semigroup \(S\) such that for every element \(x \in S\) there exists some \(n \in \mathbb{N}\) such that \(x^n = x^{n+1}\). They are distinguished among semigroups by being the most un-grouplike of all: they contain no non-trivial subgroups! Conversely, if a finite semigroup contains no non-trivial subgroups then it must be aperiodic. One direction is slightly easier…
Finite semigroups are important in computer science in particular because they can represent composition of state transitions of deterministic automata, including non-invertible transitions. From an algebraic perspective they are interesting because they can be very un-grouplike: for example, many interesting examples of semigroups have non-trivial idempotent elements, so that \(x^2 = x\) is…
The term ETL stands for Extract, Transform, and Load. In a database it is very common to Extract data from multiple sources (interior or exterior to the local database), Transform that data in some prespecified manner, and finally Load that transformed data into a destination resource such as a table. In SQL on relational databases, it seems to be common practice to have stored procedures handle…
There is an interesting monoid instance for Maybe a types whenever a is a monoid, which ignores Nothing and applies the underlying monoid under the Just. In Fizz-Buzz, Fizz is supposed to appear in place of every third number, and Buzz in place of every fifth number, but both should appear on every fifteenth number. So we can generate a fizzbuzz stream first, and then find a way to combine it with…
Suppose I want to write a function that takes a list together with one of its elements, and produces a new list of the same type. Here is a naive attempt at a type signature: f :: [a] -> a -> [a] Do you see the problem? There is no guarantee that the second argument is actually an element of the list, so f [1,2,3] 4 should not be a valid invocation of the function.
So, a modern way to do the natural numbers at the type level is to take advantage of the relatively recent DataKinds extension to GHC, which automatically promotes (many) types to kinds and their type constructors to constructors for these kinds. {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, GADTs #-} So here they are: -- | Type for natural numbers data Nat = Z | S Nat DataKinds…
I recently found this post about dealing with Renderable objects in the context of game design. The solution presented there introduced a composite type data Game = Game Ball Player Player where Ball and Player are instances of a typeclass Render a: class Render a where render :: a -> IO () Then one can write a function that renders a Game by pattern matching on the Game constructor. If the…
In imperative programming circles (particularly C++) there has been debate over whether it is better to use return values or exceptions to propagate information about exceptional conditions. First of all there is the usual distinction to be made between errors and exceptions: an error is an unexpected condition arising from a mistake in the program code, while an exception is an expected condition…
The Maybe monad is a certain endofunctor on the category of types. There is another endofunctor called Id on this category, and a natural transformation Just: Id -> Maybe. For any object a there is therefore a morphism Just: a -> Maybe a. There is another endofunctor, namely *, sending every type to the unit type (), and a natural transformation Nothing: * -> Maybe. To describe the monoid…
I recently read the paper on extensible effects in Haskell. It was good to see open union types being used for something like this, and the coroutine-based handlers seemed easy enough to write. Edward Kmett pointed out that it essentially looked like a CPSed free monad on a coproduct, much like a datatypes a la carte approach. Going over to read the original `a la carte paper explained some of the…
Today I decided to have a go at installing Yesod for the first time. I already had the Haskell Platform installed, so according to the tutorial I was supposed to run cabal update cabal install yesod yesod-bin cabal-dev and be on my merry way. Unfortunately, instead of having a functional Yesod installation I had instant Cabal hell. Doing yesod init set up the scaffolding fine, and it recommended a…
I finally got around to writing some code to output finite directed cubical complexes in VTK format. Initially I was trying to get it to work with the XTK project in hopes of getting some slick WebGL-based presentations, but XTK’s parser for VTK polydata files only supports triangles at the moment (rather than general polygons). I was able to partially work around this by rendering only the…
As an oddball way of “updating” my skills, I decided some 6 months ago to learn Vim. Of course, I had to debate over Vim vs. Emacs and other editors first, but I had used Emacs and relatives before and found their Ctrl/Meta-everything approach to keyboard shortcuts to be annoying. On the other hand, I had also had the classic Vim newcomer experience: you start Vim, and are immediately…
I’ve just released a new Haskell library on GitHub which I intend to get onto Hackage real soon now. It’s called “directed-cubical”, and it contains a couple of modules for creating, transforming, and reducing finite directed cubical complexes. The reduction algorithms are based on my forthcoming paper “Computing Path Categories of Finite Directed Cubical…
Coming from imperative languages, one of the biggest initial shocks with Haskell has to be the lack of loops (or more accurately, the lack of special syntactic sugar for them). Imperative loops are rather “unstructured” from a functional perspective: you set up a counter and then insert a bunch of effectful tasks to execute on each iteration that may or may not be related to each…
FizzBuzz is a fun little exercise for thinking about conditional statements. The Haskell versions over there were not quite the way I did it, so I figured I’d post a solution here: f x = if null fizzbuzz then show x else fizzbuzz where fizz = if x `mod` 3 == 0 then 'Fizz' else '' buzz = if x `mod` 5 == 0 then 'Buzz' else '' fizzbuzz = fizz ++ buzz main = putStr .
I am working on my first significant little project in Haskell; some code should appear on Github in the not-too-distant future. This has spawned some thoughts on the language as a whole: The Good Parts: Pure functions. This is probably the single biggest win versus most mainstream languages. If you don’t believe me, listen to John Carmack talk about his experience: youtube link. The ability…
Today I got my first true taste of dependency hell in Haskell, via cabal install (as expected). Actually it is rather easy to land in hell by attempting to cabal install anything outside of the batteries-included Haskell Platform, which is inevitable given that we all eventually want to use the latest of this-or-that package. My particular issue was kind of interesting: I wanted to use packages A,…
List processing and functional programming style have now come up more than once as a solution to my database programming woes, although by “list processing” I often just mean “set processing” (ordering only matters for the final resultset). I have found that the combination of the following two principles is very powerful for any type of software development: A function…
I was recently inspired by Lipton’s blog to have a look at a fun little problem about finite strings. Fixing an alphabet Σ, a finite string \(x\) over Σ is just a finite sequence of elements of Σ, and the length \(|x|\) of \(x\) is the number of elements appearing in this sequence. Given two strings \(x\) and \(y\) over Σ, there is a binary operation called concatenation which sends the pair…
My current job involves coding a lot of SQL queries and has had me thinking about relational database concepts in general. I have come to believe that SQL queries of 100 lines or less are “simple”, that queries of about 500 lines are moderately complex, and that queries of over 1000 lines indicate that one is starting to really use the language seriously (provided most of those lines…
I am trained as a mathematician (Ph.D., 2009) and currently work as a Machine Learning Architect specializing in business applications of statistics and ML. I enjoy partnering with businesses to strategically leverage their data. This is my blog so you’ll find a lot of my personal ramblings on mathematics, machine learning, statistics, and functional programming. None of them necessarily…