Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Inverting a Type Family

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?

like image 231
crockeea Avatar asked Oct 24 '14 05:10

crockeea


2 Answers

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.

like image 70
András Kovács Avatar answered Nov 08 '22 16:11

András Kovács


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.)

like image 43
crockeea Avatar answered Nov 08 '22 16:11

crockeea