haskell - 为什么 Djinn 无法实现常见的一元函数？

Question

我最近偶然发现了Djinn并且短暂地使用它来尝试看看它在我的日常编码工作流程中是否有用。我很高兴看到 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 对 typeclass 有一个简单的概念，并且以某种方式对待 m a作为“固定”，以便 m (a, b)不被视为 m a 的情况，但我不知道如何使它比当前的手波形式更具体，也不知道这种直觉是否正确。

Answer 1

正确支持类型类看起来很像支持 rank-2 类型；相比:

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

与:

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

不幸的是，Djinn 使用的技术根本无法处理 2 级类型。如果您将 foralls float 以便 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 将给出正确的实现。 ...但是，那是作弊。