How can I make heterogeneous lists (aka HLists) with constrained elements?

Question

I've been experimenting with using type families to abstract UI toolkits. I've come unstuck as I try to make use of HLists (http://homepages.cwi.nl/~ralf/HList/) to improve the API.

My API initially looked something like this:

{-# LANGUAGE TypeFamilies #-}

class UITK tk where
  data UI tk :: * -> *

  stringEntry :: (UITK tk) => UI tk String
  intEntry :: (UITK tk) => UI tk Int

  tuple2UI :: (UI tk a,UI tk b) -> (UI tk (a,b))
  tuple3UI :: (UI tk a,UI tk b,UI tk c) -> (UI tk (a,b,c))
  tuple4UI :: (UI tk a,UI tk b,UI tk c,UI tk d) -> (UI tk (a,b,c,d))

ui :: (UITK tk) => (UI tk (String,Int)) 
ui = tuple2UI (stringEntry,intEntry)

This works, but the UI combiner works on tuples, and so I need a different function for each tuple size. I thought I could make use of something like HLists, but either it's not possible, (or hopefully) I just lack the necessary type-fu.

Here's my attempt:

{-# LANGUAGE TypeFamilies,FlexibleInstances,MultiParamTypeClasses #-}

-- A heterogeneous list type 

data HNil = HNil deriving (Eq,Show,Read)
data HCons e l = HCons e l deriving (Eq,Show,Read) 

-- A list of UI fields, of arbitrary type, but constrained on their
-- tk parameter. The StructV associated type captures the return
-- type of the combined UI

class (UITK tk) => FieldList tk l
  where type StructV tk l

instance (UITK tk) => FieldList tk HNil
  where type StructV tk HNil = HNil

instance (UITK tk, FieldList tk l) => FieldList tk (HCons (UI tk a) l)
  where type StructV tk (HCons (UI tk a) l) = (HCons a (StructV tk l))

fcons :: (UITK tk, FieldList tk l) => UI tk a -> l  -> HCons (UI tk a) l
fcons = HCons

-- Now the abstract ui toolkit definition

class UITK tk where
    data UI tk :: * -> *

    stringEntry :: (UITK tk) => UI tk String
    intEntry :: (UITK tk) => UI tk Int

    structUI :: (FieldList tk l) => l -> (UI tk (StructV tk l))

-- this doesn't work :-(

ui :: (UITK tk) => (UI tk (HCons String (HCons Int HNil)))
ui = structUI (fcons stringEntry
              (fcons intEntry
              HNil ))

The definition at the end gives me several errors, the first of which is:

Z.hs:38:6:
    Could not deduce (FieldList
                        tk (HCons (UI tk0 String) (HCons (UI tk1 Int) HNil)))
      arising from a use of `structUI'
    from the context (UITK tk)
      bound by the type signature for
                 ui :: UITK tk => UI tk (HCons String (HCons Int HNil))
      at Z.hs:(38,1)-(40,21)
    Possible fix:
      add (FieldList
             tk
             (HCons
                (UI tk0 String) (HCons (UI tk1 Int) HNil))) to the context of
        the type signature for
          ui :: UITK tk => UI tk (HCons String (HCons Int HNil))
      or add an instance declaration for
         (FieldList tk (HCons (UI tk0 String) (HCons (UI tk1 Int) HNil)))
    In the expression:
      structUI (fcons stringEntry (fcons intEntry HNil))
    In an equation for `ui':
        ui = structUI (fcons stringEntry (fcons intEntry HNil))

Without completely understanding this, I think I can see at least one of the problems. I'm not successfully informing the compiler that the 3 tk type parameters are all the same type (ie it refers to tk, tk0, tk1) above. I don't understand this - my fcons constructor is intended to keep the UI tk parameters consistent for the constructed HList.

This is my first experience with type families and multi-parameter types classes, so it's likely I'm missing something fundamental.

Is is possible to construct heterogeneous lists with constrained elements? Where am I going wrong?

Answer 1

The type error is from this chain of logic: the 'ui' has 'structui' outermost and 'structUI :: (FieldList tk l) =>' needs the '(FieldList tk l)' where 'tk' and 'l' must match the type signature you wrote for 'ui'.

Everything is, individually, polymorphic in the type variable 'tk'.

The type checker gives a different tk0 to the argument to structui/fcons and just because you have an instance with matching tk's does not mean that I will not come along and make a FieldList instance with distinct tk's. Thus the type checker is stuck.

Here is how I can fix this for the type checker:

-- Use this instance instead of the one you wrote
instance (UITK tk, FieldList tk l, tk ~ tk') => FieldList tk (HCons (UI tk' a) l)
  where type StructV tk (HCons (UI tk' a) l) = (HCons a (StructV tk l))

-- Now this works :)
ui :: (UITK tk) => (UI tk (HCons String (HCons Int HNil)))
ui = structUI (fcons stringEntry
              (fcons intEntry
              HNil ))

The replacement instance matches all possible combinations of tk and tk', then requires they be the same. No one can come along and write another such instance without overlapping.

Responding to timbod's comment: Consider this code, note that (toEnum 97)::Char is 'a'

class TwoParam a b where
  combine :: a -> b -> (a,b)
  combine = (,)

instance TwoParam c c

t1 :: (TwoParam Char b) => Char -> b -> (Char,b)
t1 = combine

main = print (t1 'a' (toEnum 97))

This fails with the message:

No instance for (TwoParam Char b0) arising from a use of `t1'
Possible fix: add an instance declaration for (TwoParam Char b0)
In the first argument of `print', namely `(t1 'a' (toEnum 98))'
In the expression: print (t1 'a' (toEnum 98))
In an equation for `main': main = print (t1 'a' (toEnum 98))
Failed, modules loaded: none.

Why? The type checker infers that (toEnum 98) has some Enum type, and this might be Char, but it will not make the inference that it must be Char. The type checker will not match (toEnum 97) to Char even though the only available instance of (TwoParam Char b) would require matching b with Char. The compiler is correct here because I could later write another instance:

--  instance TwoParam Char Integer

With this second (overlapping) instance it is no longer obvious which instance ought to be chosen. The solution is to use the above 'trick':

-- instance (c ~ d) => TwoParam c d

The type checker only looks at the 'TwoParam c d' when choosing an instance, and this matches everything. Then it tries to satisfy the constraint

Char ~ typeOf (fromEnum 98)

which will succeed. With the trick 'main' prints ('a','a')