Profunctors的自由单子的模拟

Question

我们可以定义data Free f a = Pure a | Free (f (Free f a))，也可以定义Functor f => Monad (Free f)。

如果我们定义data T f a b = R a | S b | T (f a (T f a b))，我们有一些类似的M，所以Profunctor f => M (T f a)，其中class Profunctor f where dimap :: (a -> b) -> (c -> d) -> f b c -> f a d

自从我注意到Data.Comp.Term.Context和Free在Data.Comp.Param.Term.Context的潜在类似物上是同构的，我就一直在想。

Answer 1

有一个更合适的概念，那就是从profunctor中创建一个免费的东西。然后我们就可以通过类比来工作了。

由集合X生成的自由么半群Y可以看作是方程"Y=1+XY“的解。在Haskell表示法中，即

data List a = Nil | Cons a (List a)

由函子F生成的自由单子M可以被认为是方程"M=1+FM“的解，其中乘积”FM“是函子的组合。1就是单位函子。

data Free f a = Pure a | Free (f (Free a))

从形式函数P中释放一些东西应该看起来像是"A=1+PA“的解决方案A。产品"PA“是标准的composition of profunctors。1是“标识”的profunctor，(->)。所以我们得到了

data Free p a b = Pure (a -> b) | forall x.Free (p a x) (Free p x b)

这也是一个profunctor：

instance Profunctor b => Profunctor (Free b) where
    lmap f (Pure g) = Pure (g . f)
    lmap f (Free g h) = Free (lmap f g) h
    rmap f (Pure g) = Pure (f . g)
    rmap f (Free g h) = Free g (rmap f h)

如果profunctor很强大，那么免费版本也是如此：

instance Strong p => Strong (Free p) where
    first' (Pure f) = Pure (first' f)
    first' (Free f g) = Free (first' f) (first' g)

但是Free p到底是什么呢？它实际上是一种叫做pre-arrow的东西。受限的、自由的、强大的profunctors是箭头：

instance Profunctor p => Category (Free p) where
    id = Pure id
    Pure f . Pure g = Pure (f . g)
    Free g h . Pure f = Free (lmap f g) h
    Pure f . Free g h = Free g (Pure f . h)
    f . Free g h = Free g (f . h)

instance (Profunctor p, Strong p) => Arrow (Free p) where
    arr = Pure
    first = first'

直观地说，您可以将profunctor P a b的元素想象为将a-ish thing转换为b-ish thing，典型的示例由(->)给出。Free P是这些元素的未评估链，具有兼容(但不可观察)的中间类型。

Answer 2

所以我想我弄明白了：M ~ Monad☺

instance Profunctor f => Functor (T f a) where
    fmap f (In m) = In (dimap id (fmap f) m)
    fmap f (Hole x) = Hole (f x)
    fmap f (Var v) = Var v

instance Profunctor f => Applicative (T f a) where
    pure = Hole
    (<*>) = ap

instance Profunctor f => Monad (T f a) where
    In m >>= f = In ((>>= f) <$> m)
    Hole x >>= f = f x
    Var v >>= _ = Var v

在事后的思考中似乎很明显。