Почему я получаю эту ошибку, когда пытаюсь написать определение типа локальной функции в Haskell?

Это мое определение функции any'

any' :: (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b

Я получаю эту ошибку при загрузке в объятиях:

ERROR "folds.hs":65 - Inferred type is not general enough
*** Expression    : step
*** Expected type : Bool -> a -> Bool
*** Inferred type : Bool -> _7 -> Bool

... и это в ghci:

folds.hs:65:27:
    Couldn't match expected type `t' with actual type `t1'
      `t' is a rigid type variable bound by
          the type signature for any' :: (t -> Bool) -> [t] -> Bool
          at folds.hs:62:9
      `t1' is a rigid type variable bound by
           the type signature for step :: Bool -> t1 -> Bool at folds.hs:64:22
    In the first argument of `f', namely `x'
    In the expression: f x
    In a stmt of a pattern guard for
                   an equation for `step':
      f x

Когда я удаляю определение типа шага, оно работает нормально, поэтому мой вопрос... Есть ли способ правильно написать это определение типа, или я имею дело с одной из тех ситуаций, когда локальные функции не могут быть явно типизированы?


person matiascelasco    schedule 08.02.2014    source источник
comment
Вам нужно расширение переменных типа с областью действия, иначе компилятор увидит вторую переменную t как другую переменную нового полиморфного типа, а не ту же t, что и в объявлении основного типа.   -  person not my job    schedule 08.02.2014
comment
Кстати, почему foldl, а не foldr?   -  person Sassa NF    schedule 09.02.2014
comment
вы правы Sassa NF, foldr лучше, так как позволяет делать что угодно даже (повторить 2)   -  person matiascelasco    schedule 09.02.2014


Ответы (2)


t в подписи

where step :: Bool -> t -> Bool

не то же самое t, что и в подписи any'. Вместо этого он интерпретируется как переменная нового типа, которая является локальной для сигнатуры step.

Другими словами, ваш код фактически эквивалентен

any' :: (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
   where step :: Bool -> a -> Bool          -- t renamed to a
         step b x | f x       = True
                  | otherwise = b

и компилятор затем жалуется, потому что step утверждает в своей подписи, что он применим к любому типу a, в то время как f требует t.

Возможным решением является удаление подписи step. В этом случае компилятор сам выведет правильный тип. Это не совсем приятно с точки зрения программиста, так как теперь компилятор не будет проверять, что подпись step действительно та, которую задумал программист.

Еще одно исправление, предложенное в комментариях, заключается в включении расширения Haskell, которое позволяет нам писать свой тип.

{-# LANGUAGE ScopedTypeVariables #-}
import Data.List

any' :: forall t. (t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b

Здесь явный квантификатор forall t сообщает компилятору, что t, встречающееся внутри определения any', на самом деле является тем же самым t, а не переменной нового типа.

person chi    schedule 08.02.2014
comment
Спасибо! отличный ответ. Знаете ли вы, есть ли недостатки в использовании этого расширения? Я предполагаю, что есть, иначе он был бы включен по умолчанию. - person matiascelasco; 09.02.2014
comment
@matiascelasco не недостаток, а тот факт, что компилятор должен его поддерживать. GHC делает. - person chi; 09.02.2014
comment
@MathematicalOrchid Да, требуется расширение forall, иначе t не будет включено в область действия подписи step. - person chi; 10.02.2014
comment
По-видимому, я вообще не понимаю, как работают переменные типа с областью действия... Я думал, что это просто означает, что все переменные типа остаются в области видимости. - person MathematicalOrchid; 10.02.2014

Вам нужно расширение переменных типа с областью действия, иначе компилятор увидит вторую переменную t как другую переменную нового полиморфного типа, а не ту же t, что и в объявлении основного типа.

Подсказка, что это происходит, содержится в сообщении Couldn't match expected type 't' with actual type 't1'. Ясно, что ghci переименовал второй t в t1, потому что он не считает их одинаковыми.

Вы можете использовать ScopedTypeVariables и явный forall, чтобы ввести t в область действия внутренней функции.

{-# LANGUAGE ScopedTypeVariables #-}

any' :: forall t.(t -> Bool) -> [t] -> Bool
any' f = foldl' step False
       where step :: Bool -> t -> Bool
             step b x | f x       = True
                      | otherwise = b
person not my job    schedule 08.02.2014