Fundamentals of Haskell Type Classes and "could not deduce (~) from the context (~)" error

Question

I'm relatively new to Haskell, and I believe I'm misunderstanding something fundamental about type classes. Suppose I'd like to create a type class 'T' implementing n-ary trees supported by four algebraic types 'A, B, C, and D' whose structure imposes a maximum depth of four. This seems like a silly example but I think it best illustrates my point.

module Test where

class T t0 where
    parent :: T t1 => t0 -> Maybe t1
    children :: T t1 => t0 -> [t1]

data A = A [B]
instance T A where
    parent (A _) = Nothing
    children (A bs) = bs

data B = B A [C]
instance T B where
    parent (B a _) = Just a
    children (B _ cs) = cs

data C = C B [D]
instance T C where
    parent (C b _) = Just b
    children (C _ ds) = ds

data D = D C
instance T D where
    parent (D c) = Just c
    children (D _) = []

I'd like to write generic parent and children functions, but GHC isn't having any of it.

Test.hs:10:27:
    Could not deduce (t1 ~ B)
    from the context (T t1)
      bound by the type signature for children :: T t1 => A -> [t1]
      at Test.hs:10:9-28
      `t1' is a rigid type variable bound by
           the type signature for children :: T t1 => A -> [t1]
           at Test.hs:10:9
    Expected type: [t1]
      Actual type: [B]
    In the expression: bs
    In an equation for `children': children (A bs) = bs
    In the instance declaration for `T A'

Test.hs:14:31:
    Could not deduce (t1 ~ A)
    from the context (T t1)
      bound by the type signature for parent :: T t1 => B -> Maybe t1
      at Test.hs:14:9-31
      `t1' is a rigid type variable bound by
           the type signature for parent :: T t1 => B -> Maybe t1
           at Test.hs:14:9
    In the first argument of `Just', namely `a'
    In the expression: Just a
    In an equation for `parent': parent (B a _) = Just a

Test.hs:15:29:
    Could not deduce (t1 ~ C)
    from the context (T t1)
      bound by the type signature for children :: T t1 => B -> [t1]
      at Test.hs:15:9-30
      `t1' is a rigid type variable bound by
           the type signature for children :: T t1 => B -> [t1]
           at Test.hs:15:9
    Expected type: [t1]
      Actual type: [C]
    In the expression: cs
    In an equation for `children': children (B _ cs) = cs
    In the instance declaration for `T B'

Test.hs:19:31:
    Could not deduce (t1 ~ B)
    from the context (T t1)
      bound by the type signature for parent :: T t1 => C -> Maybe t1
      at Test.hs:19:9-31
      `t1' is a rigid type variable bound by
           the type signature for parent :: T t1 => C -> Maybe t1
           at Test.hs:19:9
    In the first argument of `Just', namely `b'
    In the expression: Just b
    In an equation for `parent': parent (C b _) = Just bv

I (think I) understand that type classes aren't at all like Java interfaces, in that the class-level functions must work for any possible value of the provided type variables; the caller isn't "deciding" the type. I don't understand why GHC can't deduce (t1 ~ _), because the type substituted for t1 is always an instance of 'T'. I see that there's a sort of circular dependency among the instance declarations, e.g. A's instance declaration depends on B's being valid, which depends on A's and C's, and so on, but I feel as though GHC is smart enough to figure that out and I'm simply missing something. I always seem to get this error whenever I'd like a function in a type class to accept one type in the class but return another... Is there a way to accomplish this with type classes?

I see that there are many similarly-worded questions here, but I have yet to find one that matches my problem(as far as I can tell).

Thanks in advance.

Answer 1

You've correctly understood the problem: these signatures really mean

parent :: forall t1 . T t1 => t0 -> Maybe t1

rather that what you'd have in a covariant OO language,

parent :: exists t1 . T t1 => t0 -> Maybe t1

The two usual solutions for such kind of stuff are to use the similar syntactic extensions

• TypeFamilies

  class T t0 where
    type Child t0 :: *
    parent :: Child t0 -> Maybe t0
    children :: t0 -> [Child t 0]
  
  instance T A where
    type Child A = B
    parent (A _) = Nothing
  
  ...
  

• or MultiparamTypeClasses

  class T child t0 where
    parent :: child -> Maybe t0
    children :: t0 -> [child]
  
  instance T A B where
  ...
  

Note that in both cases, D won't have an instance.

As to which of these extensions is "better" – you can't really answer that. MultiparamTypeClasses by itself is often too "weak" in that you need to fix all the involved types manually, but that can be lifted through adding a FunctionalDependency. In a special case of class T child t0 | t0 -> child, that's then largely equivalent to the TypeFamilies solution. But in your case, class T child t0 | t0 -> child, child -> t0 would also be possible.

Consider the Haskell Wiki for details.

Answer 2

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!