Dependently typed red-black tree in Haskell, part 2

Red-black constraint

The basic red-black constraint can easily be captured by a pair of mutually recursive ADTs

type RedBlack a = Either (Red a) (Black a)

data Red a = Red a (Black a) (Black a)

data Black a = Leaf |
               Black a (RedBlack a) (RedBlack a)

However, we also wanted this to be a left leaning red-black tree, meaning all 3-nodes lean left. This can also be build into the ADTs

data Red a = Red a (Black a) (Black a)

data Black a = Leaf |
               Black2 a (Black a) (Black a) |
               Black3 a (Red a) (Black a) |
               Black4 a (Red a) (Red a)

Black depth constraint

Black depth is the fun part, where we parameterize the ADT by a natural number to track the depth. First we'll need to switch to GADTs, so we need to enable the GHC extension. Additionally, we need StandaloneDeriving to get things like Show for GADTs.

{-# LANGUAGE GADTs, StandaloneDeriving #-}

data Red a where
  Red :: a -> (Black a) -> (Black a) -> Red a

data Black a where
  Leaf :: Black a
  Black2 :: a -> (Black a) -> (Black a) -> Black a
  Black3 :: a -> (Red a) -> (Black a) -> Black a
  Black4 :: a -> (Red a) -> (Red a) -> Black a

deriving instance Show a => Show (Black a)
deriving instance Show a => Show (Red a)

Now to parameterize by black depth, n

{-# LANGUAGE DataKinds, GADTs, StandaloneDeriving #-}

module Page2 (Black(Leaf)) where

import Data.Type.Natural

data Red a n where
  Red :: a -> (Black a n) -> (Black a n) -> Red a n

data Black a n where
  Leaf :: Black a Z
  Black2 :: a -> (Black a n) -> (Black a n) -> Black a (S n)
  Black3 :: a -> (Red a n) -> (Black a n) -> Black a (S n)
  Black4 :: a -> (Red a n) -> (Red a n) -> Black a (S n)

deriving instance Show a => Show (Black a n)
deriving instance Show a => Show (Red a n)

A couple interesting points here. Note how we explicitly declare that leaves have a black depth of zero (Z). Red nodes have the same black depth as their children. Black nodes are one level deeper than their children (children, the second and third arguments of the constructors, have a depth of n, while current node has a depth of (S n), ie, n+1).

One more detail, the depth parameter is a pain because it changes on inserts and deletes. Even worse, it only changes on some inserts and deletes (and is, in general, path dependent). Luckily, we can hide the depth behind another GADT.

data Root a where
  Root :: Black a n -> Root a

And that's about it. Given these definitions, it is impossible to construct a tree that violates any of these constraints. That just leaves the binary search tree constraint, ie, proving that all the tree operations maintain sort order. However, this is tricky, especially given GHC's limited support for dependent types.

Last step is to implement insert and delete.

Dependently typed red-black tree in Haskell, part 1

Introduction

Dependent types, and the idea of baking both algorithmic and business constraints into the type system are very exciting to me. However, beyond a few toy examples of Peano arithmetic and vectors, I haven't found a lot of examples online. So in the spirit of scratching my own itch, I am going to working through implementing a left-leaning red-black tree, capturing as many of the constraints as possible in the type system.

A warning at the outset, I am relatively new to Haskell and very new to dependent types, so I welcome any feedback on both my Haskell, if it is not idiomatic,  my use of dependent types and my choice of library dependencies. This series will be based entirely on GHC, and I will make liberal use of GHC extensions.

Find my Github repository at:
https://github.com/farrellm/dependent-rbtree

Dependencies

Note that GHC does have type-level natural numbers built in¹. However, in my experimentation, these seem not to be useful for more complex use cases. Rather I will be using the following libraries:

• singletons - Seems to be the de factor standard for dependent types in GHC, I depend on it transitively
• type-natural - A powerful library for type level natural numbers implemented in with the singletons library

Also, I will be using stack, rather than cabal, to manage the project. At the moment, stack seems to be a saner tool for managing Hackage dependencies.

Overview

Red-black trees have several defining properties²:

1. Binary search tree
2. Alternating red-black properties
3. Consistent black-height

Left-leaning red-black trees add:

4. Require that all 3-nodes lean left.

Property 1 is beyond the scope of this blog; at some future time I may attempt to port this to Idris, at which time I will attempt 1.

Property 2 can be easily captured using ADTs.

Property 3 is my primary target with dependent types.

Property 4 I haven't thought about enough yet :-)

---

1 https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html^↩

2 https://en.wikipedia.org/wiki/Red%E2%80%93black_tree^↩

Clojure on Windows

Mostly this is stolen from http://onbeyondlambda.blogspot.com/2012/01/setting-up-clojure-emacs-on-windows.html with some updates where appropriate.

1. Install Java 7 JDK
2. Use environment variables:
   JAVA_HOME = C:\Program Files\Java\jdk1.7.0_03Path = %Path%;%Java_Home%\bin;c:\lein
   JAVA_CMD = %java_home%/bin/java.exe
3.  Make directory c:\lein
4. Extract to c:\lein
   http://www.paehl.com/open_source/?download=curl_729_0_ssl.ziphttps://raw.github.com/technomancy/leiningen/stable/bin/lein.bat
5. Open a command prompt (win-r, "cmd")
6. Run "lein self-install". Test install was successful by running "lein repl"
7. Download Emacs. Extract it anywhere you like, and run "bin/runemacs"
   http://mirror.clarkson.edu/gnu/gnu/emacs/windows/emacs-24.3-bin-i386.zip
8. Open ~/.emacs (<Ctrl>-X <Ctrl>-F ~/.emacs <Enter>) and add the following to enable an extra package repository, then restart:
   ;;; ELPA
   (require 'package)
   (add-to-list 'package-archives
       '("marmalade" . "http://marmalade-repo.org/packages/"))
9. Install package "nrepl" (<Alt>-x package-install <Enter> nrepl <Enter>). This will also install "clojure-mode" as it is a dependency of nrepl.

Now, on to scad-clj!

1. Download and install Openscad
   https://openscad.googlecode.com/files/OpenSCAD-2013.01-Installer.exe
2. Download the project from github and extract anywhere you like
   https://github.com/farrellm/scad-clj/archive/master.zip
3. Open a sample design, eg, "scad-clj-master/src/scad_clj/designs/cage.clj"
4. Start a REPL (<Alt>-x nrepl-jack-in)

Tail recursion in Python

Admittedly, not the most "pythonic" code, whatever that means...

#!/usr/bin/python

from inspect import isfunction

recur = 0

def loop(func):
  def inner(a,b):
    global recur
    old_recur = recur
    recur = lambda a,b: lambda:func(a,b)
    ret = func(a,b)
    while isfunction(ret):
      ret = ret()
    recur = old_recur
    return ret
  return inner

Which creates a nice decorator:

@loop
def foo(n, a):
  if n == 0:
    return a
  else:
    return recur(n-1,a*n)

print(foo(6,1))

Tail recursion in Perl

I finally get to use local! This really should be wrapped up in some type of module, but it is getting late.

#!/usr/bin/perl -w

$recur = 0;

sub loop($) {
    my ($func) = @_;

    sub {
        local $recur = sub {
            my @args = @_;
            sub { $func->(@args); }
        };

        my $ret = $func->(@_);
        while ('CODE' eq ref($ret)) {
           $ret = $ret->(); 
        }
        $ret;
    };
}

Example usage:

my $foo = loop sub {
    my ($n, $a) = @_;
    if ($n == 0) {
        $a;
    }
    else {
        $recur->($n-1, $a*$n);
    }
};

print $foo->(999999,1) . "\n";

Tail recursion in Groovy

Groovy ships with a limited form of tail recursion via a trampoline mechanism. Here, I expand on the existing trampoline to add a cleaner, more intuitive interface. This extension has two parts: a Java class and a new Object method (read: global function).

A Java class:

import groovy.lang.Closure;
// loop/recur

class RecursionWrapper {
    private Closure<object> _target;

    public RecursionWrapper(Closure<object> target) {
     _target = target;
    }
    
    public Object recur() {
        return _target.trampoline();
    }
    public Object recur(Object a) {
        return _target.trampoline(a);
    }
    public Object recur(Object... a) {
        return _target.trampoline(a);
    }
}

A global function:

// loop/recur

Object.metaClass.loop = {closure->
 def cln = closure.clone()
 def trCln = cln.trampoline()
 def rw = new RecursionWrapper(trCln)
 cln.delegate = rw
 trCln
}

Tail recursion

To restart my blogging, I will be writing a short series of posts on adding Clojure style loop/recur tail recursion to other languages. Code will generally come first and I will fill in details as I have time.