将域建模为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出于美学原因)维基百科示例的以下几乎字面翻译:

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实例以避免丑陋的嵌套OpBind.

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

Answer 1

这种使用do注释来构建一个稍后将被解释的语法树的样式由免费的monad建模.(我实际上将演示所谓的更自由或操作的 monad,因为它更接近你到目前为止所拥有的.)

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

一个想法可能是使用实际列表,即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

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,打破monad关联性法则.

你可以制作Program一个单子.

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是一个免费的单子,不管是什么i是.此版本Program是一种用于建模命令式语言的通用工具.