Jak nazywa się ten funktor używający RankNTypes?

Question

Podczas gry wokół pakietu objective zauważyłem, że następujący typ ma interesującą właściwość.

> {-# LANGUAGE RankNTypes #-} 
> data N f r = N { unN :: forall x. f x -> (x, r) } 

To jest Funktor.

> instance Functor (N f) where 
> fmap f (N nat) = N $ fmap (fmap f) nat 
>   -- or, = N $ \fx -> let { (x,a) = nat fx } in (x, f a) 

Po kilku godzinach google/hoogle, dałem się znaleźć żadnych istniejący moduł, który zawiera tego typu. Co to jest ten typ? Jeśli jest dobrze znana, jak się nazywa? Czy jest to użyteczne, czy ignorowane, ponieważ bezużyteczne?

To nie jest moje 100% oryginalne dzieło, ponieważ N został wyprowadzony z Obiektu znalezionego w pakiecie celu.

> data Object f g = Object { 
>  runObject :: forall x. f x -> g (x, Object f g) 
> } 

N f jest funktora co daje Object f Identity gdy Fix wniosek.

---

Poniżej znajduje się fakt o tym typie i dlaczego uważam, że jest interesujący.

N przekształca program Reader to Writer, i na odwrót. (Tutaj użyłem (=) symbol izomorfizmu między typami)

N ((->) e) r 
= forall x. (e -> x) -> (x, r) 
= (e, r) 

N ((,) d) r 
= forall x. (d, x) -> (x, r) 
= d -> r 

N konwertuje Store comonad do monady państwa, ale odwrotna nie jest prawdziwa.

> data Store s a = Store s (s -> a) 
> type State s a = s -> (s, a) 

N (Store s) r 
= forall x. (s, (s -> x)) -> (x, r) 
= forall x. s -> (s -> x) -> (x, r) 
= s -> (s, r) 
= State s r 

N (State s) r 
= forall x. (s -> (s, x)) -> (x, r) 
= forall x. (s -> s, s -> x) -> (x, r) 
= forall x. (s -> s) -> (s -> x) -> (x, r) 
= (s -> s) -> (s, r) -- ??? 

N nie może brać Być może.

N Maybe r 
= forall x. Maybe x -> (x, r) 
= forall x. (() -> (x, r), x -> (x, r)) 
= Void  -- because (() -> (x, r)) can't be implemented 

Następujące funkcje mogą być zabawne. Nie mogłem tego zrobić odwrotnie.

> data Cofree f a = Cofree a (f (Cofree f a)) 
> data Free f a = Pure a | Wrap (f (Free f a)) 

> unfree :: Free (N f) r -> N (Cofree f) r 
> unfree (Pure r) = N $ \(Cofree a _) -> (a, r) 
> unfree (Wrap n_f) = N $ 
> \(Cofree _ f) -> let (cofree', free') = unN n_f f 
>     in unN (unfree free') cofree' 

Cały wpis jest piśmienny Haskell (.lhs).

Answer 1

Nazywam to funktorem "opiekunem". Object byłeś zdefiniowany za pomocą funktora przewodnika przed zwolnieniem celu.

Tak, ten funktor jest interesujący - Cofree (Handler f) ma publicznego gettera, a Free (Handler f) to mortal object. Być może powinienem był wysłać funktorowi przewodnika ...

Answer 2

Chociaż już udzielono odpowiedzi, sam znalazłem inną odpowiedź na to pytanie.

Typ N był reprezentacją poziomu klasy Pairing, opisaną w poniższych artykułach.

Free for DSLs, cofree for interpreters

Cofree Comonads and the Expression Problem (Okrawki nazywa Podwójny tutaj)

Parowanie i N są same rzeczy

Definicja powiązanie jest to.

> class Pairing f g where 
> pair :: (a -> b -> c) -> f a -> g b -> c 

f i N f jest Parowanie.

> instance Pairing f (N f) where 
> pair k fa nb = uncurry k $ unN nb fa 

N może być reprezentowany w kategoriach Parowanie.

> data Counterpart f r = forall g. Pairing f g => Counterpart (g r) 
> 
> iso1 :: N f r -> Counterpart f r 
> iso1 = Counterpart 
> 
> iso2 :: Counterpart f r -> N f r 
> iso2 (Counterpart gr) = N $ \fx -> pair (,) fx gr 

Jest Free-vs-Cofree instancji, który odpowiada moim unfree. Inne interesujące przykłady są również zdefiniowane w artykułach.

> instance Pairing f g => Pairing (Free f) (Cofree g) where 
> pair = undefined -- see link above 

Wydłużenie parowanie PairingM do obiektu

poprzedniego artykułu goes to rozszerzenie parowanie wykonać obliczenie wewnątrz Monad m.

> class PairingM f g m | f -> g, g -> f where 
> pairM :: (a -> b -> m r) -> f a -> g b -> m r 

Jeśli przepisujemy PairingM na formularz podobny do N, otrzymamy obiekt ponownie.

> -- Monad m => HandlerM' f m r ~ HandlerM f m r 
> data HandlerM' f m r = forall g. PairingM f g m => HandlerM' (g r) 
> data HandlerM f m r = HandleM { runHandlerM :: forall x. f x -> m (x, r) } 
> 
> -- Fix (HandlerM f m) ~ Object f m 
> -- Free (HandlerM f m) ~ (mortal Object from f to m)