Inverting a Type Family

7
votes

I've got a "linear" type family, i.e. of the form

type family Foo a
type instance Foo T1 = T2
type instance Foo T2 = T3
...
type instance Foo T9 = T10

In my particualr use-case, it is very convenient to define the "reverse" family FooRev and then enforce the constraint (FooRev (Foo x) ~ x):

type family FooRev a
type instance FooRev T10 = T9
type instance FooRev T9 = T8
...
type instance FooRev T2 = T1

The reverse family allows GHC to infer many types that would otherwise be ambiguous due to non-injectivity. It is essentially the same idea that was proposed here. This solution works pretty well, but it is annoying, programatic, and error-prone to have to define a "reverse" type family by listing out all the cases. Is there a more generic way to define the reverse of a linear family such as Foo?

2
haskelltype-families
Maybe you could use data families instead somehow, which are known injective. Not sure if it fits your problem. – luqui
Metaprogramming (i.e. Template Haskell) might generate both, keeping your code DRY if that's your concern. Otherwise, you could define a type-level association list, a type level lookup, a type level map swap, and derive both type families from the list. – chi
@luqui I just saw that before posting, but as far as I know, that's not really what I need. In my case, the Ti are all type Bar a b c where the type parameters change. That won't fit into a data family, will it? – crockeea
@chi Perhaps you could demonstrate one of those ideas? – crockeea

2 Answers

5
votes

I think FunctionalDependencies should be the best solution for your case:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

class Foo a b | a -> b, b -> a
instance Foo T1 T2
instance Foo T2 T3
...

Now each b can be inferred from an a and vice versa.

5
votes

I decided to give @chi's idea try, and but I came up with something a little simpler in the end. 

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies #-}

type family NextElt (a :: *) (xs :: [*]) where
  NextElt a (a ': b ': cs) = b
  NextElt a (b ': c ': cs) = NextElt a (c ': cs)

type family PrevElt (a :: *) (xs :: [*]) :: * where
  PrevElt a (b ': a ': xs) = b
  PrevElt a (b ': c ': xs) = PrevElt a (c ': xs)

data T1
data T2
data T3
type TSeq = '[T1, T2, T3]

type NextRp a = NextElt a TSeq
type PrevRp a = PrevElt a TSeq

Using a type list to represent the linear sequence of types allows me to express the relationship without writing each type twice (which is necessary using type family instances or instances of a class). The type families above uses a sliding-window approach to search for an element in a list with a previous or next element. These type families are generic (and can be extended to work for non-* kinds using Data.Type.Equality.)