Почему это расширение эта необходимо?

Ответ 1

fComp имеет тип более высокого ранга и тип вывода для типов более высокого ранга очень ограничен. Это может быть немного легче понять (но гораздо дольше!), Если мы расширим синоним типа:

fComp :: forall f a b c. Functor f => 
                (forall f1. Functor f1 => f1 b -> f1 c) ->
                (forall f2. Functor f2 => f2 a -> f2 b) ->
                (f a -> f c)

Типы более высокого ранга f и f' указаны явно в этой сигнатуре типа. Это позволяет начать вывод типа, уже зная типы f и f', и тем самым может объединить их с типом ..

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

По сути, компилятор не может создавать типы более высокого ранга для заполнения неизвестных во время вывода типа и должен полагаться на аннотации программистов, и нам нужно как имя (f, так и f') и подпись типа для получения эти аннотации.

Более простым примером для понимания может быть функция более высокого ранга id:

myId :: (forall a. a) -> (forall b. b)

Определение myId x = id x компилируется, но myId = id дает следующую ошибку:

/home/tikhon/Documents/so/eta-expansion-needed.hs:11:8:
    Couldn't match type ‘b’ with ‘forall a. a’
      ‘b’ is a rigid type variable bound by
          the type signature for myId :: (forall a. a) -> b
          at /home/tikhon/Documents/so/eta-expansion-needed.hs:11:1
    Expected type: (forall a. a) -> b
      Actual type: b -> b
    In the expression: id
    In an equation for ‘myId’: myId = id
Failed, modules loaded: none.

(Имейте в виду, что forall b. (forall a. a) -> b совпадает с (forall a. a) -> (forall b. b).)

Ответ 2

Позвольте мне переписать пример, используя нотацию System-F, в которой мы также передаем типы. Ниже \\ обозначает тип-абстракция (большая лямбда), а также абстракция словаря. Кроме того, @ означает приложение типа/словаря.

Прежде чем это сделать, напомните тип (.):

(.) :: forall a b c . (b -> a) -> (c -> b) -> (c -> a)

Здесь аннотированный код (будьте осторожны, а не для слабонервных):

fComp :: F b c -> F a b -> F a c
fComp (f :: forall f1. Functor f1 => f1 b -> f1 c)
      (f':: forall f2. Functor f2 => f2 a -> f2 b) 
   = \\ ff :: (* -> *) ->
     \\ ffD :: Functor ff ->
     ((.) @ (ff c) @ (ff b) @ (ff a))   -- instantiated composition
     (f  @ ff @ ffD)                    -- first argument of (.)
     (f' @ ff @ ffD)                    -- second argument of (.)

(Выше я притворился a, b, c - это константы типа, чтобы избежать дальнейших lambdas уровня уровня.)

Важные части:

• f и f' используются для определенных типов. То есть они применяются к аргументам уровня на уровне до того, как они будут отправлены на (.).
• (.) применяется на уровне типа к типам (ff c и т.д.), которые не являются политипами f и f'

Как вы можете видеть, исходный код далеко не тривиален. Вывод типа позволяет добавлять необходимые ямбы и приложения типа уровня. После того, как они добавлены, мы больше не можем просто выполнить контракт fComp.

В варианте с нулевой точкой, вывод типа должен делать больше, чем в точном случае. Хотя первый аргумент fComp имеет тип F a b, первый аргумент (.) должен иметь вид x -> y, который не объединяется для F a b = forall g . .... Действительно, нет способа успешно решить попытку ввода ниже:

fComp :: F b c -> F a b -> F a c
fComp 
   = \\ ff :: (* -> *) ->
     \\ ffD :: Functor ff ->
     ((.) @ ???a @ ???b @ ???c)

Выше нет no ???a,..., что может привести к желаемому типу.

Единственная возможность заключается в создании экземпляров forall -квантированных переменных, скрытых в типах F x y, но для этого нам нужна точка. Компилятор может вывести этот код для вас так, чтобы точки отображались и поэтому могут быть созданы, теоретически, но на практике этого не будет.

(Кроме того, расширение eta не всегда действует в Haskell: например, seq (undefined::()->()) 3, а seq (\x->(undefined::()->()) x) 3 возвращает 3).