Подтвердить что ты не робот

Как называется этот функтор, который использует RankNTypes?

Во время воспроизведения вокруг objective пакета я заметил, что следующий тип имеет интересное свойство.

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

Это функтор.

> 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 было получено из Object, найденного в объективном пакете.

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

N f - это Functor, который дает Object f Identity, когда Fix применяется к.

Ниже приведена информация об этом типе и почему я думал, что это интересно.

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

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

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

N конвертирует Хранить comonad в State monad, но инверсия неверна.

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

4b9b3361

ОТВЕТЫ

Ответ 1

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

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

Ответ 2

Хотя он уже ответил, я нашел еще один ответ на этот вопрос.

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

Бесплатно для DSL, cofree для интерпретаторов

Cofree Comonads и проблема выражения (Paring называется 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

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

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

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

Бывшая статья переходит к, расширяющему Сопряжение, чтобы выполнять вычисления внутри Monad m.

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