Efficient type-level division for Haskell

Another approach I wanted to explore to Encsé's 9-digit problem was creating a type-level solution in Haskell. First I'll describe what that would entail, and then present a solution to one of its sub-problems: testing special cases of divisibility in a more efficient way than the naïve implementation of repeating subtractions.

Type-level programming

Basically, a type-level Haskell program is to regular Haskell programs what C++ template metaprograms are to C++ proper. Conrad Parker wrote a great introduction to type-level programming using functional dependencies in issue 6 of The Monad.Reader journal, titled Type-Level Instant Insanity. You encode values as types, and then construct an expression whose type, as inferred by the Haskell compiler, encodes the output of your computation. To actually implement the equivalent of a function, typeclasses are used.

For example, take the following (value-level) Haskell definition of length: (deliberately not using any builtin types, and using unary representation for simplicity):

module ValueLength where
        
data Nat = Z | S Nat      
data List a = Nil | a ::: (List a)
infixr 6 :::

length :: List a -> Nat
length Nil = Z
length (x ::: xs) = S (length xs)
      

(note that due to technical limitations, both : and :: are reserved names in Haskell, and so we have to use ::: for our cons)

To lift this definition to the level of types, we first need a way to represent actual numbers and lists as types. This is pretty straightforward using algebraic datatypes. Since we are ultimately only going to be interested in the type of expressions and not their value, no constructors are defined.

{-# LANGUAGE EmptyDataDecls, TypeOperators,
             FunctionalDependencies,
             MultiParamTypeClasses, UndecidableInstances #-}
module TypeLength where

data Z
data S n

data Nil
data x ::: xs
infixr 6 :::

-- Continued below
      

Compiling Haskell into C++ template metaprograms

After Lőri posted his C++ template meta-program solution to the 9-digit problem, Encsé asked me to help him understand it, being the first real-world metaprogram he's encountered. To help both him and myself, I rewrote, function-by-function, his code into Haskell.

This rewriting process was surprisingly straightforward, and the resulting code, while being in a very strict one-to-one correspondence with the original C++ code, was immensely more readable. So this, naturally, lead to the idea of a simple functional programming language that could be compiled into C++ compile-time metaprograms.

A couple of days later, I had a small accident and had to stay in bed for a week, which gave me plenty of time to throw together a proof-of-concept compiler from a Haskell-like language into C++ TMP.

And so MetaFun was born.

MetaFun is structured into three separate modules, one for parsing and typechecking the input language called Kiff (for Keep It Fun & Functional), one for unparsing C++ metaprograms, and the third one is, of course, the compiler itself. I plan to re-use the Kiff module whenever I come up with an idea for another new throwaway functional compiler.

Unary arithmetics is even slower than you'd expect

My coworker Encsé posted a challange use the 9-digit number problem to demonstrate interesting programming techniques. So I sat down and wrote my first practical program using dependant types, in Agda. I've been playing around with Agda previously, but this seemed like a good opportunity to try to write an actual, self-contained, provably correct program with it.

I'm not going to get into details now about the resulting Agda code, because I'm planning to present it in detail in a later post. In its current form, my program is formally proven to produce only good nine-digit numbers; the only property that still needs proving is that it finds all of them.

But the sad surprise came when I tried to actually run it. It was unbearably slow to just get to all possible combinations for the first three digits. I'm talking about 12 minutes just to list them from 123 to 423 (at which point I killed the process). For comparison, the following Haskell program, which is an implementation of the same naïve algorithm, finds the (unique) solution in 4 milliseconds:

import Control.Monad.List

fromDigits = foldr shift 0
    where shift d s = 10 * s + d

p `divides` q = q `mod` p == 0

encse :: [Int]
encse = map fromDigits $ encse' 0 []
    where encse' 9 ds = return ds
          encse' n ds = do d <- [1..9]
                           let ds' = d:ds
                               n' = n + 1
                           guard $ not (d `elem` ds)
                           guard $ n' `divides` fromDigits ds'
                           encse' n' ds'
      

So where's that slowdown coming from?

The first intuition would be that the code generated by Agda is slow because in parallel to the actual computation, it is also evaluating all kinds of proofs. But the proofs exist only in the world of types, so they shouldn't matter once the program is compiled.

The real answer is that calculating in unary representation is slow. Very, very slow. Even slower than you'd imagine.

Neked aztán lehet

Ezt Viki mesélte, de szerintem érdemes ide is.

Az az alaphelyzet, hogy a suli mellett az ELTÉn dolgozik operátorként. Keveset operál, annál többet kell segítenie random ELTÉs oktatóknak akiknek "nem megy a levelezés". Szóval endless fun. Most viszont becsúszott egy jó sztori.

Bölcsészmérnök felhívja telefonon az operátori szolgálatot valami fájással, mondják neki hogy azonosítás végett küldjön egy levelet a benti címéről (ugyanis az SMTP autentikált). Persze, hogy leírja a levélben a jelszavát is. Válaszolnak neki hogy jó, akkor most mielőtt bármi egyéb történik, letiltották a jelszavát mert kiadta, itt meg itt tud ETR-en keresztül újat választani (remélhetőleg az ETR-es hozzáférését még nem adta ki senkinek).

Mivel ez már bőven túl bonyolult volt neki (amúgy én azt is el tudom képzelni, hogy azt hitte, szivatásból tiltották le), bement személyesen az irodába. Ott Viki elmondta neki az alábbi 3 (három) információt:

• Ne legyen a jelszóban ékezetes betű
• Nem praktikus, ha van benne y vagy z betű
• Soha senkinek, az operátori szolgálatnak se adja ki a jelszavát. Sosenem.

Különösebben hosszú gondolkodási idő nélkül vágta erre rá az alábbi, azóta nálunk szállóigévé vált mondatot:

Akkor lehet a jelszavam az, hogy "prüntyőke"?

Internet-celebritás lettem...

... pedig nem is tudtam róla.

Ez a mostani sztori kb. egy hete kezdődött, amikor ránéztem a Google Analytics oldalon a honlapom napi látogatóinak számára, és az alábbi grafikont láttam (a mellbevágóbb hatás kedvéért itt most fél évre visszamenőleg látszanak az adatok):

Adja magát a kérdés, hogy mégis mi az isten történt január végén-február elején, amitől, hirtelen, a hatszorosára ugrott a látogatottságom, és utána is csak lassan csörgedezik vissza a megszokott szintre. Első blikkre csak annyi látszott, hogy a Google képkereső a fő forrása a forgalomnak, konkrétan pedig a domb szóra rákeresve talált rá ez a hirtelen jött sokaság erre a fotóra.

Ennél több akkor, egy hete nem is derült ki. Elkönyveltem magamban azzal, hogy hát a "domb" egy elég gyakori, egyszerű szó, és valóban ez a kép a második-harmadik a keresési eredmények között, úgyhogy ha sokan keresnek fotókat dombokról, miért is ne néznék meg az első néhány találatot.

Aztán tegnap kaptam egy emailt egy ismeretlen embertől: