使用monad隐式检查优化类型的格式是否正确 [英] Using a monad to implicitly check refinement type well-formedness

问题描述

在实施优化类型系统时，我需要进行检查以确保类型格式正确.例如，不应出现类似 Num [100,0] 的类型，其中 Num [lb，ub] 是大于 lb ，并且小于 ub .然后我写了:

While implementing a refinement type system, I need to put in checks to make sure the types are well-formed. For example, a type like Num[100,0] shouldn't happen, where Num[lb,ub] is the type of numbers larger than lb and smaller than ub. I then wrote:

-- 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
-}

这让我陷入了一个已知问题"受限的Monad ".建议的答案是使 Wellformed monad具有通用性，但限制功能.但是，这可以追溯到在各处添加格式正确的支票.有更好的出行方式吗?

Which got me into the known problem of "restricted Monad". The suggested answer is to have the Wellformed monad to be general but restrict the functions. However that would go back to adding the well-formed check everywhere. Is there a better way to get around?

推荐答案

在您的情况下，我认为您实际上并不想要单子，只是 do 表示法附带的糖.例如，您是否考虑过 Applicative 的定义会是什么样?当您尝试通过这种方式欺骗自己时，事情变得很快.

In your case, I don't think you actually want a monad, just the sugar that accompanies do notation. For example, have you thought about what your definition of Applicative will look like? Things get messy fast when you try to cheat your way through this.

相反，如果要使用 do 表示法，建议您使用

Instead, if you want to use the do-notation, I suggest you use

{-# LANGUAGE RebindableSyntax #-}

允许您重新定义用于取消执行 do 块的(>> =)和 return .然后，您可以编写如下内容:

which allows you to redefine, amongst other thing, the (>>=) and return used in desugaring a do block. You could then write something like:

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

我不确定我是否同意这些定义，但是无论您随后将能够写出类似的内容

I'm not sure I agree with those definitions, but regardless you would then be able to write something like

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

这篇关于使用monad隐式检查优化类型的格式是否正确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！