<span style="font-family:courier new,monospace">I've recently been playing with Sebastian Fischer's explicit sharing monad</span><br style="font-family:courier new,monospace"><div class="gmail_quote"><span style="font-family:courier new,monospace">library (found at <a href="http://sebfisch.github.com/explicit-sharing" target="_blank">http://sebfisch.github.com/explicit-sharing</a>) and after</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">looking at the code noticed the implementation memoizes values into an IntMap</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">of untyped values that are coerced into the correct type on retrieval, which</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">is a sensible and practical way to implement this.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Just for fun I thought I'd have a go at implementing a (very impractical)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">version without type casting but, disappointingly, I didn't quite get there.</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">I ran out of steam by the time I got around to playing with parameterized</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">monads by which stage the type signatures started looking a bit scary.</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">That and I needed to get back to my projects.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">This has been sitting on my hard drive for a couple of weeks now and I've</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">finally decided to clean it up and post it, maybe someone else will find it</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">amusing.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">The post is about HList inspired type level implementation of Okasaki's</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">skew binary random access lists indexed by Roman numerals, using ideas from</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Ralf Hinze's paper "Functional Pearl: Typed Quote/Antiquote - Or: Compile-time</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Parsing" and some fun tricks from the MLton wiki:</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><a href="http://www.cs.ox.ac.uk/ralf.hinze/publications/Quote.pdf" target="_blank">http://www.cs.ox.ac.uk/ralf.hinze/publications/Quote.pdf</a></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"><a href="http://mlton.org/Fold" target="_blank">http://mlton.org/Fold</a></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><a href="http://mlton.org/Fold01N" target="_blank">http://mlton.org/Fold01N</a></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"><a href="http://mlton.org/VariableArityPolymorphism" target="_blank">http://mlton.org/VariableArityPolymorphism</a></span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">With that out of the way, we start of by declaring all the different</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">extensions we'll need.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE FlexibleInstances #-}</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE FunctionalDependencies #-}</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> {-# LANGUAGE MultiParamTypeClasses #-}</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE ScopedTypeVariables #-}</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> {-# LANGUAGE TypeFamilies #-}</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE TypeSynonymInstances #-}</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">These two are ugly. We need undecidable instances for bunch of things and</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">overlapping instances for the type equality trick borrowed from the HList</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">paper:</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><a href="http://homepages.cwi.nl/%7Eralf/HList/paper.pdf" target="_blank">http://homepages.cwi.nl/~ralf/HList/paper.pdf</a></span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE OverlappingInstances #-}</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> {-# LANGUAGE UndecidableInstances #-}</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">For GHC 7 we also need to increase the context stack.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> {-# OPTIONS_GHC -fcontext-stack=100 #-}</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Define Boolean values at the type level.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data T = T</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data F = F</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And now Peano numbers. We don't actually use the constructors for</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">anything but if we omitted them we'd have to use another extension,</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">EmptyDataDecls.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data Z = Z</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data S n = S n</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Here we create some types for heterogeneous lists and trees. Note that Pair</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">has an extra type parameter. We provide two different versions of the cons</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">operation. One requires that extra parameter but does not require undecidable</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">instances. Unfortunately we still need undecidable instances later</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">on for indexing.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data Pair i x y = Pair x y deriving Show</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data Nil = Nil deriving Show</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> data Tree l x r = Node l x r deriving Show</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> data Leaf x = Leaf x deriving Show</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type Pair' x y = Pair () x y</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> nil :: Nil</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> nil = Nil</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Equality, less than, addition, subtraction and multiplication by 2 type</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">functions for Peano numbers.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type family Equals m n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Equals Z Z = T</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Equals Z (S n) = F</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Equals (S n) Z = F</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Equals (S m) (S n) = Equals m n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type family LessThan m n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance LessThan Z Z = F</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance LessThan Z (S n) = T</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance LessThan (S n) Z = F</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance LessThan (S m) (S n) = LessThan m n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type family Add m n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Add Z n = n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Add n Z = n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Add (S m) (S n) = S (S (Add m n))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type family Sub m n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Sub n Z = n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Sub (S m) (S n) = Sub m n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type family Mul2 n</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Mul2 Z = Z</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Mul2 (S n) = S (S (Mul2 n))</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And finally tree depth and weight/size.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type family Depth t</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Depth (Leaf x ) = S Z</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Depth (Tree l x r) = S (Depth l)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type family Weight t</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Weight (Leaf x ) = S Z</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Weight (Tree l x r) = S (Mul2 (Weight l))</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">For reference, here is normal implementation of random access lists</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> newtype List a = List { unList :: [(Int, Tree a)] } deriving Show</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> data Tree a = Leaf a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | Node (Tree a) a (Tree a) deriving Show</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> cons :: a -> List a -> List a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> cons x (List wts) = List $ case wts of</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> (v, l) : (w, r) : wts' | v == w -> (1 + w + w, Node l x r) : wts'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> _ -> (1 , Leaf x ) : wts</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">List here is a list of pairs of balanced binary trees and their weights.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">The cons function has exactly two cases. The second case is trivial, we are</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">mostly interested in the first case. If the weights of the two trees at the</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">front of the list are the same, we combine them into a new tree with the newly</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">inserted element at the top.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now we are ready to implement cons. This first version is simpler but requires</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">undecidable instances.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> class Cons' x y z | x y -> z where cons' :: x -> y -> z</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Here we cover the cases of inserting an element into an empty list, and</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">inserting an element into a list with a single element. These cover two out of</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">four different possibilities when inserting a new element.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Cons' x Nil (Pair' (Leaf x) Nil) where cons' = Pair . Leaf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Cons' x (Pair' y Nil) (Pair' (Leaf x) (Pair' y Nil)) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cons' = Pair . Leaf</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">The remaining two cases occur when we have at least two elements in the list.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">This is where we need to compare weights of trees. First observation is that</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">we don't need weight of a tree, depth is sufficient.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now we have a problem. We'd like to be able to write something like</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> instance (Depth l ~ u, Depth r ~ v, Equals u v ~ T) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> Cons' x (Pair' l (Pair' r y)) (Pair' (Tree l x r) y) where ...</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> instance (Depth l ~ u, Depth r ~ v, Equals u v ~ F) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> Cons' x y (Pair' (Leaf x) y) where ...</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">but we get a functional dependency conflict in the second instance as the type</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">variable y might stand for Pair' l (Pair' r y) and the functional dependency</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">already says the result should be Pair' (Tree l x r) y, not</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Pair' (Leaf x) (Pair' l (Pair' r y))</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We need to merge these two instances into one and then branch on the result of</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">the comparison of tree depths.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">To do this, we introduce another type class to do the branching.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> class ConsIf c x y z | c x y -> z where consIf :: c -> x -> y -> z</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And merge the instances.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( Depth l ~ u</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Depth r ~ v</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Equals u v ~ c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , ConsIf c x (Pair' l (Pair' r y)) z ) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> Cons' x (Pair' l (Pair' r y)) z where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> cons' = consIf (undefined :: c)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ConsIf F x y (Pair' (Leaf x) y) where consIf _ = Pair . Leaf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance (Depth l ~ u, Depth r ~ u) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ConsIf T x (Pair' l (Pair' r y)) (Pair' (Tree l x r) y) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> consIf _ x (Pair l (Pair r y)) = Pair (Node l x r) y</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We can now test our cons function.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t0' = cons' 'a'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons' (33 :: Int)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons' (4.4 :: Float)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons' (88 :: Integer)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons' ([1 .. 8] :: [Int])</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons' "moose"</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons' ((6, 3) :: (Int, Int))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ nil</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And ghci tells us the type is</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">*Main> :t t0'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">t0'</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> :: Pair'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (Tree</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> (Tree (Leaf Float) Int (Leaf Integer))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> Char</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> (Tree (Leaf [Char]) [Int] (Leaf (Int, Int))))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> Nil</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now we get to the second version that doesn't need the undecidable instances</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">extension. In this one we go a step back and attempt to keep track of depth</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">information in the type of the list. When we again end up at the point where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">we need to compare if two trees at the front of the list are of the same</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">depth, we run into a problem.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> instance Cons x (Pair i l (Pair i r y))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (Pair (S i) (Tree l x r) y) where ...</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> instance Cons x (Pair i y (Pair j z w))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (Pair (S Z) x (Pair i y (Pair j z w))) where ...</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">This clearly won't work as we again get a functional dependency conflict. The j</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">type variable could be the same as i in which case we have two different rules</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">for what the result of consing x with (Pair i l (Pair i r y)) should be.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">As we don't want to use undecidable instances, we are stuck. Unless we can</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">find a way to disambiguate the two instances.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Instead of keeping track of depth information, we could try to track how many</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">elements we need to complete a new tree. That way instead of counting up, we</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">are counting down towards zero and it becomes easy to differentiate the two</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">instances as only the one where the depths of the two trees are equal will</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">contain a Z.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Keeping track of how many elements are missing turns out to be a problem,</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">at least as long as we don't want to use undecidable instances. Fortunately</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">we can replace the number of elements missing with the number of levels the</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">tree at the front needs before its depth matches the tree that follows.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> class Cons x y z | x y -> z where cons :: x -> y -> z</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Inserting an element into an empty list involves adding the element to the</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">front and setting its the depth counter to 1.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Cons x Nil (Pair (S Z) (Leaf x) Nil) where cons = Pair . Leaf</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">If we are inserting an element into a list that already has a single tree,</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">we again add the new element to the front, set its counter to 1 and we</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">decrement the counter of the tree that now follows the newly inserted element.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Cons x (Pair (S i) y Nil) (Pair (S Z) (Leaf x) (Pair i y Nil)) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cons x (Pair y z) = Pair (Leaf x) (Pair y z)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Here we have the case where the list already contains at least two trees but</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">their depths are not equal. Like with the previous instance we insert the new</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">element to the front and decrement the counter of the tree that now follows it.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Cons x (Pair (S i) y (Pair (S j) z w))</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> (Pair (S Z) (Leaf x) (Pair i y (Pair (S j) z w))) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> cons x (Pair y z) = Pair (Leaf x) (Pair y z)</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">That means we are left with one more case to handle. The case when the depths</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">of the two trees are the same, or rather when the counter reaches 0.</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">As we merge the two trees and create a new tree, we must also decrement the</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">counter of the tree that follows. What this means is that we really need two</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">instances. One where there are only two trees of the same depth in the list,</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">and one where those two trees are followed by at least one more tree.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance (Depth l ~ i, Depth r ~ i) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> Cons x (Pair i l (Pair Z r Nil)) (Pair (S i) (Tree l x r) Nil) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> cons x (Pair l (Pair r y)) = Pair (Node l x r) y</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">As we merge the trees into a new tree, we reset and increment the depth</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">counter. Note that we are using the first tree's counter. Reason for that is</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">that the counter must represent the tree's depth as the tree at the front was</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">either just inserted and so its counter is 1, or it was created when two</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">smaller trees merged and its counter was set to its depth.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Finally we must also decrement the counter of the tree that follows.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance (Depth l ~ i, Depth r ~ i) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> Cons x (Pair i l (Pair Z r (Pair (S j) y z)))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> (Pair (S i) (Tree l x r) (Pair j y z)) where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cons x (Pair l (Pair r (Pair y z))) = Pair (Node l x r) (Pair y z)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Now we can test the new cons function.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> t0 = cons 'a'</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons (33 :: Int)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons (4.4 :: Float)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons (88 :: Integer)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons ([1 .. 8] :: [Int])</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ cons "moose"</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> $ cons ((6, 3) :: (Int, Int))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> $ nil</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">The type is slightly more verbose.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">*Main> :t t0</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">t0</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> :: Pair</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (S (S (S Z)))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> (Tree</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (Tree (Leaf Float) Int (Leaf Integer))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> Char</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (Tree (Leaf [Char]) [Int] (Leaf (Int, Int))))</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> Nil</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Here we introduce our wrapper for Roman numerals though we won't get to</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">play with those just yet.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> newtype R n = R { unR :: Int } deriving Show</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We want to get indexing and updates out of the way first. The reference</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">implementation for the indexing function is a bit more complex than the cons</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">function. Each of the cases we need to handle has been marked with a comment</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">so we can see which instance matches which part of the code.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> index :: List a -> Int -> Maybe a</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> index (List ((w, t) : wts)) i</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | i < w = index' w i t -- 1</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> | otherwise = index (List wts) (i - w) -- 2</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> index' 1 0 (Leaf x ) = Just x -- 3</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> index' _ _ (Leaf _ ) = Nothing</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> index' w i (Node l x r)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | i == 0 = Just x -- 4</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> | i <= w' = index' w' (i - 1 ) l -- 5</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | otherwise = index' w' (i - 1 - w') r -- 6</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> w' = w `div` 2</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> index _ _ = Nothing</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">We don't need to do anything when the index is out of range - the type system</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">takes care of that for us.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> class Index i x y | i y -> x where index :: y -> R i -> x</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> class IndexIf c i x y | c i y -> x where indexIf :: c -> y -> R i -> x</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">First we handle the easy cases.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Index Z x (Leaf x ) where index (Leaf x ) _ = x -- 3</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance Index Z x (Tree l x r) where index (Node _ x _) _ = x -- 4</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Cases 5 and 6 require the use of a second type class so we can branch on the</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">result of the comparison i <= w, though we rewrite it to w < i' + 1 to make</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">use of the LessThan type family and to differentiate instance 6 from</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">instance 4.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Instead of halving the weight of the tree we are currently working on, we</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">get the weight of one of its children.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( Weight l ~ w</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , LessThan w (S i) ~ c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , IndexIf c i x (Tree l y r) ) => Index (S i) x (Tree l y r) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> index t _ = indexIf (undefined :: c) t (undefined :: R i) -- 5, 6</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Index i x l => IndexIf F i x (Tree l y r) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> indexIf _ (Node l _ _) = index l -- 5</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( Weight r ~ w</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Sub i w ~ j</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Index j x r ) => IndexIf T i x (Tree l y r) where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> indexIf _ (Node _ _ r) _ = index r (undefined :: R j) -- 6</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Cases 1 and 2 are handled in a similar way.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( Weight t ~ w</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , LessThan i w ~ c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , IndexIf c i x (Pair j t y) ) => Index i x (Pair j t y) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> index = indexIf (undefined :: c) -- 1, 2</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Index i x t => IndexIf T i x (Pair j t y) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> indexIf _ (Pair t _) = index t -- 1</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( Weight t ~ w</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Sub i w ~ j</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Index j x y ) => IndexIf F i x (Pair k t y) where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> indexIf _ (Pair _ y) _ = index y (undefined :: R j) -- 2</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Update is similar.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> update :: Int -> a -> List a -> List a</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> update i x (List ((w, t) : wts)) = List $</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> if i < w then (w, update' w i t) : wts -- 1</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> else (w, t) : unList (update (i - w) x (List wts)) -- 2</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> update' 1 0 (Leaf _ ) = Leaf x -- 3</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> update' _ _ (Leaf _ ) = error "update"</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> update' w i (Node l x' r)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | i == 0 = Node l x r -- 4</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> | i <= w' = Node l' x' r -- 5</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> | otherwise = Node l x' r' -- 6</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> w' = w `div` 2</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> l' = update' w' (i - 1 ) l</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> r' = update' w' (i - 1 - w') r</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> update _ _ _ = error "update"</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> class Index i x z => Update i x y z | i x y -> z where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> update :: y -> R i -> x -> z</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> class UpdateIf c i x y z | c i x y -> z where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> updateIf :: c -> y -> R i -> x -> z</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance Update Z x (Leaf y) (Leaf x) where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> update _ _ x = Leaf x -- 3</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Update Z x (Tree l y r) (Tree l x r) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> update (Node l _ r) _ x = Node l x r -- 4</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( Weight l ~ w</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , LessThan w (S i) ~ c</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Index (S i) x t</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , UpdateIf c i x (Tree l y r) t) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> Update (S i) x (Tree l y r) t where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> update t _ = updateIf (undefined :: c) t (undefined :: R i) -- 5, 6</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance Update i x l l' => UpdateIf F i x (Tree l y r) (Tree l' y r) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> updateIf _ (Node l y r) i x = Node (update l i x) y r -- 5</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( Weight r ~ w</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Sub i w ~ j</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Update j x r r' ) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> UpdateIf T i x (Tree l y r) (Tree l y r') where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> updateIf _ (Node l y r) _ x = -- 6</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> Node l y (update r (undefined :: R j) x)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( Weight t ~ w</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , LessThan i w ~ c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Index i x p</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , UpdateIf c i x (Pair j t y) p ) => Update i x (Pair j t y) p where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> update = updateIf (undefined :: c) -- 1, 2</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance Update i x t t' => UpdateIf T i x (Pair j t y) (Pair j t' y) where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> updateIf _ (Pair t y) i x = Pair (update t i x) y -- 1</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( Weight t ~ w</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , Sub i w ~ j</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , Update j x y z ) => UpdateIf F i x (Pair k t y) (Pair k t z) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> updateIf _ (Pair t y) _ x = -- 2</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> Pair t (update y (undefined :: R j) x)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Maybe we could combine Update and Index type classes into a single class? But</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">we won't attempt that here.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now that we have indexing and updates, we need values we can use to index the</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">list. Typing Z, S Z, S (S Z) and so on is too tedious and not very readable.</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We could use templates to predefine a whole bunch of type level numbers.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">That's kind of ugly though. And we can do it without using any extensions, in</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">plain Haskell 98.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We start off by making I a type synonym for S. Then we define types II to X,</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">XX to C in steps of 10, CC to M in steps of 100 and finally we define MM and</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">MMM. I don't know how Roman numerals are supposed to work above 3999 so that's</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">the largest number we will be able to encode. Probably for the best as the</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">type system doesn't seem too happy about having to deal with types of this</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">sort.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type I n = S n</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type II n = I (I n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type III n = I (II n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type IV n = I (III n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type V n = I (IV n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type VI n = I (V n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type VII n = I (VI n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type VIII n = I (VII n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type IX n = I (VIII n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type X n = I (IX n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type XX n = X (X n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type XXX n = X (XX n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type XL n = X (XXX n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type L n = X (XL n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type LX n = X (L n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type LXX n = X (LX n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type LXXX n = X (LXX n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type XC n = X (LXXX n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type C n = X (XC n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type CC n = C (C n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type CCC n = C (CC n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type CD n = C (CCC n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type D n = C (CD n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type DC n = C (D n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type DCC n = C (DC n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type DCCC n = C (DCC n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type CM n = C (DCCC n)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type M n = C (CM n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type MM n = M (M n)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type MMM n = M (MM n)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now for the fun part. We'd like to be able to construct only valid Roman</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">numerals and that the type signatures match the values. We start of by</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">defining the return and lift functions as described in Ralf Hinze's paper.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">We don't go all the way to creating a monad as these two functions are the</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">only thing we need.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ret a f = f a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> lift f = ret . f</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now before we continue, we need a way to ensure that only valid numbers are</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">constructed. We can group numbers in the range I to X into one group, let's</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">call it ones, X to C into group tens, C to M into group hundreds and M, MM and</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">MMM are in group thousands. A valid number can have at most 1 digit from each</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">group. Digits also have to be ordered from largest to smallest, left to right.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">To do that, we could try and reuse the LessThen type family from before and add</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">constraints so that a digit from the tens group can only be appended to a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">number less than ten. And a digit from the hundreds group can only be applied</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">to a number less than a hundred. This approach works but it makes the GHC's</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">type system choke and evaluating types of expressions takes minutes.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We could also create a class for each of the groups and a set of combinators</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">that can only be applied to a group of a lower rank. This works better.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">But we can go a step further than that - we don't actually need any type</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">classes. All we need is one more phantom type for the rank of the number.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">So we introduce a second type that resembles R, only has one extra type</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">variable.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> newtype R' n s = R' { unR' :: Int } deriving Show</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Here we make use of ret and lift to create polyvariadic functions for</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">constructing Roman numerals. rn starts the construction and nr finalizes it.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> rn :: ((R' n s -> R n) -> r) -> r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> rn f = ret (R . unR') f</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> nr :: (R' Z (IV Z) -> r) -> r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> nr f = f (R' 0)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Trying them in ghci we get</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">*Main> rn nr</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">R {unR = 0}</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">*Main> :t rn nr</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">rn nr :: R Z</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We have a zero. Notice in the type signature for nr, rank of zero is 4.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Now we need to generate the digits. We can use a single function to generate</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">all of them.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> mkR n = lift (\f -> f . R' . (+ n) . unR')</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And we encode the constraints in the type. Digits from the ones group can only</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">be applied to a number of rank 4. There is only one number of rank 4 and that</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">is zero.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">Applying a digit from the ones group to a zero gives us a number of rank 3.</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Digits from the tens group can be applied to numbers of ranks 3 or 4 and</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">return a number of rank 2. And so on.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type RF n m s t k r = (R' n s -> k) -> ((R' m t -> k) -> r) -> r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> i :: RF (I n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> ii :: RF (II n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> iii :: RF (III n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> iv :: RF (IV n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> v :: RF (V n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> vi :: RF (VI n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> vii :: RF (VII n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> viii :: RF (VIII n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ix :: RF (IX n) n (III Z) (IV s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> x :: RF (X n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> xx :: RF (XX n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> xxx :: RF (XXX n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> xl :: RF (XL n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> l :: RF (L n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> lx :: RF (LX n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> lxx :: RF (LXX n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> lxxx :: RF (LXXX n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> xc :: RF (XC n) n (II Z) (III s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> c :: RF (C n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cc :: RF (CC n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ccc :: RF (CCC n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cd :: RF (CD n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> d :: RF (D n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> dc :: RF (DC n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> dcc :: RF (DCC n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> dccc :: RF (DCCC n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> cm :: RF (CM n) n (I Z) (II s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> m :: RF (M n) n Z (I s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> mm :: RF (MM n) n Z (I s) k r</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> mmm :: RF (MMM n) n Z (I s) k r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> i = mkR 1</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> ii = mkR 2</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> iii = mkR 3</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> iv = mkR 4</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> v = mkR 5</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> vi = mkR 6</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> vii = mkR 7</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> viii = mkR 8</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ix = mkR 9</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> x = mkR 10</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> xx = mkR 20</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> xxx = mkR 30</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> xl = mkR 40</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> l = mkR 50</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> lx = mkR 60</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> lxx = mkR 70</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> lxxx = mkR 80</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> xc = mkR 90</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> c = mkR 100</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cc = mkR 200</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> ccc = mkR 300</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> cd = mkR 400</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> d = mkR 500</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> dc = mkR 600</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> dcc = mkR 700</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> dccc = mkR 800</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> cm = mkR 900</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> m = mkR 1000</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> mm = mkR 2000</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> mmm = mkR 3000</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">We can now try to construct a number such as 2011.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> r2011 = rn mm x i nr</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">*Main> r2011</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">R {unR = 2011}</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">*Main> :t r2011</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">r2011 :: R (MM (X (I Z)))</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">The type reflects the value we entered.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">Attempting to construct an invalid number gives us an error</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">*Main> rn v vi nr</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><interactive>:1:0:</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> Couldn't match expected type `Z' against inferred type `S s'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> Probable cause: `rn' is applied to too many arguments</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> In the expression: rn v vi nr</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> In the definition of `it': it = rn v vi nr</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">I'll finish off this post with a generic map function. Here we use the type</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">equality trick from the HList paper.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> class GMap t p q | t p -> q where gmap :: t -> p -> q</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> class GMapIf c t p q | c t p -> q where gmapIf :: c -> t -> p -> q</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance GMap (a -> b) Nil Nil where gmap _ = id</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( TypeEq a x c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , GMapIf c (a -> b) (Leaf x) (Leaf y) ) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> </span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> GMap (a -> b) (Leaf x) (Leaf y) where gmap = gmapIf (undefined :: c)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( TypeEq a x c</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , GMapIf c (a -> b) (Tree l x r) (Tree l' y r') ) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> GMap (a -> b) (Tree l x r) (Tree l' y r') where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> gmap = gmapIf (undefined :: c)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( GMap (a -> b) x y</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , GMap (a -> b) p q ) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> GMap (a -> b) (Pair i x p) (Pair i y q) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> gmap f (Pair x p) = Pair (gmap f x) (gmap f p)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance GMapIf F (a -> b) (Leaf x) (Leaf x) where gmapIf _ _ = id</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance GMapIf T (a -> b) (Leaf a) (Leaf b) where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> gmapIf _ f (Leaf a) = Leaf (f a)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance ( GMap (a -> b) l l'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> , GMap (a -> b) r r' ) =></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> GMapIf F (a -> b) (Tree l x r) (Tree l' x r') where</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> gmapIf _ f (Node l x r) = Node (gmap f l) x (gmap f r)</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance ( GMap (a -> b) l l'</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> , GMap (a -> b) r r' ) =></span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> GMapIf T (a -> b) (Tree l a r) (Tree l' b r') where</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> gmapIf _ f (Node l a r) = Node (gmap f l) (f a) (gmap f r)</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type family Cast a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type family Cast' t a</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type family Cast'' t a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Cast a = Cast' () a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> type instance Cast' t a = Cast'' t a</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> type instance Cast'' () a = a</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> class TypeEq x y c | x y -> c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance Cast c ~ F => TypeEq x y c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance TypeEq Char Char T</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance TypeEq Int Int T</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> instance TypeEq Float Float T</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> instance TypeEq a a T => TypeEq [a] [a] T</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">And a few tests to see if it all works.</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t1 = gmap (length :: String -> Int) t0</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> t2 = gmap (length :: [Int] -> Int) t1</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t3 = gmap ((+ 1000) :: Int -> Int) t2</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t4 = cons (t0 `index` rn iv nr) t3</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t5 = update t4 (rn iv nr) "asdf"</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t1' = gmap (length :: String -> Int) t0'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">> t2' = gmap (length :: [Int] -> Int) t1'</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t3' = gmap ((+ 1000) :: Int -> Int) t2'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t4' = cons' (t0' `index` rn iv nr) t3'</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">></span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">> t5' = update t4' (rn iv nr) "asdf"</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">As a bonus the implementation of type-level Roman numerals in Standard ML.</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">SML/NJ has a fit trying to load the code. It seems to cope with it if</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">constructors for values above 100 are commented out. And it gives really nice</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">type signatures. MLton has no problems compiling the code, but fully expands</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">all type signatures.</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">(*****************************************************************************)</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">signature ROMAN = sig</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type z</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n i</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ii = 'n i i</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n iii = 'n i ii</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n iv = 'n i iii</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n v = 'n i iv</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n vi = 'n i v</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n vii = 'n i vi</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n viii = 'n i vii</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ix = 'n i viii</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n x = 'n i ix</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n xx = 'n x x</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n xxx = 'n x xx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n xl = 'n x xxx</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n l = 'n x xl</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n lx = 'n x l</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n lxx = 'n x lx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n lxxx = 'n x lxx</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n xc = 'n x lxxx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n c = 'n x xc</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n cc = 'n c c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ccc = 'n c cc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n cd = 'n c ccc</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n d = 'n c cd</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n dc = 'n c d</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n dcc = 'n c dc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n dccc = 'n c dcc</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n cm = 'n c dccc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n m = 'n c cm</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n mm = 'n m m</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n mmm = 'n m mm</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type ('n, 's) r'</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val toInt : 'n r -> int</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val <| : ((('n, 's) r' -> 'n r) -> 'r) -> 'r</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val |> : ((z, z iv) r' -> 'r) -> 'r</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type ('n, 'm, 's, 't, 'k, 'r) rf =</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> (('n, 's) r' -> 'k) -> ((('m, 't) r' -> 'k) -> 'r) -> 'r</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val i : ('n i , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val ii : ('n ii , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val iii : ('n iii , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val iv : ('n iv , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val v : ('n v , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val vi : ('n vi , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val vii : ('n vii , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val viii : ('n viii, 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val ix : ('n ix , 'n, z iii, 's iv , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val x : ('n x , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val xx : ('n xx , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val xxx : ('n xxx , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val xl : ('n xl , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val l : ('n l , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val lx : ('n lx , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val lxx : ('n lxx , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val lxxx : ('n lxxx, 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val xc : ('n xc , 'n, z ii , 's iii, 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val c : ('n c , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val cc : ('n cc , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val ccc : ('n ccc , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val cd : ('n cd , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val d : ('n d , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val dc : ('n dc , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val dcc : ('n dcc , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val dccc : ('n dccc, 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val cm : ('n cm , 'n, z i , 's ii , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val m : ('n m , 'n, z , 's i , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> val mm : ('n mm , 'n, z , 's i , 'k, 'r) rf</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> val mmm : ('n mmm , 'n, z , 's i , 'k, 'r) rf</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">end</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">structure Roman :> ROMAN = struct</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> datatype z = Z</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> datatype 'n i = I of 'n</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ii = 'n i i</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n iii = 'n i ii</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n iv = 'n i iii</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n v = 'n i iv</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n vi = 'n i v</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n vii = 'n i vi</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n viii = 'n i vii</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ix = 'n i viii</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n x = 'n i ix</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n xx = 'n x x</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n xxx = 'n x xx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n xl = 'n x xxx</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n l = 'n x xl</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n lx = 'n x l</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n lxx = 'n x lx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n lxxx = 'n x lxx</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n xc = 'n x lxxx</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n c = 'n x xc</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n cc = 'n c c</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n ccc = 'n c cc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n cd = 'n c ccc</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n d = 'n c cd</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n dc = 'n c d</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n dcc = 'n c dc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n dccc = 'n c dcc</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n cm = 'n c dccc</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n m = 'n c cm</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n mm = 'n m m</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type 'n mmm = 'n m mm</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> type 'n r = int</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> datatype ('n, 's) r' = R of int</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> type ('n, 'm, 's, 't, 'k, 'r) rf =</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> (('n, 's) r' -> 'k) -> ((('m, 't) r' -> 'k) -> 'r) -> 'r</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun toInt n = n</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> local</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun unR (R n) = n</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun ret a f = f a</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun lift f = ret o f</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun mkR n k = lift (fn g => g o R o (fn x => x + n) o unR) k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> in</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun <| f = ret unR f</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun |> f = f (R 0)</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun i k = mkR 1 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun ii k = mkR 2 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun iii k = mkR 3 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun iv k = mkR 4 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun v k = mkR 5 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun vi k = mkR 6 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun vii k = mkR 7 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun viii k = mkR 8 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun ix k = mkR 9 k</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun x k = mkR 10 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun xx k = mkR 20 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun xxx k = mkR 30 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun xl k = mkR 40 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun l k = mkR 50 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun lx k = mkR 60 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun lxx k = mkR 70 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun lxxx k = mkR 80 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun xc k = mkR 90 k</span><br style="font-family:courier new,monospace"><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun c k = mkR 100 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun cc k = mkR 200 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun ccc k = mkR 300 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun cd k = mkR 400 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun d k = mkR 500 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun dc k = mkR 600 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun dcc k = mkR 700 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun dccc k = mkR 800 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun cm k = mkR 900 k</span><br style="font-family:courier new,monospace">
<br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun m k = mkR 1000 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> fun mm k = mkR 2000 k</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace"> fun mmm k = mkR 3000 k</span><br style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"> end</span><br style="font-family:courier new,monospace">
<span style="font-family:courier new,monospace">end</span><br style="font-family:courier new,monospace">
</div><br>