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

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作为参数,然后Maybe b为调用者选择的任何b生成一个.允许返回列表中的函数的唯一值是?,Nothing和Just ?.

也就是说,当使用impredicative polymorphism时,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

但也许这个问题是你所拥有的更复杂问题的抽象,更简单的反应是行不通的？一切都应该尽可能简单,但并不简单.