Recursive types is haskell, which do not repeat the same constructor

user_13998590 0
Viewed 191

I want to make a tree in Haskell with different node tags. The general case looks like this:

data Tree a
    = Leaf a
    | Node1 [Tree a]
    | Node2 [Tree a]
    ...
    | NodeN [Tree a]

Now I want to tell the compiler that every specific node does not repeat. I made that using GADTs and sum types

data Tree t a where
  Leaf  :: a -> Tree t a
  Node1 :: [Either (Tree 2 a) (Tree 3 a)] -> Tree 1 a
  Node2 :: [Either (Tree 1 a) (Tree 3 a)] -> Tree 2 a
  Node3 :: [Either (Tree 1 a) (Tree 2 a)] -> Tree 3 a

But I don't like my solution for several reasons.

  • An instance is not well defined because you can put a Leaf into a Left or Right.
  • Adding another node would change the type of all the other constructors.
  • Using this tree from outside causes pain because the type of a specific tree depends on its root.

Is there a better solution? Can I say something like "I want every type Tree t a but not Tree 1 a"?

Update 1 According to the answer from chi I made this

data Tag = L | A | B | C

data Tree (a :: Tag) v where
    Leaf :: l -> Tree L v
    N1 :: NotEqual a A => [Tree a v] -> Tree A v
    N2 :: NotEqual a B => [Tree a v] -> Tree B v
    N3 :: NotEqual a C => [Tree a v] -> Tree C v

type family NotEqual (a :: Tag) (b :: Tag) :: Constraint where
  NotEqual x x = TypeError (Text "forbidden Case")
  NotEqual _ _ = ()

I works well but I cant create N1 [N2 [Leaf 1], N3 [Leaf 3] ] with that.

gadt tree recursion haskell types
1 Answers

You might want to use a custom constraint here, and exploit DataKinds.

Below, I only show an untested sketch.

We start by defining a type for tags.

data Tag = T1 | T2 | ...

Then we annotate the tree with the list of forbidden tags, i.e. those tags than can not be used in the tree. This list is then checked each time we use a constructor.

data Tree (forbidden :: [Tag]) a where
  Leaf  :: a -> Tree forbidden a
  Node1 :: NotIn 'T1 forbidden => [Tree ('T1 ': forbidden) a] -> Tree forbidden a
  Node2 :: NotIn 'T2 forbidden => [Tree ('T2 ': forbidden) a] -> Tree forbidden a
  ...

Now we need to define the constraint. We can proceed by induction on the "forbidden tags list".

type family NotIn (x :: Tag) (xs :: [Tag]) :: Constraint where
   NotIn _ '[]       = ()
   NotIn x '(x :  _) = TypeError "forbidden case"
   NotIn x '(_ : xs) = NotIn x xs

The main disadvantage of this approach is that we can not write a O(1) weakening, as in

weakening :: Tree '(t : f) a -> Tree f a

For that we need to traverse the whole tree, using O(N) time.

user_32349590
Related