类型级别的验证

Question

假设我想构造满足某些不变量的子类型，而无需借助 LiquidHaskell 等外部工具(理想情况下，即使没有类型类，我也想做到这一点)。最优雅的方法是什么？到目前为止，我尝试了以下方法:

class Validated a where
  type Underlying a
  validate :: Underlying a -> Bool
  construct :: Underlying a -> a
  use :: a -> Underlying a

makeValidated :: Validated a => Underlying a -> Maybe a
makeValidated u = if validate u 
                    then Just (construct u)
                    else Nothing


newtype Name = Name String
instance Validated Name where
  type Underlying Name = String
  validate str = and  [ isUppercase (str !! 0 )
                      , all isLetter str ]
  construct = Name
  use (Name str) = str

我假设如果我不从模块中导出“Name”构造函数，我将有一个可行的解决方案，因为构造该类型元素的唯一方法是通过 makeValidated 函数。

但是编译器会这样提示:

Could not deduce (Underlying a0 ~ Underlying a)
from the context (Validated a)
  bound by the type signature for
             makeValidated :: Validated a => Underlying a -> Maybe a
  at validated.hs:11:18-55
NB: `Underlying' is a type function, and may not be injective
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the first argument of `validate', namely `u'
In the expression: validate u
In the expression:
  if validate u then Just (construct u) else Nothing

如何修复它？

Answer 1

底层是一个类型函数，它可能不是单射的。即:

instance Validate T1 where
   type Underlying T1 = Int
   validate = ... -- code A

instance Validate T2 where
   type Underlying T2 = Int
   validate = ... -- code B

现在考虑

validate (42 :: Int)

这应该做什么？它应该调用代码 A 还是 B ？由于底层 T1 = 底层 T2 = Int，因此无法判断。

不可能明确地调用validate。为了避免这种情况，一个可能的解决方法是向您的验证函数添加一个“代理”参数:

data Proxy a = Proxy

class Validate a where
    validate :: Proxy a -> Underlying a -> Bool

现在您可以使用:

validate Proxy (42 :: Int)               -- still ambiguous!
validate (Proxy :: Proxy T1) (42 :: Int) -- Now OK!
validate (Proxy :: Proxy T2) (42 :: Int) -- Now OK!