Type heterogeneous lists and default (?) With type families?

Question

I am working on a library where I want to define a recursive class that I have simplified here to:

{-# LANGUAGE MultiParamTypeClasses , FlexibleInstances #-} data Snoc st bc = Snoc (st b) (c -> b) data Top a = Top class StackTo a st c where runStack :: st c -> (c -> a) instance StackTo a Top a where runStack _ = id instance (StackTo a st b) => StackTo a (Snoc st b) c where runStack (Snoc st' cb) = runStack st' . cb 

This allows me, for example,

 *Main Data.Label> let f = runStack $ Snoc (Snoc Top fst) head :: [(a,x)] -> a *Main Data.Label> f [('a',undefined)] 'a' 

But this seems to require careful use of type annotations, otherwise ...

 *Main Data.Label> let f = runStack $ Snoc (Snoc Top fst) head <interactive>:1:1: No instance for (StackTo a0 Top b0) arising from a use of `runStack' Possible fix: add an instance declaration for (StackTo a0 Top b0) In the expression: runStack In the expression: runStack $ Snoc (Snoc Top fst) head In an equation for `it': it = runStack $ Snoc (Snoc Top fst) head 

I think that these are the same problems that were discussed in this issue , but it is difficult for me to adapt this solution here. Can I use type families or some other method to come up with a more user-friendly solution for my recursive continuation stack?

Answer 1

The answer to a related question hides the following rather useful trick: to generalize the title of the instance and specialize in the context of the instance.

 instance a ~ b => StackTo a Top b where runStack _ = id 

When choosing an instance to use, the GHC checks only the available chapters of the instance — not contexts — and selects the one (if any) that matches what is currently known about the type. He will not specialize in type before making this choice, even if specialization allows one or more available instance heads to match. So the difference between the instance given here and the question above is that it is more general: this one applies every time the middle type is Top , while yours only applies when the middle type is Top , and we only need to know about two other types to know that they are equal.

Yours will overlap with fewer other potential instances, but it will drive the output engine more.

Answer 2

Is there any special reason why the star Kleene GADT will not do this job?

 data Star rab where Nil :: Star raa Cons :: rab -> Star rbc -> Star rac compose :: Star (->) ab -> a -> b compose Nil = id compose (Cons f fs) = compose fs . f 

But if you need a class type approach, I would not intervene.