haskell - 将域建模为 GADT 类型并为其提供 do-sugar

Question

假设我们想要构建一个代表典型操作的类型，比如说，一个无锁算法:

newtype IntPtr = IntPtr { ptr :: Int } deriving (Eq, Ord, Show)

data Op r where 
  OpRead :: IntPtr -> Op Int
  OpWrite :: IntPtr -> Int -> Op ()

  OpCAS :: IntPtr -> Int -> Int -> Op Bool

理想情况下，我们希望使用方便的 do 来表示此模型中的一些算法。 -符号，例如(假设对应 read = OpRead 和 cas = OpCAS 出于美学原因)以下 Wikipedia example 的几乎字面翻译:

import Prelude hiding (read)
import Control.Monad.Loops

add :: IntPtr -> Int -> Op Int
add p a = snd <$> do
  iterateUntil fst $ do
    value <- read p
    success <- cas p value (value + a)
    pure (success, value + a)

我们怎样才能做到这一点？让我们向 Op 添加更多构造函数表示纯注入(inject)值和一元绑定(bind):

  OpPure :: a -> Op a
  OpBind :: Op a -> (a -> Op b) -> Op b

所以让我们试着写一个 Functor实例。 OpPure和 OpBind很容易，例如:

instance Functor Op where
  fmap f (OpPure x) = OpPure (f x)

但是指定 GADT 类型的构造函数开始闻起来很糟糕:

  fmap f (OpRead ptr) = do
    val <- OpRead ptr
    pure $ f val

在这里，我们假设我们将编写 Monad无论如何，稍后实例以避免丑陋的嵌套 OpBind s。

这是处理此类类型的正确方法，还是我的设计非常错误，这是它的标志？

Answer 1

这种使用方式do用于构建稍后将被解释的语法树的 -notation 由 free monad 建模。 (我实际上将展示所谓的更自由或可操作的 monad，因为它更接近您目前所拥有的。)

您的原创 Op数据类型 - 没有 OpPure和 OpBind - 表示一组原子类型指令(即 read 、 write 和 cas )。在命令式语言中，程序基本上是一个指令列表，所以让我们设计一个表示 Op 列表的数据类型。 s。

一种想法可能是使用实际列表，即 type Program r = [Op r] .显然这不会做，因为它将程序中的每条指令都限制为具有相同的返回类型，这不会成为一种非常有用的编程语言。

关键的见解是，在解释性命令式语言的任何合理操作语义中，控制流不会继续通过指令，直到解释器计算出该指令的返回值。也就是说，程序的第 n 条指令通常取决于指令 0 到 n-1 的结果。我们可以使用延续传递风格对此进行建模。

data Program a where
    Return :: a -> Program a
    Step :: Op r -> (r -> Program a) -> Program a

一个 Program是一种指令列表:它要么是返回单个值的空程序，要么是单个指令后跟指令列表。 Step里面的函数构造函数意味着运行 Program 的解释器必须想出一个 r在它可以恢复解释程序的其余部分之前的值。所以顺序是由类型来保证的。

构建你的原子程序 read , write和 cas ，你需要把它们放在一个单例列表中。这涉及将相关指令放入 Step构造函数，并传递一个无操作延续。

lift :: Op a -> Program a
lift i = Step i Return

read ptr = lift (OpRead ptr)
write ptr val = lift (OpWrite ptr val)
cas ptr cmp val = lift (OpCas ptr cmp val)

Program不同于您的调整 Op在每个 Step只有一个指令。 OpBind的左参数可能是 Op 的整个树s。这将允许您区分不同关联的 >>= s，打破单子(monad)结合律。

您可以制作 Program一个单子(monad)。

instance Monad Program where
    return = Return
    Return x >>= f = f x
    Step i k >>= f = Step i ((>>= f) . k)

>>=基本上执行列表连接 - 它走到列表的末尾(通过在 Step 延续下组合对自身的递归调用)并移植到新的尾部。这是有道理的——它对应于 >>= 的直观“运行这个程序，然后运行那个程序”语义。 .

注意到 Program的 Monad实例不依赖于 Op ，一个明显的概括是参数化指令的类型并使 Program进入任何旧指令集的列表。

data Program i a where
    Return :: a -> Program i a
    Step :: i r -> (r -> Program i a) -> Program a

instance Monad (Program i) where
    -- implementation is exactly the same

所以 Program i是一个免费的单子(monad)，无论如何 i是。这个版本的 Program是一种用于对命令式语言进行建模的相当通用的工具。