Допустим, у меня есть инъективное семейство типов T
type family T a = b | b -> a
Мой первый вопрос: есть ли способ написать:
type family T' = the inverse of T
Без повторения всех экземпляров T, но наоборот.
Таким образом: T (X1 a (T' a)) = a
Кажется, что это должно работать, поскольку как T, так и T' являются инъективными, поскольку одна сторона механически работает над другой.
В любом случае написать T'?
С помощью подходящих расширений можно написать:
type T' b = forall a. T a ~ b => a
Например, пример, показывающий, что вы получаете совместимость с базовым типом с синонимом этого типа:
type family T a = b | b -> a
type instance T Int = Bool
f :: T' Bool -> Int
f x = x