{"action":"created","comment":{"url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/comments/213610596","pull_request_review_id":150480561,"id":213610596,"node_id":"MDI0OlB1bGxSZXF1ZXN0UmV2aWV3Q29tbWVudDIxMzYxMDU5Ng==","diff_hunk":"@@ -0,0 +1,1100 @@\n+---\n+title: \"A dependently-typed binomial heap\"\n+description: Who put binary numbers in my type system?\n+tags: haskell\n+---\n+\n+Introduction\n+============\n+\n+This posts makes a bit of a departure from the \"practical Haskell\" I usually try\n+to write about, although -- believe it or not -- this blogpost actually\n+originated from a very practical origin [^practical-origin].\n+\n+[^practical-origin]: For [work], I recently put together an interpreter for a\n+lambda calculus that was _way_ faster than I expected it to be -- around 30\n+times as fast.  I suspected this meant that something was broken, so in order to\n+convince myself of its correctness, I wrote a well-typed version of it in the\n+style of Francesco's [well-typed suspension calculus] blogpost.  It used a\n+standard [length-indexed list](#vec) which had the unfortunate side effect of\n+pushing me into _O(n)_ territory for random access.  I started looking for an\n+asymptotically faster way to do this, which is how I ended up looking at heaps.\n+In this blogpost, I am using the binomial heap as a priority queue rather than a\n+bastardized random access skip list since that is what readers are presumably\n+more familiar with.\n+\n+[work]: https://fugue.co/\n+[well-typed suspension calculus]: https://mazzo.li/posts/suspension.html\n+\n+This blogpost is a literal Haskell file, which means you can just download it\n+and load it into GHCi to play around with it.  In this case, you can also verify\n+the properties we will be talking about (yes, GHC as a proof checker).  Since we\n+are putting our feet into dependent types territory here, we will need to enable\n+some extensions that are definitely a bit more on the advanced side.\n+\n+> {-# LANGUAGE DataKinds            #-}\n+> {-# LANGUAGE GADTs                #-}\n+> {-# LANGUAGE KindSignatures       #-}\n+> {-# LANGUAGE PolyKinds            #-}\n+> {-# LANGUAGE ScopedTypeVariables  #-}\n+> {-# LANGUAGE TypeFamilies         #-}\n+> {-# LANGUAGE TypeOperators        #-}\n+> {-# LANGUAGE UndecidableInstances #-}\n+\n+Since the goal of this blogpost is mainly educational, we will only use a few\n+standard modules and generally define things ourselves.  This\n+also helps us to show that there is no\n+[magic](https://github.com/ekmett/constraints/blob/5ffe5e7da8249eb3adbc0a735c039e75a7feab65/src/Data/Constraint/Nat.hs#L70)\n+[going on](http://hackage.haskell.org/package/base-4.11.1.0/docs/Unsafe-Coerce.html#v:unsafeCoerce)\n+behind the scenes: all term-level functions in this file are total and\n+compile fine with `-Wall`.\n+\n+> import           Data.List          (intercalate, minimumBy)\n+> import           Data.List.NonEmpty (NonEmpty (..))\n+> import qualified Data.List.NonEmpty as NonEmpty\n+> import           Data.Ord           (comparing)\n+\n+I assume most readers will be at least somewhat familiar with the standard\n+length-indexed list:\n+\n+<div id=\"vec\"></div>\n+\n+> data Nat = Zero | Succ Nat deriving (Show)\n+>\n+> data Vec (n :: Nat) a where\n+>     VNull :: Vec 'Zero a\n+>     VCons :: a -> Vec n a -> Vec ('Succ n) a\n+\n+These vectors carry their length in their types.  In GHCi:\n+\n+~~~~~\n+*Main> :t VCons \"Hello\" (VCons \"World\" VNull)\n+Vec ('Succ ('Succ 'Zero)) [Char]\n+~~~~~\n+\n+This blogpost defines a similar way to deal with [binomial heaps].  Binomial\n+heaps are one of my favorite data structures because of their simple elegance\n+and the fascinating way their structure corresponds to binary numbers.\n+\n+[binomial heaps]: https://en.wikipedia.org/wiki/Binomial_heap\n+\n+We will use this idea to lift **binary numbers to the type level** -- which is\n+great because we get _log(n)_ size and time in places where we would see _n_ for\n+the Peano numbers defined above (in addition to being insanely cool).  In GHCi:\n+\n+~~~~~\n+*Main> :t pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $\n+            pushHeap 'd' $ pushHeap 'e' emptyHeap\n+Heap ('B1 ('B0 ('B1 'BEnd))) Char\n+~~~~~\n+\n+Where _101_ [^reverse-101] is, of course, the binary representation of the\n+number 5.\n+\n+[^reverse-101]: Too be pedantic, for reasons that will become later, the binary\n+numbers that pop up on the type level should be read right-to-left, so a\n+palindrome was chosen as example here to avoid having to explain that at this\n+point.\n+\n+In short, this blogpost is meant to be an introductory-level explanation of a\n+non-trivial (and again, insanely cool) example of dependent Haskell programming.\n+\n+Table of contents\n+-----------------\n+\n+1.  [Introduction](#introduction)\n+2.  [Singletons and type equality](#singletons-and-type-equality)\n+3.  [Binomial heaps: let’s build it up](#binomial-heaps-lets-build-it-up)\n+    a.  [Binomial trees](#binomial-trees)\n+    b.  [Type level binary numbers](#type-level-binary-numbers)\n+    c.  [Binomial forests](#binomial-forests)\n+    d.  [The binomial heap](#the-binomial-heap)\n+4.  [Binomial heaps: let’s break it down](#binomial-heaps-lets-break-it-down)\n+    a.  [Taking apart a single tree](#taking-apart-a-single-tree)\n+    b.  [More Vec utilities](#more-vec-utilities)\n+    c.  [Popcount and width](#popcount-and-width)\n+    d.  [Lumberjack](#lumberjack)\n+    e.  [Lumberjack: final form](#lumberjack-final-form)\n+    f.  [popHeap: gluing the pieces together](#popheap-gluing-the-pieces-together)\n+5.  [Appendices](#appendices)\n+    a.  [Appendix 1: runtime cost of this approach](#appendix-1-runtime-cost-of-this-approach)\n+    b.  [Appendix 2: “pretty”-printing of heaps](#appendix-2-pretty-printing-of-heaps)\n+    c.  [Appendix 3: left-to-right increment](#appendix-3-left-to-right-increment)\n+\n+Singletons and type equality\n+============================\n+\n+If I perform an appropriate amount of hand-waving and squinting, I feel\n+like there are two ways to work with these stronger-than-usual types in Haskell.\n+We can either make sure things are correct by _construction_, or we can come\n+up with a _proof_ that they are in fact correct.\n+\n+The former is the simpler approach we saw in the `Vec` [snippet](#vec): by using\n+the constructors provided by the GADT, our constraints always are satisfied.\n+The latter builds on the [singletons] approach introduced by Richard Eisenberg\n+and Stephanie Weirich.\n+\n+[singletons]: https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf\n+\n+We need both approaches for this blogpost.  We assume that the reader is\n+somewhat familiar with the first one, and in this section we will give a brief\n+introduction to the second one.  It is in no way intended to be a full tutorial,\n+we just want to give enough context to understand the code in the blogpost.\n+\n+If we consider a closed type family for addition of natural numbers (we are\n+using an `N` prefix since we will later use `B` for addition of binary numbers):\n+\n+> type family NAdd (x :: Nat) (y :: Nat) :: Nat where\n+>     NAdd ('Succ x) y = 'Succ (NAdd x y)\n+>     NAdd 'Zero     y = y\n+\n+We can trivially define the following function:\n+\n+> data Proxy a = Proxy\n+>\n+> cast01 :: Proxy (NAdd 'Zero x) -> Proxy x\n+> cast01 = id\n+\n+`NAdd 'Zero x` is easily reduced to `x` by GHC since it is simply a clause of\n+the type family, so it accepts the definition `id`.  However, if we try to write\n+\n+~~~~~{.haskell}\n+cast02 :: Proxy (NAdd x 'Zero) -> Proxy x\n+cast02 = id\n+~~~~~\n+\n+We run into trouble, and GHC will tell us:\n+\n+~~~~~\n+Couldn't match type ‘x’ with ‘NAdd x 'Zero’\n+~~~~~\n+\n+We will need to prove to GHC that these two types are equal -- commutativity\n+doesn't come for free!  This can be done by providing evidence for the equality\n+by way of a GADT constructor [^data-type-equality].\n+\n+[^data-type-equality]: This type and related utilities are found in\n+[Data.Type.Equality](http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Type-Equality.html),\n+but redefined here for educational purposes.\n+\n+> data EqualityProof (a :: k) (b :: l) where\n+>     QED :: EqualityProof a a\n+>\n+> type a :~: b = EqualityProof a b\n+\n+Take a minute to think about the implications this GADT has -- if we can\n+construct a `QED` value, we have actually provided evidence that the two types\n+are equal.\n+\n+The `QED` constructor lives on the term-level though, not on the type level.  We\n+must synthesize this constructor using a term-level computation.  This means we\n+need a term-level representation of our natural numbers as well.  This is the\n+idea behind of _singletons_ and again, a much better explanation is in that\n+paper among some [talks](https://www.youtube.com/watch?v=rLJ_YyVRKzs), but I\n+wanted to at least give some intuition here.\n+\n+The singleton for `Nat` is called `SNat` and it's easy to see that each `Nat`\n+has a unique `SNat` and the other way around:\n+\n+> data SNat (n :: Nat) where\n+>     SZero :: SNat 'Zero\n+>     SSucc :: SNat n -> SNat ('Succ n)\n+\n+We can use such a `SNat` to define a proof for what we were trying to\n+accomplish.  Since this proof can be passed any `n` in the form of an `SNat`, it\n+must be correct for all `n`.\n+\n+> lemma1 :: SNat n -> NAdd n 'Zero :~: n\n+\n+GHC can figure out the base case on its own by reducing `NAdd 'Zero 'Zero` to\n+`'Zero`:\n+\n+> lemma1 SZero = QED\n+\n+And we can use induction to complete the proof.  The important trick here is\n+that in the body of the pattern match on `EqualityProof a b`, GHC knows that `a`\n+is equal to `b`.\n+\n+> lemma1 (SSucc n) = case lemma1 n of QED -> QED\n+\n+This can be used to write `cast02`:\n+\n+> cast02 :: SNat x -> Proxy (NAdd x 'Zero) -> Proxy x\n+> cast02 snat = case lemma1 snat of QED -> id\n+\n+`cast02` takes an extra parameter, and there are several ways to synthesize this\n+value, the common one being a typeclass that can give us an `SNat x` from a\n+`Proxy x`.  In this blogpost, however, we keep things simple and make sure we\n+always have the right singletons on hand by passing them around in a few places.\n+In other words: don't worry about this for now.\n+\n+Binomial heaps: let's build it up\n+=================================\n+\n+Binomial trees\n+--------------\n+\n+A _binomial heap_ consists of zero or more _binomial trees_.  I will quote the\n+text from the Wikipedia article here since I think it is quite striking how\n+straightforward the definition translates to GADTs that enforce the structure:\n+\n+- A binomial tree of order 0 is a single node\n+- A binomial tree of order k has a root node whose children are roots of\n+  binomial trees of orders k−1, k−2, ..., 2, 1, 0 (in this order).\n+\n+> data Tree (o :: Nat) a where\n+>     Tree :: a -> Children o a -> Tree o a\n+\n+> data Children (o :: Nat) a where\n+>     CZero :: Children 'Zero a\n+>     CCons :: Tree o a -> Children o a -> Children ('Succ o) a\n+\n+Some illustrations to make this a bit more clear:\n+\n+![Illustration of trees of different sizes, with the children array marked in\n+green](/images/draft-01.png)\n+\n+This is definitely a very good example of the correctness by construction\n+approach I talked about earlier: it is simply impossible to create a tree that\n+does not have the right shape.\n+\n+Empty trees do not exist according to this definition.  A singleton tree is\n+easy to create:\n+\n+> singletonTree :: a -> Tree 'Zero a\n+> singletonTree x = Tree x CZero\n+\n+We only need to define one operation on trees, namely merging two trees.\n+\n+A tree of order `o` has `2ᵒ` elements, so it makes sense that merging two trees\n+of order `o` creates a tree of order `o+1`.  We can see this in the type\n+signature as well:\n+\n+> mergeTree :: Ord a => Tree o a -> Tree o a -> Tree ('Succ o) a\n+\n+Concretely, we construct the new tree by taking either the left or the right\n+tree and attaching it as new child to the other tree.  Since we are building\n+heap to use for as a priority queue, we want to keep the smallest element in the\n+root of the new tree.\n+\n+> mergeTree l@(Tree lroot lchildren) r@(Tree rroot rchildren)\n+>     | lroot <= rroot = Tree lroot (CCons r lchildren)\n+>     | otherwise      = Tree rroot (CCons l rchildren)\n+\n+![Merging two trees.  Since 'a' is smaller than 'b' we attach the 'b' tree as a\n+new child to the 'a' tree.](/images/draft-02.png)\n+\n+Type level binary numbers\n+-------------------------\n+\n+With these trees defined, we can move on to _binomial heaps_.\n+\n+While binomial trees are interesting on their own, they can really only\n+represent collections that have a number of elements that are exactly a power of\n+two.\n+\n+Binomial heaps solve this in a surprisingly simple way.  A binomial heap is\n+a collection of binomial trees where we may only have at most one tree for every\n+order.\n+\n+This is where the correspondence with binary numbers originates.  If we have a\n+binomial heap with 5 elements, the only way to do this is to have binomial\n+trees of orders 2 and 0 (2² + 2⁰ = 5).\n+\n+We start out by defining a simple datatype that will be lifted to the kind\n+level, just as we did with `Nat`:\n+\n+> data Binary\n+>     = B0 Binary\n+>     | B1 Binary\n+>     | BEnd\n+>     deriving (Show)\n+\n+It's important to note that we will represent binary numbers in a right-to-left\n+order since this turns out to match up more naturally with the way we will be\n+defining heaps.\n+\n+For example, the type:\n+\n+~~~~~~\n+B0 (B1 (B1 BEnd))\n+~~~~~~\n+\n+represents the number 6 (conventionally written _110_).\n+\n+I think it is fairly common in Haskell for a developer to play around with\n+different ways of representing a certain thing until you converge towards an\n+elegant representation.  This is many, many times more important when we are\n+dealing with dependently-typed Haskell.\n+\n+Unelegant and awkward data representations can make term-level programming\n+clunky.  Unelegant and awkward type representations can make type-level\n+programming downright infeasible due to the sheer amount of lemmas that need to\n+be proven.\n+\n+Consider the relative elegance of defining a type family for incrementing a\n+binary number that is read from the right to the left:\n+\n+> type family BInc (binary :: Binary) :: Binary where\n+>     BInc 'BEnd        = 'B1 'BEnd\n+>     BInc ('B0 binary) = 'B1 binary\n+>     BInc ('B1 binary) = 'B0 (BInc binary)\n+\n+[Appendix 3](#appendix-3) contains an (unused) implementation of incrementing\n+left-to-right binary numbers.  Getting things like this to work is not too much\n+of a stretch these days (even though GHCs error messages can be very cryptic).\n+However, due to the large amount of type families involved, proving things about\n+it presumably requires ritually sacrificing an inappropriate amount of Agda\n+programmers while cantating Richard Eisenberg's writings.\n+\n+To that end, it is almost always worth trying to figure out alternate\n+representations that work out more elegantly.  This can lead to some arbitrary\n+looking choices -- we will see this in full effect when trying to define\n+[CutTree](#cuttree) further below.\n+\n+Addition is not too hard to define:\n+\n+> type family BAdd (x :: Binary) (y :: Binary) :: Binary where\n+>     BAdd 'BEnd   y       = y\n+>     BAdd x       'BEnd   = x\n+>     BAdd ('B0 x) ('B0 y) = 'B0 (BAdd x y)\n+>     BAdd ('B1 x) ('B0 y) = 'B1 (BAdd x y)\n+>     BAdd ('B0 x) ('B1 y) = 'B1 (BAdd x y)\n+>     BAdd ('B1 x) ('B1 y) = 'B0 (BInc (BAdd x y))\n+\n+Let's quickly define a number of examples\n+\n+> type BZero  = 'B0 'BEnd\n+> type BOne   = BInc BZero\n+> type BTwo   = BInc BOne\n+> type BThree = BInc BTwo\n+> type BFour  = BInc BThree\n+> type BFive  = BInc BFour\n+\n+This allows us to play around with it in GHCi:\n+\n+~~~~~\n+*Main> :set -XDataKinds\n+*Main> :kind! BAdd BFour BFive\n+BAdd BFour BFive :: Binary\n+= 'B1 ('B0 ('B0 ('B1 'BEnd)))\n+~~~~~\n+\n+Finally, we define a corresponding singleton to use later on:\n+\n+> data SBin (b :: Binary) where\n+>     SBEnd :: SBin 'BEnd\n+>     SB0   :: SBin b -> SBin ('B0 b)\n+>     SB1   :: SBin b -> SBin ('B1 b)\n+\n+Binomial forests\n+----------------\n+\n+Our heap will be a relatively simple wrapper around a recursive type called\n+`Forest`.  This datastructure follows the definition of the binary numbers\n+fairly closely, which makes the code in this section surprisingly easy and we\n+end up requiring no lemmas or proofs whatsoever here.\n+\n+A `Forest o b` refers to a number of trees starting with (possibly) a tree of\n+order `o`.  The `b` is the binary number that indicates the shape of the forest\n+-- i.e., whether we have a tree of a given order or not.\n+\n+Using a handwavy but convenient notation, this means that _Forest 3 101_ refers\n+to binomial trees of order 3 and 5 (and no tree of order 4).\n+\n+> data Forest (o :: Nat) (b :: Binary) a where\n+>     FEnd :: Forest o 'BEnd a\n+>     F0   ::             Forest ('Succ o) b a -> Forest o ('B0 b) a\n+>     F1   :: Tree o a -> Forest ('Succ o) b a -> Forest o ('B1 b) a\n+\n+The empty forest is easily defined:\n+\n+> emptyForest :: Forest o ('B0 'BEnd) a\n+> emptyForest = F0 FEnd\n+\n+`insertTree` inserts a new tree into the forest.  This might require\n+merging two trees together -- roughly corresponding to carrying in binary\n+increment.\n+\n+> insertTree\n+>     :: Ord a\n+>     => Tree o a -> Forest o b a\n+>     -> Forest o (BInc b) a\n+> insertTree s FEnd     = F1 s FEnd\n+> insertTree s (F0 f)   = F1 s f\n+> insertTree s (F1 t f) = F0 (insertTree (mergeTree s t) f)\n+\n+<div id=\"merge\"></div>\n+\n+Similarly, merging two forests together corresponds with adding two binary\n+numbers together:\n+\n+> mergeForests\n+>     :: Ord a\n+>     => Forest o lb a -> Forest o rb a\n+>     -> Forest o (BAdd lb rb) a\n+> mergeForests FEnd      rf   = rf\n+> mergeForests lf        FEnd = lf\n+> mergeForests (F0 lf)   (F0 rf)   = F0 (mergeForests lf rf)\n+> mergeForests (F1 l lf) (F0 rf)   = F1 l (mergeForests lf rf)\n+> mergeForests (F0 lf)   (F1 r rf) = F1 r (mergeForests lf rf)\n+> mergeForests (F1 l lf) (F1 r rf) =\n+>     F0 (insertTree (mergeTree l r) (mergeForests lf rf))\n+\n+It's worth seeing how the different branches in `insertTree` and `mergeForests`\n+match up almost 1:1 with the different clauses in the definition of the type\n+families `BInc` and `BAdd`.  If we overlay them visually:\n+\n+![Overlaying mergeForests and BAdd brings out the\n+similarity](/images/draft-mind-blown.gif)\n+\n+That is the intuitive explanation as to why no additional proofs or type-level\n+trickery is required here.\n+\n+Here is an informal illustration of what happens when we don't need to merge any\n+trees.  The singleton `Forest` on the left is simply put in the empty `F0` spot\n+on the right.\n+\n+![Simple merge; 1 + 100 = 101](/images/draft-03.png)\n+\n+When there is already a tree there, we merge the trees using `mergeTree` and\n+carry that, in a very similar way to how carrying works in the addition of\n+binary numbers:\n+\n+![Merge with carry, 1 + 101 = 110](/images/draft-04.png)\n+\n+The binomial heap\n+-----------------\n+\n+The `Forest` structure is the main workhorse and `Heap` is just a simple wrapper\n+on top of that, where we start out with a tree of order 0:\n+\n+> newtype Heap (b :: Binary) a = Heap {unHeap :: Forest 'Zero b a}\n+\n+The operations on `Heap` are also simple wrappers around the previously defined\n+functions:\n+\n+> emptyHeap :: Heap ('B0 'BEnd) a\n+> emptyHeap = Heap emptyForest\n+\n+> pushHeap :: Ord a => a -> Heap b a -> Heap (BInc b) a\n+> pushHeap x (Heap forest) = Heap (insertTree (singletonTree x) forest)\n+\n+> mergeHeap :: Ord a => Heap lb a -> Heap rb a -> Heap (BAdd lb rb) a\n+> mergeHeap (Heap lf) (Heap rf) = Heap (mergeForests lf rf)\n+\n+We are now ready to show this off in GHCi again:\n+\n+~~~~~\n+*Main> :t pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $\n+            pushHeap 'd' $ pushHeap 'e' emptyHeap\n+Heap ('B1 ('B0 ('B1 'BEnd))) Char\n+~~~~~\n+\n+We can also take a look at the internals of the datastructure using a custom\n+show instance provided in the [appendix 2](#appendix-2):\n+\n+~~~~~~\n+*Main> pushHeap 'a' $ pushHeap 'b' $ pushHeap 'c' $\n+            pushHeap 'd' $ pushHeap 'e' emptyHeap\n+(tree of order 0)\n+ 'a'\n+(no tree of order 1)\n+(tree of order 2)\n+ 'b'\n+  'd'\n+   'e'\n+  'c'\n+~~~~~~\n+\n+Neat!\n+\n+Binomial heaps: let's break it down\n+===================================\n+\n+I think it's interesting that we have implemented an append-only heap without\n+even requiring any lemmas so far.  It is perhaps a good illustration of how\n+append-only datastructures are conceptually much simpler.\n+\n+![Yes, this is a long blogpost.  We've arrived at the halfway point, so it's a\n+good time to get a coffee and take a break.  You deserved it for sticking with\n+me so far.](/images/draft-coffee.jpg)\n+\n+Things get _significantly_ more complicated when we try to implement popping the\n+smallest element from the queue.  For reference, I implemented the heap we have\n+at this point implemented in a couple of hours, where I worked on the rest of\n+the code on and off for about a week.\n+\n+Let's look at a quick illustration of how popping works.\n+\n+We first select the tree with the smallest root and cut it from the heap:\n+\n+![](/images/draft-06.png)\n+\n+We break up this tree we selected into its root (which will be the element that\n+is \"popped\") and its children, which we turn into a new heap:\n+\n+![](/images/draft-07.png)\n+\n+We [merge](#merge) the remainder heap from step 1 together with the new heap we\n+made out of the children of the removed tree:\n+\n+![](/images/draft-08.png)\n+\n+The above merge requires carrying twice.\n+\n+Taking apart a single tree\n+--------------------------\n+\n+We will start by implementing step 2 of the algorithm above since it is a bit\n+easier.  In this step, we are taking all children from a tree and turning that\n+into a new heap.\n+\n+We need to keep all our invariants intact, and in this case this means tracking\n+them in the type system.  A tree of `o` has `2ᵒ` elements.  If we remove the\n+root, we have `o` children trees with `2ᵒ - 1 ` elements in total.  Every child\n+becomes a tree in the new heap.  This means that the heap contains `o` full\n+trees, and its shape will be written as `o` \"1\"s.  This matches our math: if you\n+write `o` \"1\"s, you get the binary notation of `2ᵒ - 1`.\n+\n+Visually:\n+\n+![A tree of order 3 results in a heap with a \"11\" shape](/images/draft-07.png)\n+\n+We introduce a type family for computing `n` \"1\"s:\n+\n+> type family Ones (n :: Nat) :: Binary where\n+>     Ones 'Zero     = 'BEnd\n+>     Ones ('Succ n) = 'B1 (Ones n)\n+\n+We will use a helper function `childrenToForest_go` to maintain some invariants.\n+The wrapper `childrenToForest` is trivially defined but its type tells us a\n+whole deal:\n+\n+> childrenToForest\n+>     :: SNat n\n+>     -> Children n a\n+>     -> Forest 'Zero (Ones n) a\n+> childrenToForest nnat children =\n+>     childrenToForest_go SZero nnat FEnd children\n+\n+The tricky bit is that the list of trees in `Children` has them in descending\n+order, and we want them in ascending order in `Forest`.  This means we will\n+have to reverse the list.\n+\n+We can reverse a list easily using an accumulator in Haskell.  In order to\n+maintain the type invariants at every step, we will increase the size of the\n+accumulator as we descrease the size of the children.  This can be captured\n+by requiring that their sum remains equal (`m ~ NAdd x n`).\n+\n+> childrenToForest_go\n+>     :: m ~ NAdd x n\n+>     => SNat x\n+>     -> SNat n\n+>     -> Forest n (Ones x) a\n+>     -> Children n a\n+>     -> Forest 'Zero (Ones m) a\n+\n+> childrenToForest_go xnat _snat@SZero acc CZero =\n+\n+I will not always go into detail on how the lemmas apply but let's do it here\n+nonetheless.\n+\n+For the base case, we simply want to return our accumulator.  However, our\n+accumulator has the type `Forest n (Ones x)` and we expect something of the type\n+`Forest n (Ones m)`.  Furthermore, we know that:\n+\n+~~~~~~\n+n ~ 'Zero, m ~ NAdd x n\n+⊢ m ~ NAdd x 'Zero\n+~~~~~~\n+\n+We need to prove that `x ~ m` in order to do the cast from `Forest n (Ones x)`\n+to `Forest n (Ones m)`.\n+\n+We can do so by applying `lemma1` to `x` (the latter represented here by\n+`xnat`).  This gives us `lemma1 xnat :: NAdd x 'Zero :~: n`.  Combining this\n+with what we already knew:\n+\n+~~~~~~\n+m ~ NAdd x 'Zero, NAdd x 'Zero ~ n\n+⊢ m ~ x\n+~~~~~~\n+\n+...which is what we needed to know.\n+\n+>     case lemma1 xnat of QED -> acc\n+\n+The inductive case is a bit harder and requires us to prove that:\n+\n+~~~~~~\n+m ~ NAdd x n, m ~ NAdd x n, n ~ 'Succ o\n+⊢ Ones m ~ 'B1 (Ones (NAdd x o))\n+~~~~~~\n+\n+GHC does a great job and ends up with something like:\n+\n+~~~~~~\n+Ones (NAdd x (Succ o)) ~ 'B1 (Ones (NAdd x o))\n+~~~~~~\n+\n+Which only requires us to prove commutativity on `NAdd`.  You can see that\n+proof in `lemma2` a bit further below.  This case also illustrates well how we\n+carry around the singletons as inputs for our lemmas and call on them when\n+required.\n+\n+> childrenToForest_go xnat (SSucc nnat) acc (CCons tree children) =\n+>     case lemma2 xnat nnat of\n+>         QED -> childrenToForest_go\n+>             (SSucc xnat)\n+>             nnat\n+>             (F1 tree acc)\n+>             children\n+\n+Proving `lemma2` is trivial... once you figure out what you need to prove and\n+how all of this works.\n+\n+It took me a good amount time to put the different pieces together in my head.\n+It is not only a matter of proving the lemma: restructuring the code in\n+`childrenToForest_go` leads to different lemmas you can attempt to prove, and\n+figuring which ones are feasible is a big part of writing code like this.\n+\n+> lemma2 :: SNat n -> SNat m -> NAdd n ('Succ m) :~: 'Succ (NAdd n m)\n+> lemma2 SZero     _ = QED\n+> lemma2 (SSucc n) m = case lemma2 n m of QED -> QED\n+\n+More Vec utilities\n+------------------\n+\n+These are some minor auxiliary functions we need to implement on `Vec`.  We\n+mention them here because we'll also need two type classes dealing with\n+non-zeroness.\n+\n+First, we need some sort of `map`, and we can do this by implementing the\n+`Functor` typeclass.\n+\n+> instance Functor (Vec n) where\n+>     fmap _ VNull       = VNull\n+>     fmap f (VCons x v) = VCons (f x) (fmap f v)\n+\n+Secondly we need a very simple function to convert a `Vec` to a list.  Note that\n+this erases the information we have about the size of the list.\n+\n+> vecToList :: Vec n a -> [a]\n+> vecToList VNull       = []\n+> vecToList (VCons x v) = x : vecToList v\n+\n+Using `vecToList`, we can build a function to convert a non-empty `Vec` to a\n+`NonEmpty` list.  This uses an additional `NNonZero` typeclass.\n+\n+> vecToNonEmpty :: NNonZero n ~ 'True => Vec n a -> NonEmpty a\n+> vecToNonEmpty (VCons x v) = x :| vecToList v\n+\n+> type family NNonZero (n :: Nat) :: Bool where\n+>     NNonZero 'Zero     = 'False\n+>     NNonZero ('Succ _) = 'True\n+\n+Non-zeroness can be defined on binary numbers as well:\n+\n+> type family BNonZero (b :: Binary) :: Bool where\n+>     BNonZero 'BEnd   = 'False\n+>     BNonZero ('B1 b) = 'True\n+>     BNonZero ('B0 b) = BNonZero b\n+\n+Popcount and width\n+------------------\n+\n+The minimal element will always be the root of one of our trees.  That means we\n+have as many choices for our minimal element as there are trees in our heap.  We\n+need some way to write down this number as a type.\n+\n+Since we have a tree for every _1_ in our binary number, we can define the\n+number of trees as the [popcount] of the binary number.\n+\n+[popcount]: https://en.wikichip.org/wiki/population_count\n+\n+In a weird twist of fate, you can also pretend this stands for \"the count of\n+trees which we can _pop_\", which is exactly what we will be using it for.\n+\n+> type family Popcount (b :: Binary) :: Nat where\n+>     Popcount 'BEnd   = 'Zero\n+>     Popcount ('B1 b) = 'Succ (Popcount b)\n+>     Popcount ('B0 b) = Popcount b\n+\n+`Popcount` can be used to relate the non-zeroness of a natural number, and the\n+non-zeroness of a binary number.\n+\n+> lemma3\n+>     :: BNonZero b ~ 'True\n+>     => SBin b\n+>     -> NNonZero (Popcount b) :~: 'True\n+> lemma3 (SB1 _) = QED\n+> lemma3 (SB0 b) = case lemma3 b of QED -> QED\n+\n+In addition to caring about the `popcount` of a binary number, we are sometimes\n+interested in its `width` (number of bits).  This is also easily captured in a\n+type family:\n+\n+> type family Width (binary :: Binary) :: Nat where\n+>     Width 'BEnd        = 'Zero\n+>     Width ('B0 binary) = 'Succ (Width binary)\n+>     Width ('B1 binary) = 'Succ (Width binary)\n+\n+That is a fair amount of type families so far.  To make things a bit more clear,\n+here is an informal visual overview of all the type families we have defined,\n+including `BDec` (binary decrement, defined further below).\n+\n+![Rectangles represent (lifted) kinds, arrows are type families](/images/draft-05.png)\n+\n+<div id=\"cuttree\"></div>\n+\n+Lumberjack\n+----------\n+\n+Now, popping the smallest element from the heap first involves cutting a single\n+tree from the forest inside the heap.  Afterwards, we take the root of that tree\n+and merge the children of the tree back together with the original heap.\n+\n+![Selecting a single tree](/images/draft-06.png)\n+\n+However, just selecting (and removing) a single tree turns out to be quite an\n+endeavour on its own.  We define an auxiliary GADT which holds the tree, the\n+remainder of the heap, and most importantly a lot of invariants.\n+\n+Feel free to scroll down to the datatype from here if you are willing to assume\n+the specific constraint and types are there for a reason.\n+\n+The two first fields are simply evidence singletons that we carry about.  `o`\n+stands for the same concept as in `Forest`, it means we are starting with an\n+order of `o`.  `x` stands for the index of the tree that was selected.\n+\n+This means the tree that was selected has an order of `NAdd o x`, as we can see\n+in the third field.  If the remainder of the heap is `Forest o b a`, its shape\n+is denoted by `b` and we can reason about the shape of the original heap.\n+\n+The children of tree (`Tree (NAdd o x) a`) that was selected will convert to\n+heap of shape `Ones x`.  If we add the root to that, we get `BInc (Ones x)`.\n+Merging this together with the remainder of the heap (`Forest o b a`) yields a\n+shape of `BAdd b (BInc (Ones x))`.  Finally, we restructure the type in that\n+result to `BInc (BAdd b (Ones x))`.  The restructuring is trivially allowed by\n+GHC since it just requires applying the necessary type families.\n+\n+We also carry a constraint here that seems very arbitrary and relates the widths\n+of two binary numbers.  It is more easy to understand from an intuitive point of\n+view: the new (merged) heap has the same width as the original heap.\n+Why is it here?\n+\n+Well, it turns out we will need this fact in a further function definition.  If\n+we can conclude it here by construction in the GADT, we avoid having to prove it\n+further down.\n+\n+Of course, I know that I will need this further down because I already have the\n+code compiling.  When writing this, there is often a very, very painful dialogue\n+in between different functions and datatypes, where you try to mediate by making\n+the requested and expected types match by bringing them closer together step by\n+step.  In the end, you get a monstrosity like:\n+\n+> data CutTree (o :: Nat) (b :: Binary) a where\n+>     CutTree\n+>         :: Width (BAdd b (Ones x)) ~ Width (BInc (BAdd b (Ones x)))\n+>         => SNat x\n+>         -> SNat o\n+>         -> Tree (NAdd o x) a\n+>         -> Forest o b a\n+>         -> CutTree o (BInc (BAdd b (Ones x))) a\n+\n+Fortunately, this type is internal only and doesn't need to be exported.\n+\n+`lumberjack_go` is the worker function that takes all possible trees out of a\n+heap.  For every _1_ in the shape of the heap, we have a tree: therefore it\n+should not be a surprise that the length of the resulting vector is\n+`Popcount b`.\n+\n+> lumberjack_go\n+>     :: forall o b a.\n+>        SNat o\n+>     -> Forest o b a\n+>     -> Vec (Popcount b) (CutTree o b a)\n+\n+The definition is recursive and a good example of how recursion corresponds with\n+inductive proofs (we're using `lemma1` and `lemma2` here).  We don't go in too\n+much detail with our explanation here -- this code is often hard to write but\n+surprisingly easy to read.\n+\n+> lumberjack_go _ FEnd = VNull\n+> lumberjack_go nnat0 (F0 forest0) = fmap\n+>     (\\cutTree -> case cutTree of\n+>         CutTree xnat (SSucc nnat) t1 forest1 -> CutTree\n+>             (SSucc xnat)\n+>             nnat\n+>             (case lemma2 nnat xnat of QED -> t1)\n+>             (F0 forest1))\n+>     (lumberjack_go (SSucc nnat0) forest0)\n+> lumberjack_go nnat0 (F1 tree0 forest0) = VCons\n+>     (CutTree\n+>         SZero\n+>         nnat0\n+>         (case lemma1 nnat0 of QED -> tree0)\n+>         (F0 forest0))\n+>     (fmap\n+>         (\\cutTree -> case cutTree of\n+>             CutTree xnat (SSucc nnat) t1 forest1 -> CutTree\n+>                 (SSucc xnat)\n+>                 nnat\n+>                 (case lemma2 nnat xnat of QED -> t1)\n+>                 (F1 tree0 forest1))\n+>         (lumberjack_go (SSucc nnat0) forest0))\n+\n+Lumberjack: final form\n+----------------------\n+\n+Now that we can select `Popcount b` trees, it time to convert this to something\n+more convenient to work it.  We will use a `NonEmpty` to represent our list of\n+candidates to select from.\n+\n+> lumberjack\n+>     :: forall b a. BNonZero b ~ 'True\n+>     => Forest 'Zero b a\n+>     -> NonEmpty.NonEmpty (CutTree 'Zero b a)\n+\n+\n+First we select the `Popcount b` trees:\n+\n+> lumberjack trees =\n+>     let cutTrees :: Vec (Popcount b) (CutTree 'Zero b a)\n+>         cutTrees = lumberjack_go SZero trees in\n+\n+Then we convert it to a `NonEmpty`.  This requires us to call `lemma3` (the\n+proof that relates non-zeroness of a binary number with non-zeroness of a\n+natural number through popcount).  We need an appropriate `SBin` to call\n+`lemma3` and the auxiliary function `treesToSBin` defined just below does that\n+for us.\n+\n+>     case lemma3 (treesToSBin trees :: SBin b) of\n+>          QED -> vecToNonEmpty cutTrees\n+\n+This sneaky function constructs an `SBin b` from a `Forest o b a` value.  It is\n+maybe a bit naughty but this prevents us from carrying around the singletons in\n+a bunch of places.\n+\n+> treesToSBin :: Forest o b a -> SBin b\n+> treesToSBin FEnd     = SBEnd\n+> treesToSBin (F0 t)   = SB0 (treesToSBin t)\n+> treesToSBin (F1 _ t) = SB1 (treesToSBin t)\n+\n+popHeap: gluing the pieces together\n+-----------------------------------\n+\n+We can now find all trees in the heap that may be cut.  They are returned in a\n+`CutTree` datatype.  If we assume that we are taking a specific `CutTree`, we\n+can take the root from the tree inside this datatype, and we can construct a new\n+heap from its children using `childrenToForest`.  Then, we merge it back\n+together with the original heap.\n+\n+The new heap has one less element -- hence we use `BDec` (binary decrement,\n+define just a bit below).\n+\n+> popForest\n+>     :: forall a b. Ord a\n+>     => CutTree 'Zero b a\n+>     -> (a, Forest 'Zero (BDec b) a)","path":"posts/2018-08-16-well-typed-heap.lhs","position":900,"original_position":900,"commit_id":"92ee13d3b49ad9fb473ee5205ea2575b916f93b4","original_commit_id":"92ee13d3b49ad9fb473ee5205ea2575b916f93b4","user":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"body":"You can do it with just `BInc` but you end up with a more awkward signature for `popHeap` involving `Width`, and type inference isn't as good for things like `:t popHeap h` in GHCi, so I'll leave it as is.","created_at":"2018-08-29T09:40:14Z","updated_at":"2018-08-29T09:40:14Z","html_url":"https://github.com/jaspervdj/jaspervdj/pull/16#discussion_r213610596","pull_request_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16","author_association":"OWNER","_links":{"self":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/comments/213610596"},"html":{"href":"https://github.com/jaspervdj/jaspervdj/pull/16#discussion_r213610596"},"pull_request":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16"}},"in_reply_to_id":213548520},"pull_request":{"url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16","id":211560102,"node_id":"MDExOlB1bGxSZXF1ZXN0MjExNTYwMTAy","html_url":"https://github.com/jaspervdj/jaspervdj/pull/16","diff_url":"https://github.com/jaspervdj/jaspervdj/pull/16.diff","patch_url":"https://github.com/jaspervdj/jaspervdj/pull/16.patch","issue_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/16","number":16,"state":"open","locked":false,"title":"Binomial heap blogpost","user":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"body":"","created_at":"2018-08-28T21:13:49Z","updated_at":"2018-08-29T09:40:14Z","closed_at":null,"merged_at":null,"merge_commit_sha":"04787398f3868ed3778b68f63ca5a4c9a467cbf2","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16/commits","review_comments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16/comments","review_comment_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/comments{/number}","comments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/16/comments","statuses_url":"https://api.github.com/repos/jaspervdj/jaspervdj/statuses/92ee13d3b49ad9fb473ee5205ea2575b916f93b4","head":{"label":"jaspervdj:drafts","ref":"drafts","sha":"92ee13d3b49ad9fb473ee5205ea2575b916f93b4","user":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"repo":{"id":458451,"node_id":"MDEwOlJlcG9zaXRvcnk0NTg0NTE=","name":"jaspervdj","full_name":"jaspervdj/jaspervdj","owner":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/jaspervdj/jaspervdj","description":"Source code of my personal home page.","fork":false,"url":"https://api.github.com/repos/jaspervdj/jaspervdj","forks_url":"https://api.github.com/repos/jaspervdj/jaspervdj/forks","keys_url":"https://api.github.com/repos/jaspervdj/jaspervdj/keys{/key_id}","collaborators_url":"https://api.github.com/repos/jaspervdj/jaspervdj/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/jaspervdj/jaspervdj/teams","hooks_url":"https://api.github.com/repos/jaspervdj/jaspervdj/hooks","issue_events_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/events{/number}","events_url":"https://api.github.com/repos/jaspervdj/jaspervdj/events","assignees_url":"https://api.github.com/repos/jaspervdj/jaspervdj/assignees{/user}","branches_url":"https://api.github.com/repos/jaspervdj/jaspervdj/branches{/branch}","tags_url":"https://api.github.com/repos/jaspervdj/jaspervdj/tags","blobs_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/refs{/sha}","trees_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/trees{/sha}","statuses_url":"https://api.github.com/repos/jaspervdj/jaspervdj/statuses/{sha}","languages_url":"https://api.github.com/repos/jaspervdj/jaspervdj/languages","stargazers_url":"https://api.github.com/repos/jaspervdj/jaspervdj/stargazers","contributors_url":"https://api.github.com/repos/jaspervdj/jaspervdj/contributors","subscribers_url":"https://api.github.com/repos/jaspervdj/jaspervdj/subscribers","subscription_url":"https://api.github.com/repos/jaspervdj/jaspervdj/subscription","commits_url":"https://api.github.com/repos/jaspervdj/jaspervdj/commits{/sha}","git_commits_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/commits{/sha}","comments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/comments{/number}","issue_comment_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/comments{/number}","contents_url":"https://api.github.com/repos/jaspervdj/jaspervdj/contents/{+path}","compare_url":"https://api.github.com/repos/jaspervdj/jaspervdj/compare/{base}...{head}","merges_url":"https://api.github.com/repos/jaspervdj/jaspervdj/merges","archive_url":"https://api.github.com/repos/jaspervdj/jaspervdj/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/jaspervdj/jaspervdj/downloads","issues_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues{/number}","pulls_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls{/number}","milestones_url":"https://api.github.com/repos/jaspervdj/jaspervdj/milestones{/number}","notifications_url":"https://api.github.com/repos/jaspervdj/jaspervdj/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/jaspervdj/jaspervdj/labels{/name}","releases_url":"https://api.github.com/repos/jaspervdj/jaspervdj/releases{/id}","deployments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/deployments","created_at":"2010-01-04T19:57:09Z","updated_at":"2018-08-24T10:54:44Z","pushed_at":"2018-08-28T21:13:50Z","git_url":"git://github.com/jaspervdj/jaspervdj.git","ssh_url":"git@github.com:jaspervdj/jaspervdj.git","clone_url":"https://github.com/jaspervdj/jaspervdj.git","svn_url":"https://github.com/jaspervdj/jaspervdj","homepage":"jaspervdj.be","size":46624,"stargazers_count":85,"watchers_count":85,"language":"Haskell","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":35,"mirror_url":null,"archived":false,"open_issues_count":3,"license":null,"forks":35,"open_issues":3,"watchers":85,"default_branch":"master"}},"base":{"label":"jaspervdj:master","ref":"master","sha":"b3908e70612d7b4e144322baa5302d9c2c68b50d","user":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"repo":{"id":458451,"node_id":"MDEwOlJlcG9zaXRvcnk0NTg0NTE=","name":"jaspervdj","full_name":"jaspervdj/jaspervdj","owner":{"login":"jaspervdj","id":95501,"node_id":"MDQ6VXNlcjk1NTAx","avatar_url":"https://avatars2.githubusercontent.com/u/95501?v=4","gravatar_id":"","url":"https://api.github.com/users/jaspervdj","html_url":"https://github.com/jaspervdj","followers_url":"https://api.github.com/users/jaspervdj/followers","following_url":"https://api.github.com/users/jaspervdj/following{/other_user}","gists_url":"https://api.github.com/users/jaspervdj/gists{/gist_id}","starred_url":"https://api.github.com/users/jaspervdj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaspervdj/subscriptions","organizations_url":"https://api.github.com/users/jaspervdj/orgs","repos_url":"https://api.github.com/users/jaspervdj/repos","events_url":"https://api.github.com/users/jaspervdj/events{/privacy}","received_events_url":"https://api.github.com/users/jaspervdj/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/jaspervdj/jaspervdj","description":"Source code of my personal home page.","fork":false,"url":"https://api.github.com/repos/jaspervdj/jaspervdj","forks_url":"https://api.github.com/repos/jaspervdj/jaspervdj/forks","keys_url":"https://api.github.com/repos/jaspervdj/jaspervdj/keys{/key_id}","collaborators_url":"https://api.github.com/repos/jaspervdj/jaspervdj/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/jaspervdj/jaspervdj/teams","hooks_url":"https://api.github.com/repos/jaspervdj/jaspervdj/hooks","issue_events_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/events{/number}","events_url":"https://api.github.com/repos/jaspervdj/jaspervdj/events","assignees_url":"https://api.github.com/repos/jaspervdj/jaspervdj/assignees{/user}","branches_url":"https://api.github.com/repos/jaspervdj/jaspervdj/branches{/branch}","tags_url":"https://api.github.com/repos/jaspervdj/jaspervdj/tags","blobs_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/refs{/sha}","trees_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/trees{/sha}","statuses_url":"https://api.github.com/repos/jaspervdj/jaspervdj/statuses/{sha}","languages_url":"https://api.github.com/repos/jaspervdj/jaspervdj/languages","stargazers_url":"https://api.github.com/repos/jaspervdj/jaspervdj/stargazers","contributors_url":"https://api.github.com/repos/jaspervdj/jaspervdj/contributors","subscribers_url":"https://api.github.com/repos/jaspervdj/jaspervdj/subscribers","subscription_url":"https://api.github.com/repos/jaspervdj/jaspervdj/subscription","commits_url":"https://api.github.com/repos/jaspervdj/jaspervdj/commits{/sha}","git_commits_url":"https://api.github.com/repos/jaspervdj/jaspervdj/git/commits{/sha}","comments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/comments{/number}","issue_comment_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/comments{/number}","contents_url":"https://api.github.com/repos/jaspervdj/jaspervdj/contents/{+path}","compare_url":"https://api.github.com/repos/jaspervdj/jaspervdj/compare/{base}...{head}","merges_url":"https://api.github.com/repos/jaspervdj/jaspervdj/merges","archive_url":"https://api.github.com/repos/jaspervdj/jaspervdj/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/jaspervdj/jaspervdj/downloads","issues_url":"https://api.github.com/repos/jaspervdj/jaspervdj/issues{/number}","pulls_url":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls{/number}","milestones_url":"https://api.github.com/repos/jaspervdj/jaspervdj/milestones{/number}","notifications_url":"https://api.github.com/repos/jaspervdj/jaspervdj/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/jaspervdj/jaspervdj/labels{/name}","releases_url":"https://api.github.com/repos/jaspervdj/jaspervdj/releases{/id}","deployments_url":"https://api.github.com/repos/jaspervdj/jaspervdj/deployments","created_at":"2010-01-04T19:57:09Z","updated_at":"2018-08-24T10:54:44Z","pushed_at":"2018-08-28T21:13:50Z","git_url":"git://github.com/jaspervdj/jaspervdj.git","ssh_url":"git@github.com:jaspervdj/jaspervdj.git","clone_url":"https://github.com/jaspervdj/jaspervdj.git","svn_url":"https://github.com/jaspervdj/jaspervdj","homepage":"jaspervdj.be","size":46624,"stargazers_count":85,"watchers_count":85,"language":"Haskell","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":35,"mirror_url":null,"archived":false,"open_issues_count":3,"license":null,"forks":35,"open_issues":3,"watchers":85,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16"},"html":{"href":"https://github.com/jaspervdj/jaspervdj/pull/16"},"issue":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/16"},"comments":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/issues/16/comments"},"review_comments":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16/comments"},"review_comment":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/pulls/16/commits"},"statuses":{"href":"https://api.github.com/repos/jaspervdj/jaspervdj/statuses/92ee13d3b49ad9fb473ee5205ea2575b916f93b4"}},"author_association":"OWNER"}}
{"actor":{"display_login":"jaspervdj"}}