2016-04-29 2 views
11

Во время игры около objective package, я заметил, что следующий тип имеет интересное свойство.Как называется этот функтор, который использует RankNTypes?

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

Это Functor.

> 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) 

Через несколько часов Google/hoogle, я отказался найти любой существующий модуль, который включает в себя этот тип. Что это за тип? Если известно, какое имя? Это полезно или игнорируется, потому что бесполезно?

Это не мое 100% оригинальное творение, потому что N было получено из объекта, найденного в объективном пакете.

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

N f является функтором, который дает Object f Identity, когда Фикс применяется.


Следующий факт об этом типе и почему я думал, что это интересно.

N конвертирует считыватель в Writer, наоборот. (Здесь я) символ (= для изоморфизма между типами)

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

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

N преобразует магазин комонадой в государственный монады, но обратное не верно.

> 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 не может принять Возможно.

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

Следующая функция может быть интересной. Я не мог сделать это наоборот.

> 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' 

Весь пост является грамотным Haskell (.lhs).

+2

я не знаю имя, но записать его как '(ForAll х FX ​​-.> ((,) Г) х)' и становится чем-то, что может быть передан в 'Control.Comonad.Cofree. hoistFree'. – Gurkenglas

+1

@chi В 'N' нет' g'. Он устанавливает 'g ~ Identity' в' Object f g'. Если вы отбросите неинтересную «Идентификацию» от 'forall x. f x -> Identity (x, Object f Identity) 'вы получаете' forall x. f x -> (x, Object f) '. Если вы замените рекурсивное появление 'Object f' новым параметром' r', вы получите 'forall x. f x -> (x, r) ', что является' N f r'. 'Fix (N f)' помещает рекурсивное вхождение обратно туда, где был 'r'. – Cirdec

+0

Это выглядит как ['Ran'] (https://hackage.haskell.org/package/profunctors/docs/Data-Profunctor-Ran.html#t:Ran), но смешивает и сопоставляет профинансы и бифунторы. 'forall x. f x -> x' - это индекс в 'f'. Другая часть - читатель из среды «forall x». f x', считая структуру 'f', но не ее значения. – Cirdec

ответ

2

Я называю это «обработчиком» функтором. Object раньше определялся с помощью функтора обработчика до того, как я выпустил цель.

Да, этот функтор интересен - Cofree (Handler f) имеет публичный геттер и Free (Handler f) - mortal object. Может быть, я должен был отправить обработчика-функтора ...

1

Хотя он уже ответил, я нашел другой ответ на вопрос сам.

Тип N - это представление уровня уровня класса Pairing, описанное в следующих статьях.

Free for DSLs, cofree for interpreters

Cofree Comonads and the Expression Problem (кожура называется Dual здесь)

Сопряжение и N такие же вещи

Определение спариванием это.

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

f и N f является спаривание.

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

N можно представить с точки зрения сопряжения.

> 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 

Существует бесплатное-против-косвободным экземпляр, который соответствует моему unfree. Другие интересные примеры также определены в статьях.

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

Расширение Сопряжение с PairingM на объект

бывшая статья goes to расширения Сопряжение делать вычисления внутри монады м.

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

Если мы перепишем PairingM в форму, аналогичную N, мы снова получим объект.

> -- 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) 
Смежные вопросы