问题为什么Djinn没有实现共同的monadic功能？

我最近偶然发现了巨灵并简要介绍它，试着看看它在我的日常编码工作流程中是否有用。我很高兴看到Djinn有monad并试图看看它是否能够找到一些很酷的功能。

Djinn事实上确实有一些奇迹。最初（至少对我来说）非直观函数的类型签名 >>= (>>=) 是 Monad m => ((a -> m b) -> m a) -> (a -> m b) -> m b。 Djinn能够通过陈述立即揭开神秘的神秘面纱

Djinn> f ? Monad m => ((a -> m b) -> m a) -> (a -> m b) -> m b
f :: (Monad m) => ((a -> m b) -> m a) -> (a -> m b) -> m b
f a b = a b >>= b

不幸的是，尽管知道Monad类型类，但Djinn似乎无法在monad上找到其他标准函数。

join （应该是 join = (>>= id) 或者在Djinn中更详细的语法 join a = a >>= (\x -> x)）
```
Djinn> join ? Monad m => m (m a) -> m a
-- join cannot be realized.
```
liftM （应该是 liftM f = (>>= (return . f)) 或者在Djinn中更详细的语法 liftM a b = b >>= (\x -> return (a x))）
```
Djinn> liftM ? Monad m => (a -> b) -> m a -> m b
-- liftM cannot be realized.
```
即使是基本的 return :: Monad m => m a -> m (m a) Djinn或者找不到 return :: Monad m => (a, b) -> m (a, b)。
```
Djinn> f ? Monad m => (a, b) -> m (a, b)
-- f cannot be realized.
```

Djinn知道如何使用 \ 构建匿名函数，为什么会这样呢？

我粗略怀疑的是，也许Djinn有一个简单的类型类概念，并以某种方式对待 m a 如此“固定”那样 m (a, b) 不被视为一个案例 m a，但我不知道如何使其比现有的手工波浪形式更具体，或者直觉是否正确。

9108

2018-01-25 07:14

起源

正确支持类型类似于支持rank-2类型;比较：

join :: Monad m
     => m (m a) -> m a

VS：

join :: (forall a. a -> m a)
     -> (forall a b. m a -> (a -> m b) -> m b)
     -> m (m a) -> m a

不幸的是，Djinn使用的技术根本不处理rank-2类型。如果你漂浮起来让Djinn能够处理它，那么你突然得到的就是它具体选择：

join :: (b -> m b)
     -> (m c -> (c -> m d) -> m d)
     -> m (m a) -> m a

看起来很像你可以实现它！如果你告诉Djinn使用哪种实例，当然它会好很多。

join :: (b -> m b)
     -> (m (m a) -> (m a -> m a) -> m a)
     -> m (m a) -> m a

对于这个，Djinn将给予正确的实施。 ......但是，那是作弊。

2018-01-25 08:03

类型和等级2类型之间的关系非常酷;我以前从未想过它。我可以看到支持更高级别的类型可能会导致你需要为一般的一阶逻辑建立一个定理证明器，这似乎很难得到实际结果并且总体上是不可判定的。是否有必要完全支持类型类？ Djinn目前如何处理类型类并且可以延长吗？ - badcook

或者更清楚地陈述我的后续问题，似乎很清楚能够处理等级2类型足以处理类型类但是有必要吗？ - badcook

@badcook我认为通过为类型为rank-2的函数参数生成一个新的类型类，将处理类型类的Djinn正确地转换为处理rank-2类型的Djinn并不难。当然，魔鬼在细节中，我还没有弄清楚细节，所以我不确定。 - Daniel Wagner