haskell 这个使用RankNTypes的函子的名字是什么？

z9gpfhce 于 9个月前发布在其他

关注(0)|答案(3)|浏览(67)

在玩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/hocker，我放弃了寻找任何现有的模块，包括这种类型。* 这是什么类型？* 如果它是众所周知的，它的名字是什么？这是有用的，还是因为没用而被忽视？
这不是我100%的原创，因为N是从objective包中找到的Object派生出来的。

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

N f是一个函子，当Fix应用于时，它会产生Object f Identity。
下面是关于这种类型的一个事实，以及为什么我认为它很有趣。
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将Store 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 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）。

haskell

来源：https://stackoverflow.com/questions/36929014/what-is-the-name-of-this-functor-that-uses-rankntypes

3条答案

按热度按时间

guicsvcw1#

我称之为“处理程序”函子。在我发布objective之前，Object通常是使用处理函数来定义的。
是的，这个函子很有趣--Cofree (Handler f)有一个公共getter，而Free (Handler f)是一个mortal object。也许我应该把处理函数.

赞(0）回复(0）举报 9个月前

qpgpyjmq2#

虽然这个问题已经有了答案，但我自己找到了另一个答案。
类型N是类型类Pairing的值级别表示，在下面的文章中描述。
Free for DSLs, cofree for interpreters
Cofree Comonads and the Expression Problem（在这里，配对被称为对偶）

配对和`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-Anchorree示例，对应于我的unfree。其他有趣的例子也在文章中定义。

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

将Pairing扩展为PairingM to Object

以前的文章goes to扩展配对在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的形式，我们再次获得Object。

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

赞(0）回复(0）举报 9个月前

rryofs0p3#

Application接口可以用各种方式实现，例如，可以实现（**）来代替liftA 2。

(**) :: Applicative f => f a -> f b -> f (a, b)
(**) = liftA2 (,)

你可以将其理解为返回一个我们称之为Curried的数据类型：

(**) :: Applicative f => f a -> (forall b. f b -> f (a, b))
     :: Applicative f => f a -> Curried f f a
     :: Applicative f => f   ~> Curried f f

我们将Curried定义为

type    Curried :: (Type -> Type) -> (Type -> Type) -> (Type -> Type)
newtype Curried f g a = Curried (forall b. f b -> g (a, b))

在kan-extensions包中，它实际上被定义为：

type    Curried :: (Type -> Type) -> (Type -> Type) -> (Type -> Type)
newtype Curried f g a = Curried (forall b. f (a -> b) -> g b)

它来自（<*>）运算符

flip (<*>)
    :: Applicative f => f a -> f (a -> b) -> f b
    :: Applicative f => f a -> (forall b. f (a -> b) -> f b)
    :: Applicative f => f a -> Curried f f a
    :: Applicative f => f   ~> Curried f f

所以你可以把N看作是Curried f Identity。

{-# Language DerivingVia #-}

type    N :: (Type -> Type) -> Type -> Type
newtype N f r = N (forall x. f x -> (r, x))
  deriving Functor
  via Curried f Identity

对于有明确想法的人来说，咖喱是日卷积的右伴随（日f -1）。|Curried f），所以这是一个自然同构：

Day f g -> h
      <->
g -> Curried f h

日卷积的定义类似，但相反：所以量化是存在的

liftA2
    :: Applicative f => (a -> b -> c) -> (f a -> f b -> f c)
    :: Applicative f => (exists a b. (a -> b -> c, f a, f b)) -> f c
    :: Applicative f => Day f f c -> f c
    :: Applicative f => Day f f   ~> f

type Day :: (Type -> Type) -> (Type -> Type) -> (Type -> Type)
data Day f g a where
  Day :: (a -> b -> c) -> (f a -> g b -> Day f g c)

赞(0）回复(0）举报 9个月前

我来回答

haskell 这个使用RankNTypes的函子的名字是什么？

3条答案

配对和`N`是一回事

将Pairing扩展为PairingM to Object

相关问题

热门标签

最新问答

haskell 这个使用RankNTypes的函子的名字是什么？

3条答案

配对和N是一回事

将Pairing扩展为PairingM to Object

相关问题

热门标签

最新问答

配对和`N`是一回事