Convincing the compiler that there is a valid instance chain

Question

All right. The problem here is pretty abstract. Bear with me.

I have a bunch of "Units", that each have certain properties. These properties are defined in the Seq class, like this:

class Seq a x y where
    break :: x -> (a, y)
    build :: a -> y -> x

Conceptually, the a type is the important type, x is the context used to generate an a, and y is the context used to generate any further Seq instances. break breaks the Seq down, build allows you to reconstruct it.

On individual Seq instances, this works fine. However, I also have a data constructor that looks like this:

data a :/: b = a :/: b deriving (Eq, Ord)
infixr :/:

The goal of this whole operation is to be able to compose Seq instances.

For example, if I have a, b, and c all instances of Seq such that a's context feeds into b and b's feeds into c, then I should automatically have a Seq instance for a :/: b :/: c. The class to set this up is fairly simple through the recursive data type:

instance (Seq a x y, Seq b y z) => Seq (a :/: b) x z where
    break x = let
        (a, y) = break x :: (a, y)
        (b, z) = break y :: (b, z)
        in (a :/: b, z)

    build (a :/: b) z = let
        y = build b z :: y
        x = build a y :: x
        in x

The problem is that I can't seem to use it. If I define the following three Seq instances:

data Foo
instance Seq Foo Integer Bool

data Bar
instance Seq Bar Bool Bar

data Baz
instance Seq Baz Bar ()

(implementation details redacted, see here for more)

and a well-typed break function:

myBreak :: Integer -> (Foo :/: Bar :/: Baz)
myBreak = fst . break' where
    break' = break :: Integer -> (Foo :/: Bar :/: Baz, ())

then I can't even compile:

No instances for (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
  arising from a use of `break'
Possible fix:
  add instance declarations for
  (Seq Foo Integer y, Seq Bar y y1, Seq Baz y1 ())
In the expression: break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for break':
    break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())
In an equation for `myBreak':
    myBreak
      = fst . break'
      where
          break' = break :: Integer -> (Foo :/: (Bar :/: Baz), ())

It looks to me like myBreak can't be sure that there's a "working thread" of contexts from Foo → Bar → Baz. How can I convince the compiler that this is well-typed?

This is one of my first excursions into type programming, so I'm undoubtedly breaking some well-established rules. I'm quite curious as to what I'm doing wrong here, but I'm also open to suggestions as to how better achieve my goals.

Answer 1

You will probably need another language extension or two to make this work. The general problem is that multi-parameter type classes need to encode the open world assumption so, suppose someone came along and added

instance Seq Bar Integer Float

instance Seq Baz Float ()

the compiler would have no way of knowing which set of instances to use. This could potentially cause undefined behavior. If the compiler just "figured out" that no other instances were available so you must have meant these then you would be in the awkward situation of having code that could break because somebody added an instance.

The solution is to use some kind of type level function. So, if a is the important type, then perhaps there is just one combination of x and y that goes with that a. One way of doing this is with functional dependencies.

class Seq a x y | a -> x, a -> y where
   break :: x -> (a, y)
   build :: a -> y -> x

Functional dependencies are quite general, and can be used two encode bijective type functions

class Seq a x y | a -> x, a -> y, x y -> a where
   break :: x -> (a, y)
   build :: a -> y -> x

It depends on what exactly the semantics you want are. Alternatively, you can use the slightly more elegant "associated type synonym" approach using the type families extension.

class Seq a where
   type X a
   type Y a
   break :: X a -> (a, Y a)
   build :: a -> Y a -> X a

instance Seq Bar where
   type X Bar = Bool 
   type Y Bar = Bar

This version is currently considered the most idiomatic, and has some advantages over the functional dependancies version (although, you cant encode bijection this way). For completeness, this is equivalent to

type family X a
type instance X Bar = Bool

type family Y a
type instance Y Bar = Bar

class Seq a where
   break :: X a -> (a, Y a)
   build :: a -> Y a -> X a

instance Seq Bar

To editorialize: Haskell constraint solving mechanism with multi parameter type classes is a logic language kinda like prolog. As much as possible you should use functions instead of relations when type level programming. Three reasons:

1. You can get from a function to a constraint but not vice versa
2. Haskell is not prolog. Most Haskell programmers find functions easier to reason about. If you dont know Prolog (or another logic language), its extra important to stick to functions since the difference between relational and functional programming is almost as big as the difference between functional and imperative programming.
3. Despite similarities, Haskell's constraint solver is NOT Prolog (intuitively all clauses have a cut immediately after the head, dont worry if you dont know what this means). Relational type programming is much harder than coding in a language with full backtracking.

My recommendation is know both functional dependencies and type functions. Type functions fit in a little better with the rest of the language, but sometimes functional dependencies are the best tool for the job.