Inverse injective type families

11
votes

Lets say I have an injective type family T

type family T a = b | b -> a

My first question is there an way to write:

type family T' = the inverse of T

Without having to repeat all the instances of T but in reverse.

Such that: T (X1 a (T' a)) = a

It seems like this should work, as both T and T' are injective, given one side it is mechanical to work out the other.

Anyway to write T'?

1
haskelltype-families
Wouldn't a ~ T b work ? – mb14
Apparently type Tinv b = a is rejected because the tyvar a must be mentioned in the arguments of Tinv, which looks too restrictive when it is determined by them thanks to the fundeps in scope. – chi
It is impossible to convert the fundep to an explicit type family application, but as @mb14 said, using an equality constraint in a type signature you can compute the inverse - e.g. (a ~ T b) => Proxy a -> Proxy b or equivalently Proxy (T b) -> Proxy b. – user2407038
Injective type families smell like a language feature in progress. Their restrictions (such as not allowing any type family applications in the RHS) are extremely unnatural. – dfeuer

1 Answers

7
votes

With suitable extensions, one can write:

type T' b = forall a. T a ~ b => a

For example, here's an example showing that you get at least basic type compatibility with this type synonym:

type family T a = b | b -> a
type instance T Int = Bool

f :: T' Bool -> Int
f x = x