使用 monad 隐式检查细化类型的良构性

【问题标题】：Using a monad to implicitly check refinement type well-formedness使用 monad 隐式检查细化类型的良构性
【发布时间】：2016-07-25 16:16:55
【问题描述】：

在实现细化类型系统时，我需要进行检查以确保类型格式正确。例如，不应出现Num[100,0] 之类的类型，其中Num[lb,ub] 是大于lb 且小于ub 的数字类型。然后我写道：

-- FORMATION RULES

class RefTy t 
  where tyOK :: t -> Bool

instance RefTy Ty
  where tyOK (NumTy (n1, n2)) = n1 <= n2
        tyOK (CatTy cs) = isSet cs

{-
data WellFormed t = Valid t
                  | Invalid

instance Monad WellFormed
  where 
    (>>=) :: RefTy a => WellFormed a -> (a -> WellFormed b) -> WellFormed b
    Valid t >>= f 
            | tyOK t = f t
            | otherwise = Invalid
    Invalid >>= _ = Invalid
-}

这让我陷入了“restricted Monad”的已知问题。建议的答案是让Wellformed monad 通用但限制功能。但是，这将回到在任何地方添加格式正确的检查。有没有更好的出行方式？

【问题讨论】：

你如何定义return/pure？

标签： haskell dependent-type refinement-type

【解决方案1】：

在你的情况下，我认为你实际上并不想要一个单子，只是伴随do 符号的糖。例如，您是否想过您对Applicative 的定义会是什么样子？当你试图通过这种方式作弊时，事情会变得一团糟。

相反，如果你想使用do-notation，我建议你使用

{-# LANGUAGE RebindableSyntax #-}

它允许您重新定义用于脱糖 do 块的 (>>=) 和 return。然后，您可以编写如下内容：

myBind :: RefTy t1 => WellFormed t1 -> (t1 -> WellFormed t2) -> WellFormed t2
myBind Invalid _ = Invalid
myBind (Valid t) f | tyOK t = f t
                   | otherwise Invalid 

myReturn :: WellFormed t
myReturn t = Valid t

我不确定我是否同意这些定义，但不管你是否能写出类似的东西

do
  ...
  where (>>=) = myBind
        return = myReturn

【讨论】：