Type Lists with constraints

Question

I'm trying to build a list at the type level, but I'm having some trouble figuring out how to enforce constraints.

My base code is:

data Foo z q = Foo1 (z q)
             | Foo2 (z q)

class Qux q -- where ...
class Baz z -- where ...

class Bar a where             -- a has kind *->*
  type BCtx a q :: Constraint -- using ConstraintKinds to allow constraints on the concrete type
  f :: (BCtx a q) => a q -> a q -> a q
  g :: (BCtx a q, BCtx a q') => a q -> a q'

instance (Baz z) => Bar (Foo z) where
  type BCtx (Foo z) q = (Num (z q), Qux q) -- for example
  f (Foo1 x) (Foo1 y) = Foo1 $ x+y -- these functions need access to the type q to do arithmetic mod q
  f (Foo1 x) (Foo2 y) = Foo2 $ x-y
  -- ...

You can think of the qs above representing prime powers. I would also like to represent composite numbers using a type list of qis. I'm imagining something like:

data QList qi qs = QCons qi qs
                 | QNil

with the data

data FList c q = FNil 
               | FCons (c (Head q)) (FList c (Tail q))

where (Head q) should correspond to qi and (Tail q) should correspond to qs. Note that the q parameter for FList is NOT (necessarily) a (Qux q), it is a list of (Qux qi). (I don't want to flesh out anything more about this list, since it's one of the design problems I'm posing). I would like to work "modulus-wise" on the FList:

instance (Bar c) => Bar (FList c) where
   type BCtx (FList c) q = () -- Anything I put here is not enough
   f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
   -- the left call to `f` calls a concrete instance, the right call to `f` is a recursive call on the rest of the list
   -- ...

Compiling these codes snippets together in GHC result in (modulo transcription, abstraction, and typing errors):

Could not deduce (BCtx c (Head q), BCtx c (Tail q))

and then

Could not deduce (BCtx c (Head (Tail q)), BCtx c (Tail (Tail q)))

etc.

I see why I'm getting this error, but not how to fix it.

Concretely, I'm expecting an FList c q type where c~Foo z and q~QCons q1 (QCons q2 QNil), and of course my list will satisfy all of the BCtx constraints at every level.

I'm not sure that fixing those particular errors will result in compiling code, but it is a start. The entire Bar class is basically fixed (the Constraint kind is required, and the instances of Bar must have kind * -> *). I don't believe I can use existential types to create a list of generic objects because I need access to the qi parameter. I am willing to change the type of FList and QList to allow me to work modulus-wise on a collection of Bars.

Thanks for your time!

Answer 1

To handle type lists, it's necessary to discriminate empty from nonempty lists and handle them separately. The 'Could not deduce' errors in your code occur because your instance assumes a nonempty list, when in fact the list may or may not be empty. Here is a solution using the extensions TypeFamilies, TypeOperators, DataKinds, and GADTs.

With DataKinds, type lists are predefined. They have kind [*], but they'll be used in a context where kind * is expected, so an operator is needed to cast them:

data InjList (qs :: [*])

Using type lists, FList is defined as

data FList c q where
  FNil :: FList c (InjList '[])
  FCons :: c h -> FList c (InjList t) -> FList c (InjList (h ': t))

It's defined as a GADT to express how it's only possible to construct FLists over the type InjList q' for some type-list q'. For instance, the term FCons [True] FNil has type FList [] (InjList (Bool ': '[])). On the other hand, since Bool isn't of the form InjList q', there are no terms (except ⊥) of type FList [] Bool. By pattern matching on an FList, a function can verify that it has been given a non-⊥ argument, and further determine whether it's been passed an empty type list.

An instance of Bar for FLists has to handle nil lists and cons lists separately. A nil list has an empty context. A cons list has components for the head and tail of the list. This is expressed by pattern matching on the type-list in the associated type instance of BCtx. The function f examines its argument to verify that it's not ⊥ and to decide whether it's an empty list.

instance (Bar c) => Bar (FList c) where
  -- Empty context for '[]
  type BCtx (FList c) (InjList '[]) = ()
  -- Context includes components for head and tail of list
  type BCtx (FList c) (InjList (h ': t)) = (BCtx c h, BCtx (FList c) (InjList t))

  f FNil FNil = FNil
  f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)

We can load the code into GHCi to verify that it works:

instance Bar [] where
  type BCtx [] q = Num q
  f xs ys = zipWith (+) xs ys

instance Show (FList c (InjList '[])) where
  show FNil = "FNil"

instance (Show (c h), Show (FList c (InjList t))) => Show (FList c (InjList (h ': t))) where
  show (FCons h t) = "FCons (" ++ show h ++ ") (" ++ show t ++ ")"

$ ghci

> :load Test
> f (FCons [1,2] FNil) (FCons [3,4] FNil)
FCons ([4,6]) (FNil)