如何从 Haskell 中的内部参数中提取信息？

Question

在大多数支持可变变量的编程语言中，可以轻松实现类似以下 Java 示例：

interface Accepter<T> {
    void accept(T t);
}

<T> T getFromDoubleAccepter(Accepter<Accepter<T>> acc){
    final List<T> l = new ArrayList<T>();
    acc.accept(new Accepter<T>(){

        @Override
        public void accept(T t) {
            l.add(t);
        }

    });
    return l.get(0); //Not being called? Exception!
}

只是对于那些不懂Java的人来说，上面的代码接收到的东西可以提供一个带一个参数的函数，并且它应该以这个参数作为最终结果。

这不像callCC：没有控制流交替。只关心内部函数的参数。

我认为 Haskell 中的等效类型签名应该是

getFromDoubleAccepter :: (forall b. (a -> b) -> b) -> a

因此，如果有人可以为您选择的类型提供函数(a -> b) -> b，那么他必须已经拥有a。因此，您的工作是给他们一个“回调”，而不是记住他们发送给您的任何内容，一旦他们返回给您，请将 那个 值返回给您的调用者。

但我不知道如何实现这一点。我能想到几种可能的解决方案。虽然我不知道它们每个是如何工作的，但我可以根据预期的困难对它们进行评分和排序：

• Cont 或 ContT 单子。我认为这是最简单的。

• RWS monad 或类似的。

• 任何其他单子。 纯像Maybe这样的单子我认为更难。

• 仅使用标准的纯功能特性，如惰性求值、模式匹配、定点污染器等。我认为这是最难的（甚至是不可能的）。

我希望看到使用上述任何技术的答案（并且更喜欢更难的方法）。

注意：不应该对类型签名做任何修改，解决方案应该和Java代码做的一样。

更新

一旦我看到有人评论了getFromDoubleAccepter f = f id，我就意识到我做错了。基本上我使用forall 只是为了让游戏更容易，但看起来这种扭曲太容易了。实际上，上面的类型签名强制调用者传回我们给他们的任何东西，所以如果我们选择a作为b，那么该实现给出了相同的预期结果，但它只是...... . 没想到。

其实我想到的是一个类型签名，比如：

getFromDoubleAccepter :: ((a -> ()) -> ()) -> a

而这一次更难了。

另一位评论作者要求推理。我们来看一个类似的函数

getFunctionFromAccepter :: (((a -> b) -> b) -> b) -> a -> b

这个有一个幼稚的解决方案：

getFunctionFromAccepter f = \a -> f $ \x -> x a

但在下面的测试代码中它在第三个失败：

exeMain = do
    print $ getFunctionFromAccepter (\f -> f (\x -> 10)) "Example 1" -- 10
    print $ getFunctionFromAccepter (\f -> 20) "Example 2" -- 20
    print $ getFunctionFromAccepter (\f -> 10 + f (\x -> 30)) "Example 3" --40, should be 30

在失败的情况下，我们传递了一个返回30 的函数，我们希望得到该函数。然而最终结果又是40，所以它失败了。有什么方法可以实现只是做我想做的事吗？

如果这可以在 Haskell 中完成，那么会有很多有趣的序列。例如，元组（或其他“代数”类型）也可以定义为函数，因为我们可以说类似type (a,b) = (a->b->())->() 并以此实现fst 和snd。这就是我在其他几种没有原生“元组”支持但具有“闭包”功能的语言中使用的方式。

Answer 1

accept 的类型是 void accept(T)，所以等效的 Haskell 类型是 t -> IO ()（因为 Java 中的每个函数本质上都是 IO）。因此getFromDoubleAccepted可以直接翻译为

import Data.IORef

type Accepter t = t -> IO ()

getFromDoubleAccepter :: Accepter (Accepter a) -> IO a
getFromDoubleAccepter acc = do
    l <- newIORef $ error "Not called"
    acc $ writeIORef l
    readIORef l

如果您想要在 Haskell 中使用惯用的非 IO 解决方案，除了尝试模仿一些 Java 模式之外，您还需要更具体地了解您的实际最终目标。

编辑：关于更新

getFromDoubleAccepter :: ((a -> ()) -> ()) -> a

对不起，这个签名绝不等同于 Java 版本。你的意思是，对于任何a，给定一个函数，该函数接受一个接受a 但不返回任何东西或做任何副作用的函数，你想以某种方式变出一个a 类型的值。满足给定签名的唯一实现本质上是：

getFromDoubleAccepter :: ((a -> ()) -> ()) -> a
getFromDoubleAccepter f = getFromDoubleAccepter f

Answer 2

首先，我会尽可能地音译。我将把这些计算提升到一个 monad，因为 accept 返回 void（在 Haskell-land 中阅读 ()），除非有一些影响，否则这是无用的。

type Accepter m t = t -> m ()

getFromDoubleAccepter :: (MonadSomething m) => Accepter m (Accepter m t) -> m t
getFromDoubleAccepter acc = do
    l <- {- new mutable list -}
    acc $ \t -> add l t
    return (head l)

当然，我们不能制作这样的可变列表，所以我们必须在这里使用一些直观的火花。当一个动作只是将一个元素添加到某个累加器时，我会想到 Writer monad。所以也许那行应该是：

    acc $ \t -> tell [t]

由于您只是在最后返回列表的头部，这没有任何影响，我认为签名应该变成：

getFromDoubleAccepter :: Accepter M (Accepter M t) -> t

M 是一个合适的单子。它需要能够写[t]s，这样给我们：

type M t = Writer [t]

getFromDoubleAccepter :: Accepter (M t) (Accepter (M t) t) -> t

现在这个函数的类型告诉我们如何编写它的其余部分：

getFromDoubleAccepter acc = 
    head . execWriter . acc $ \t -> tell [t]

我们可以检查它是否做了一些事情......

ghci> getFromDoubleAccepter $ \acc -> acc 42
42

我猜这似乎是对的。我仍然有点不清楚这段代码应该是什么意思。

类型签名中明确的M t 在美学上对我来说有点麻烦。如果我知道我正在解决什么问题，我会仔细研究。如果您的意思是参数可以是命令序列，但没有可用的计算功能，那么您可以将类型签名专门用于：

getFromDoubleAccepter :: (forall m. (Monad m) => Accepter m (Accepter m t)) -> t

这仍然适用于我们的示例。当然，这有点傻。考虑

   forall m. (Monad m) => Accepter m (Accepter m t))
=  forall m. (Monad m) => (t -> m ()) -> m ()

这种类型的函数唯一能做的就是用各种ts 依次调用它的参数，然后返回()。这种函数中的信息完全由ts 来表征[1]，所以我们可以很容易地使用

getFromDoubleAccepter :: [t] -> t
getFromDoubleAccepter = head

---

[1] 只要我什么都不做，我还不如说在无穷大面前这不太准确。计算

crazy :: Integer -> Accepter m (Accepter m Integer)
crazy n acc = crazy (n+1) >> acc n

可以用来组成无限序列

... >> acc 3 >> acc 2 >> acc 1 >> acc 0

没有第一个元素。如果我们试图将其解释为列表，则在尝试查找第一个元素时会出现无限循环。然而，这个计算比无限循环有更多的信息——如果我们使用Last monoid 来解释它而不是列表，我们将能够在最后提取0。原来如此

forall m. (Monad m) => Accepter m (Accepter m t)

与比列表更一般的东西同构；特别是一个免费的幺半群。

Answer 3

感谢上面的回答，我终于得出结论，在 Haskell 中我们可以做一些与其他语言不同的事情。

其实这篇文章的动机是翻译著名的“single axiom classical logic reduction system”。我已经用其他一些语言实现了这一点。实施起来应该没问题

Axiom: (a|(b|c)) | ((d|(d|d)) | ((e|b) | ((a|e) | (a|e))))

但是，由于减少规则看起来像

Rule: a|(b|c), a |-- c

需要提取内部参数作为最终结果。在其他语言中，这是通过使用诸如可变槽之类的副作用来完成的。但是，在 Haskell 中，我们没有可变插槽，涉及 IO 会很丑，所以我一直在寻找解决方案。

乍一看（如我的问题所示），getFromDoubleAccepter f = f id 似乎是无稽之谈，但我意识到它在这种情况下确实有效！例如：

rule :: (forall r.a -> (b -> c -> r) -> r) -> a -> c
rule abc a = abc a $ flip const

技巧还是一样的：因为存在限定对调用者隐藏了r，而由被调用者为其选择类型，我们可以将c指定为r，所以我们只需应用给定的函数即可获得结果。另一方面，给定函数必须使用我们的输入来产生最终答案，因此它有效地将实现限制在我们真正想要的范围内！

把它们放在一起，看看我们能用它做什么：

newtype I r a b = I { runI :: a -> b -> r }

rule :: (forall r. I r a (I r b c)) -> a -> c
rule (I abc) a = abc a (I (\b c -> c))

axiom :: I r0 (I r1 a (I r2 b c)) 
          (I r0 (I r3 d (I r3 d d)) 
                (I r4 (I r2 e b) (I r4 (I r1 a e) (I r1 a e))))
axiom = let 
        a1 (I eb) e = I $ \b c -> eb e b
        a2 =  I $ \d (I dd) -> dd d d
        a3 (I abc) eb = I $ \a e -> abc a (a1 eb e)
        a4 abc = I $ \eb aeae -> runI a2 (a3 abc eb) aeae
    in I $ \abc (I dddebaeae) -> dddebaeae a2 (a4 abc)

这里我使用命名约定来跟踪类型签名：变量名称由“有效”类型变量组合（意味着它不是结果类型 - 全部为 r* 类型变量）。

我不会重复选址文章中的证明，但我想展示一些东西。在上述axiom 的定义中，我们使用了一些 let 绑定变量来构造结果。毫不奇怪，这些变量本身可以通过使用rule 和axiom 来提取。让我们看看如何：

--Equal to a4
t4 :: I r0 a (I r1 b c) -> I r2 (I r1 d b) (I r2 (I r0 a d) (I r0 a d))
t4 abc = rule axiom abc

--Equal to a3
t3 :: I r0 a (I r1 b c) -> I r1 d b -> I r0 a d
t3 abc eb = rule (t4 abc) eb

--Equal to a2
t2 :: I r a (I r a a)
t2 = rule (t3 axiom (t3 (t4 axiom) axiom)) axiom

--Equal to a1
t1 :: I r a b -> a -> I r b c
t1 ab a = rule (t3 t2 (t3 (t3 t2 t2) ab)) a

还有一点需要证明的是，我们只能使用t1 到t4 来证明所有重言式。我觉得是这样，但还没有证明。

与其他语言相比，Haskell 称呼似乎更有效且更具表现力。