类型级别的验证

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

validate 函数，如所写，在当前的 GHC 中不可用。查看其类型签名：

validate :: Validated a => Underlying a -> Bool

您可能会合理地认为，给定类型 Underlying a 的值，可以找出要使用的 Validated 实例，即 a 实例。但这是一个错误：由于 Underlying 不是单射的，因此 Underlying b ~ Underlying c 可能存在类型 b 和 c；因此 b 和 c 都不是要使用哪个实例的规范选择。也就是说，在 F (Underlying a) ~ a 始终为真的类型上没有好的映射 F！

另一种方法是使用数据族而不是类型族。

class Validated a where
    data Underlying a
    validate :: Underlying a -> Bool

instance Validated Name where
    data Underlying Name = Underlying String
    validate (Underlying name) = ...

Answer 2

Underlying 是类型函数，可能不是单射的。即：

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？自Underlying T1 = Underlying T2 = Int以来，无法判断。

明确调用validate是不可能的。为避免这种情况，一个可能的解决方法是向您的验证函数添加一个 "proxy" 参数：

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!

类型级别的验证

Validation at type level

validation

haskell

type-families