odwrotne rodziny injective typu

Powiedzmy mam injective rodzinę typu Todwrotne rodziny injective typu

type family T a = b | b -> a

Moje pierwsze pytanie czy istnieje sposób, aby napisać:

type family T' = the inverse of T

bez konieczności powtarzania wszystkich wystąpień T ale w odwrotnej kolejności.

taka, że: T (X1 a (T' a)) = a

Wydaje się, że to powinno działać, ponieważ zarówno T i T' są injective, biorąc pod uwagę z jednej strony jest to mechaniczny wypracować drugiej.

W każdym razie napisać: T'?

Źródło

2016-08-14 Clinton

Czy nie 'a ~ T b' działa? – mb14

Wygląda na to, że 'typ Tinv b = a' jest odrzucany, ponieważ tyvar' a' musi być wymieniony w argumentach 'Tinv', który wygląda zbyt restrykcyjnie, gdy jest określany przez nich dzięki danym w przybliżeniu. – chi

Nie można przekonwertować kapitalnego na jawną aplikację rodzinną typu, ale jak powiedział @ mb14, przy użyciu ograniczenia równości w sygnaturze typu można obliczyć odwrotność - np. '(a ~ T b) => Proxy a -> Proxy b' lub równoważnie' Proxy (T b) -> Proxy b'. – user2407038

z odpowiednimi rozszerzeniami, można napisać:

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

Na przykład, oto przykład pokazujący, że masz przynajmniej podstawową zgodność typu z tego typu synonim:

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

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

Źródło

2018-01-27 00:15:21

Odpowiedz

Powiązane problemy