将域建模为 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-notation 表示此模型中的一些算法，例如（出于美学原因假设相应的 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 添加更多的构造函数来表示纯注入值和 monadic 绑定：

  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 实例，以避免丑陋的嵌套 OpBinds。

这是处理此类类型的正确方法，还是我的设计错得离谱，这就是它的标志？

Answer 1

这种使用 do-notation 来构建稍后将被解释的语法树的风格是由 free monad 建模的。（实际上，我将演示所谓的 freer 或 operational monad，因为它更接近您目前所拥有的。）

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

的列表

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

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

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

A Program 是一种指令列表：它是一个空程序，其中 return 是单个值，或者它是一个指令后跟指令列表。 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，从而打破 monad 关联律。

您可以使 Program 成为 monad。

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

>>= 基本上执行列表连接 - 它走到列表的末尾（通过在 Step 延续下组合对自身的递归调用）并移植到新的尾部。这是有道理的——它对应于 >>=.

的直观 "run this program, then run that program" 语义

注意到 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 是一个相当通用的命令式语言建模工具。

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

Modeling a domain as a GADT type and providing do-sugar for it

haskell

gadt