Что делают эти явные foralls?

Какова цель foralls в этом коде?

class  Monad m  where
    (>>=)       :: forall a b. m a -> (a -> m b) -> m b
    (>>)        :: forall a b. m a -> m b -> m b
        -- Explicit for-alls so that we know what order to
        -- give type arguments when desugaring

(некоторые коды опущены). Это из кода для Monads.

Мой фон: я действительно не понимаю forall или когда Haskell имеет их неявно.

Кроме того, и это может быть несущественно, но GHCi позволяет мне опускать forall при указании типа >>:

Prelude> :t (>>) :: Monad m => m a -> m b -> m b
(>>) :: Monad m => m a -> m b -> m b
  :: (Monad m) => m a -> m b -> m b

(Нет ошибок).


haskell higher-rank-types forall
person Matt Fenwick    schedule 20.09.2012    source источник
comment
возможный дубликат Какова цель Rank2Types?   -  person Luis Casillas    schedule 21.09.2012
comment
@sacundim не согласен; вопрос не в том, что forall вообще делает, или что такое типы более высокого ранга. Вопрос в том, что именно forall делает в этом коде, в свете следующего за ним комментария.   -  person Matt Fenwick    schedule 21.09.2012
comment
Это пример ExplicitForall. Они не являются типами с более высоким рейтингом, и удаление фораллов не изменит тип. Я не совсем уверен, почему они являются преимуществом здесь. Комментарий предполагает, что это помогает компилятору на этапе дешугаринга.   -  person Matt S    schedule 21.09.2012
comment
Мэтт С прав, это именно те формы, которые язык неявно указывает, поэтому семантически их отсутствие или присутствие не имеет значения. ничего не меняй. Однако я понятия не имею, как компилятор может использовать их присутствие на этапе дешугаринга.   -  person Daniel Fischer    schedule 21.09.2012

Ответы (1)


arrow_upward
11
arrow_downward

Моя предыстория: я действительно не понимаю вообще или когда Haskell имеет их неявно.

Хорошо, рассмотрим тип id, a -> a. Что означает a и откуда оно взялось? Когда вы определяете значение, вы не можете просто использовать произвольные переменные, которые нигде не определены. Вам нужно определение верхнего уровня, или аргумент функции, или предложение where, и т. д. В общем, если вы используете переменную, она должна быть где-то привязана.

То же самое относится и к переменным типа, и forall — один из таких способов связать переменную типа. Везде, где вы видите переменную типа, которая не связана явно (например, class Foo a where ... связывает a внутри определения класса), она неявно связана forall.

Таким образом, тип id неявно равен forall a. a -> a. Что это значит? Почти то, что он говорит. Мы можем получить тип a -> a для всех возможных типов a, или с другой точки зрения, если вы выберете какой-либо конкретный тип, вы можете получить тип, представляющий "функции из выбранного вами типа самому себе". Последняя формулировка должна звучать как определение функции, и поэтому вы можете думать о forall как о лямбда-абстракции для типов.

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

Мы даже можем записать как foralls, так и лямбды как одно выражение. Я на мгновение злоупотреблю обозначениями и заменю forall a. на /\a => для визуальной согласованности. В этом стиле мы можем определить id = /\a => \(x::a) -> (x::a) или что-то подобное. Таким образом, такое выражение, как id True в вашем коде, в конечном итоге будет преобразовано во что-то вроде id Bool True; просто id True уже не имело бы смысла.

Точно так же, как вы можете переупорядочивать аргументы функции, вы можете переупорядочивать и аргументы типа, но только с тем (довольно очевидным) ограничением, что аргументы типа должны стоять перед любыми аргументами значения этого типа. Поскольку неявные forall всегда являются самым внешним уровнем, GHC потенциально может выбирать любой порядок, который он хочет, делая их явными. В обычных условиях это, очевидно, не имеет значения.

Я не уверен, точно что происходит в этом случае, но, основываясь на комментариях, я бы предположил, что преобразование в использование явных аргументов типа и дешугаризация нотации do в некотором смысле не осведомлены друг от друга, поэтому порядок аргументов типа указывается явно для обеспечения согласованности. В конце концов, если что-то слепо применяет два аргумента типа к выражению, очень важно, является ли тип этого выражения forall a b. m a -> m b -> m b или forall b a. m a -> m b -> m b!

person C. A. McCann    schedule 20.09.2012