排名较高的和不可预测的类型

Question

我想实现以下stripPrefixBy函数：

-- psuedo code signature
stripPrefixBy :: forall a. [forall b. a -> Maybe b] -> [a] -> Maybe [a]
stripPrefixBy [] xs = Just xs
stripPrefixBy _ [] = Nothing
stripPrefixBy (p:ps) (x:xs) = case p x of
  Just _ -> stripPrefixBy ps xs
  Nothing -> Nothing

res :: Maybe String
res = stripPrefixBy [const (Just 0), Just] "abc"

wantThisToBeTrue :: Bool
wantThisToBeTrue = case res of
  Just "c" -> True
  _ -> False

我尝试过使用ImpredicativeTypes和RankNTypes，但没有成功。如何使用我想要的类型来实现stripPrefixBy？

Answer 1

签名的问题是，传递给stripPrefixBy的列表被声明为一个函数列表，这些函数以某个a为参数，然后为调用者选择的任何b生成一个Maybe b。列表中的函数只能返回⊥、Nothing和Just ⊥。

也就是说，当使用非谓词多态性时，forall的含义与存在量化类型不同:在这里，forall应用于构造函数的类型，即

data MyType = forall a. Foo a
Foo :: forall a. a -> MyType

但在这里，它说的是函数必须是forall b. a -> Maybe b类型。

下面是一个使用存在类型的更正后的示例：

{-# LANGUAGE ExistentialQuantification #-}

data Pred a = forall b. Pred (a -> Maybe b)

stripPrefixBy :: [Pred a] -> [a] -> Maybe [a]
stripPrefixBy [] xs = Just xs
stripPrefixBy _ [] = Nothing
stripPrefixBy (Pred p:ps) (x:xs) = case p x of
  Just _ -> stripPrefixBy ps xs
  Nothing -> Nothing

res :: Maybe String
res = stripPrefixBy [Pred $ const (Just 0), Pred Just] "abc"

wantThisToBeTrue :: Bool
wantThisToBeTrue = case res of
  Just "c" -> True
  _ -> False

我相信UHC支持直接表达您想要的类型，如下所示

stripPrefixBy :: [exists b. a -> Maybe b] -> [a] -> Maybe [a]

Answer 2

另一种回答是，“为什么您希望它具有这种类型？”如果您愿意将函数列表(stripPrefixBy的第一个参数)都约束为具有相同的结果类型，则可以使用例如

res :: Maybe String
res = stripPrefixBy [const (Just undefined), Just] "abc"

然后为stripPrefixBy提供以下Haskell98类型：

stripPrefixBy :: [a -> Maybe b] -> [a] -> Maybe [a]

等价地，您可以观察到第一个参数中的函数的结果不能使用(没有其他参数提到类型"b")，所以您最好有一个谓词列表：

stripPrefixBy :: [a -> Bool] -> [a] -> Maybe [a]
stripPrefixBy [] xs = Just xs
stripPrefixBy _ [] = Nothing
stripPrefixBy (p:ps) (x:xs) = case p x of
  True  -> stripPrefixBy ps xs
  False -> Nothing

res :: Maybe String
res = stripPrefixBy (map (isJust.) [const (Just undefined), Just]) "abc"

isJust :: Maybe a -> Bool
isJust (Just _) = True
isJust Nothing = False

但也许这个问题是一个更复杂问题的抽象，而更简单的回答将不起作用？每件事都应该尽可能简单，但不能简单。