This really isn't an answer to your specific question but it is an solution to your problem: create an k-ary tree structure whose max depth is constrained by its type. If you aren't concerned with using a lot of GHC extensions this solution is pretty simple and extensible.
I won't go into too much detail - the rules for how exactly certain extensions work are pretty complex and if you want the gritty details you should read the docs.
{-# LANGUAGE
MultiParamTypeClasses
, DataKinds
, GADTs
, FunctionalDependencies
, KindSignatures
, FlexibleInstances
, UndecidableInstances
, PolyKinds
, TypeOperators
, FlexibleContexts
, TypeFamilies
#-}
-- Not all of these are needed; most are used to make the code cleaner
data Nat = Z | P Nat
The Nat
type is used to encode the depth on the type level. Using -XDataKinds
, GHC can take a simple datatype like Nat
and 'lift' it; that is, data constructors becomes types, and the type Nat
becomes a 'kind' (the type of a type). Z
== zero; P
== plus one.
type family LTEQ (a :: Nat) (b :: Nat) :: Bool
type instance LTEQ Z Z = True
type instance LTEQ Z (P x) = True
type instance LTEQ (P x) Z = False
type instance LTEQ (P a) (P b) = LTEQ a b
Next we define a partial order on Nat
. Notice the explicit kind signatures (ie - a :: Nat
) - these aren't needed with PolyKinds
but make it clearer what is going on. If this looks confusing, just think of it as a set of rules:
0 <= 0 == True
0 <= (1 + x) == True
(1 + x) <= 0 == False
(1 + x) <= (1 + y) == x <= y
If you want to prove to yourself that this works:
-- This would only be used for testing
data Pr p = Pr
lteq :: f ~ (a `LTEQ` b) => Pr a -> Pr b -> Pr f
lteq _ _ = Pr
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr Z)
lteq (Pr :: Pr (P Z)) (Pr :: Pr Z) :: Pr Bool 'False
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr (P Z))
lteq (Pr :: Pr (P Z)) (Pr :: Pr (P Z)) :: Pr Bool 'True
>:t lteq (Pr :: Pr (P Z)) (Pr :: Pr (P (P Z)))
lteq (Pr :: Pr (P Z)) (Pr :: Pr (P (P Z))) :: Pr Bool 'True
>:t lteq (Pr :: Pr Z) (Pr :: Pr (P (P Z)))
lteq (Pr :: Pr Z) (Pr :: Pr (P (P Z))) :: Pr Bool 'True
>:t lteq (Pr :: Pr Z) (Pr :: Pr Z)
lteq (Pr :: Pr Z) (Pr :: Pr Z) :: Pr Bool 'True
We have to use Pr
as opposed to just a -> b -> (LTEQ a b)
because a
and b
are lifted types (specifically of kind Nat
) and (->)
only takes unlifted types. If this makes no sense, don't worry too much as it doesn't really matter. Suffice it to say that it is needed here.
Defining what the max depth is, is very very simple:
type MAXDEPTH = P (P (P (P Z)))
Note how simple it is to change your max depth. Now the Tree
data type. It uses GADT (generalized algebraic datatype) syntax; basically all this means is we get way more control over exactly how you can create some thing of type Tree
. The d
type variable is the depth, a
is the element stored in the tree.
data Tree d a where
D0 :: a -> Tree Z a
DPlus :: ((P d) `LTEQ` MAXDEPTH) ~ True => a -> [Tree d a] -> Tree (P d) a
Lets break it down by constructors. The first one, D0
takes a value of type a
and creates a tree of depth zero that stores just that value: just a single node with no child nodes.
DPlus
takes a node and a list of subtrees. Adding one node obviously increases the depth by one - you can see that the result type reflects this. Then, in order to enforce the maximum depth of 4, we just say that d + 1 <= MAXDEPTH
.
Because 0 depth trees are pretty boring, you will probably want a helper function for depth 1:
depth1 a xs = DPlus a (map D0 xs)
Then a show instance just for fun:
instance Show a => Show (Tree d a) where
show (D0 a) = "D0 " ++ show a
show (DPlus a xs) = "DPlus " ++ show a ++ " " ++ show xs
And a quick test:
>depth1 'c' "hello"
DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']
>DPlus 'a' [depth1 'c' "hello"]
DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]
>DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]
DPlus 'b' [DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]]
>DPlus 'c' [DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]]
DPlus 'c' [DPlus 'b' [DPlus 'a' [DPlus 'c' [D0 'h',D0 'e',D0 'l',D0 'l',D0 'o']]]]
>DPlus 'd' [DPlus 'c' [DPlus 'b' [DPlus 'a' [depth1 'c' "hello"]]]]
<interactive>:130:1:
Couldn't match type 'False with 'True
Expected type: 'True ...
As you can see, attempting to build a tree whose depth is more than 4 will cause a type error.
A quick note: your example code is for trees which allow you to reference back 'up' their structure. Since the main purpose of my answer was to demonstrate the use of DataKinds
to enforce tree depth on the type level, I just implemented a very simple tree. You have the right idea for referencing 'up' the tree, but since now everything is a single type, you probably won't even need typeclasses!