Более высокие и недискриминационные типы

Я хочу реализовать следующую функцию 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 с типом, который я хочу иметь?

Ответы

Ответ 1

Проблема с вашей сигнатурой заключается в том, что список, переданный в stripPrefixBy, объявляется как список функций, которые принимают некий а как аргумент, а затем создают Maybe b для любого 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]

Ответ 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

Но может быть, этот вопрос является абстракцией более сложной проблемы, которую вы имеете, и более простой ответ не будет работать? Все должно быть как можно проще, но не проще.