Agfdhyk

The following type family

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where  

  ListVariadic (a ': as) b = a -> ListVariadic as b

  ListVariadic '       b = b

is visibly not injective, e.g. ListVariadic ' (a -> a) ~ ListVariadic '[a] a.

However it is very convenient to have injectivity to help type inference along, and I don't intend to use ListVariadic with its second argument being a function type.

I have come up with two workarounds, both quite unsatisfactory:

Option 1: Pass around type families that witness a left inverse to ListVariadic (through type-classes).

type family Arguments (f :: Type) :: [Type] where

  Arguments (a -> b) = a ': Arguments b

  Arguments b        = '

type family Return (f :: Type) :: Type where

  Return (a -> b) = Return b

  Return b        = b



class    ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where

instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where

For me this eventually introduced too much complexity, having to thread these helper typeclasses throughout.

Option 2. Explicitly list all non-function types that one is going to be using, in the definition of the variadic type family:

type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where  

  ListVariadic (a ': as) b = a -> ListVariadic as b

  ListVariadic ' ()     = ()

  ListVariadic ' Bool   = Bool

  ListVariadic ' Word   = Word 

  ListVariadic ' Int    = Int 

  ListVariadic ' Float  = Float

  ListVariadic ' Double = Double

  ... ... ...

  ListVariadic ' (a,b) = (a,b)

  ListVariadic ' (a,b,c) = (a,b,c)

  ... ... ...

  ListVariadic ' [a] = [a]

  ... ... ...

Then an injectivity annotation is possible and works as intended. It's obviously quite limited... and one still ends up with constraints of the form a ~ ListVariadic ' a that need to be passed around.

I was hoping there to be a way of writing the ListVariadic type family (or something fulfilling the same purpose), indicating that its second argument is not a function, and allow an injectivity annotation.

I know I am doubly in trouble, because in the provided first definition of ListVariadic, the second equation has a bare type variable on the right hand side. That's generally not allowed when checking for injectivity... but perhaps there are some clever tricks using type synonyms that can work around this problem?