haskell - 有没有办法用这个签名写一个函数？

Question

我有一个函数正在做一些当前使用特定数据类型的事情。我想知道我是否可以使它成为将军。这是它的签名的通用版本:

f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d

如果上面写不出来，也许更受限制的版本可以？

f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b

Answer 1

不，这是不可能的，至少没有非终止或不安全的操作是不可能的。

该参数本质上类似于 this one : 我们利用 f居住在我们知道不能居住的类型中。

假设存在

f :: Monad m => ((a -> b) -> c -> d) -> (a -> m b) -> m c -> m d

专精 c ~ ()

f :: Monad m => ((a -> b) -> () -> d) -> (a -> m b) -> m () -> m d

因此

(\g h -> f (\x _ -> g x) h (return ()))
  :: Monad m => ((a -> b) -> d) -> (a -> m b) -> m d

特化 d ~ a .

(\g h -> f (\x _ -> g x) h (return ()))
  :: Monad m => ((a -> b) -> a) -> (a -> m b) -> m a

特化 m ~ Cont t

(\g h -> runCont $ f (\x _ -> g x) (cont . h) (return ()))
  :: ((a1 -> b) -> a) -> (a1 -> (b -> r) -> r) -> (a -> r) -> r

拿 h = const

(\g -> runCont $ f (\x _ -> g x) (cont . const) (return ()))
  :: ((r -> b) -> a) -> (a -> r) -> r

因此

(\g -> runCont (f (\x _ -> g x) (cont . const) (return ())) id)
  :: ((r -> b) -> r) -> r

因此，类型 ((r -> b) -> r) -> r是有人居住的，因此通过 Curry-Howard 同构它对应于命题直觉逻辑的定理。但是，公式 ((A -> B) -> A) -> A是 Peirce's law众所周知，在这种逻辑中是不可证明的。

我们得到一个矛盾，因此不存在这样的 f .

相比之下，类型

f2 :: Monad m => ((a -> a) -> b -> b) -> (a -> m a) -> m b -> m b

居住在这个词中

f2 = \ g h x -> x

但我怀疑这不是你真正想要的。