Неявные параметры Haskell и полиморфная рекурсия

Question

У меня есть вопрос по главе " Неявные параметры и полиморфная рекурсия " Руководства пользователя GHC.

Код

      len1 :: [a] -> Int
len1 xs = let ?acc = 0 in len_acc1 xs

len_acc1 [] = ?acc
len_acc1 (_:xs) = let ?acc = ?acc + (1::Int) in len_acc1 xs

------------

len2 :: [a] -> Int
len2 xs = let ?acc = 0 in len_acc2 xs

len_acc2 :: (?acc :: Int) => [a] -> Int
len_acc2 [] = ?acc
len_acc2 (_:xs) = let ?acc = ?acc + (1::Int) in len_acc2 xs

В главе говорится

В первом случае len_acc1 мономорфен в своей правой части, поэтому неявный параметр ?acc не передается в рекурсивный вызов. В последнем случае, поскольку len_acc2 имеет сигнатуру типа, рекурсивный вызов выполняется для полиморфной версии, которая принимает ?acc в качестве неявного параметра.

Вопросы

• Означает ли в данном случае «мономорфный в своей правой части» тип len_acc1 :: (?acc :: Int) => [a] -> p? Почему ghci говорит len_acc1 :: (?acc::Int) => [a] -> Int?

• Почему первая функция мономорфна, а вторая нет? Если бы мое понимание было правильным, было бы наоборот.

• Или, может быть, это означает, что тип len_acc1 :: [a] -> Int, но каждый случай относится к ?accнеявное значение, поэтому я считаю, что тип должен упоминать (?acc :: Int)ограничение.

• Как этот мономорфизм подразумевает, что неявный параметр не передается в функцию?

Answer 1

В Haskell мы часто называем сигнатуры типов с переменными типа полиморфными, например полиморфную функцию подпись типа которого здесь включает переменную типа:

      id :: a -> a

Однако эта сигнатура является полиморфной не потому, что она включает переменную типа, а потому, что эта переменная определяется количественно . В Haskell сигнатуры типов неявно универсальны, поэтому приведенное выше эквивалентно:

      id :: forall a. a -> a

который на самом деле является принятым синтаксисом, если вы включите расширение. Именно эта количественная оценка делает тип полиморфным.

Когда Haskell печатает привязки без подписи типа, он использует алгоритм типизации Хиндли-Милнера для назначения типов. Этот алгоритм работает, назначая сигнатуры мономорфных типов наборам взаимозависимых привязок, а затем уточняя их, определяя отношения между ними. Этим сигнатурам разрешено содержать переменные типа (!), но они по-прежнему считаются мономорфными, поскольку переменные не определяются количественно. То есть предполагается, что переменные обозначают определенные типы, просто мы еще не выяснили их, потому что находимся в середине проверки типов.

После завершения проверки типов и присвоения «окончательных» мономорфных типов выполняется отдельный шаг обобщения. Все переменные типа, которые остаются в мономорфных типах, которые не были определены как фиксированные типы, такие как а также , обобщаются с помощью универсальной квантификации. На этом этапе определяются окончательные полиморфные типы привязок. Ограничения являются частью процесса количественной оценки и поэтому применяются только к сигнатурам типов на этапе обобщения, когда мы переходим от мономорфных к полиморфным типам.

Документация ссылается на тот факт, что при выводе типа алгоритм присваивает ему мономорфный тип, в конечном итоге окончательный мономорфный тип со свободной (т.е. неколичественной) переменной типа. Хотя средство проверки типов заметит, что требуется ограничение, оно не делает эту часть предполагаемого типа . В частности, тип, назначенный рекурсивному вызову, является мономорфным типом. без ограничений. Только после того, как этот окончательный мономорфный тип для был определен, он обобщается посредством квантификации более и добавление ограничений для получения окончательной подписи верхнего уровня.

Напротив, когда предоставляется полиморфная подпись верхнего уровня:

      len_acc2 :: forall a. (?acc :: Int) => [a] -> Int

привязка является полиморфной (вместе со связанным с ней ограничением) везде, где она используется, в частности, в рекурсивном вызове.

Результат в том, что рекурсивно вызывается мономорфно, без словаря ограничений, предоставляющего (новое) значение параметра, в то время как вызывается полиморфно, со словарем ограничений для нового ценность. Я считаю, что эта ситуация уникальна для неявных параметров. В противном случае вы бы не столкнулись с ситуацией, когда рекурсивный вызов может быть типизирован как мономорфно, так и полиморфно таким образом, что код будет вести себя по-разному при двух типизациях.

Скорее всего, вы столкнетесь с такой ситуацией, как следующая, когда требуется «очевидная» подпись типа, потому что мономорфный тип не может быть выведен:

      data Binary a = Leaf a | Pair (Binary (a,a)) deriving (Show)

-- following type signature is required... 
-- toList :: Binary a -> [a]
toList (Leaf x) = [x]
toList (Pair b) = concatMap (\(x,y) -> [x,y]) (toList b)

main = print $ toList (Pair (Pair (Leaf ((1,2),(3,4)))))

Answer 2

Я могу ответить на вопрос лишь частично.

Почему ghci говорит len_acc1 :: (?acc::Int) => [a] -> Int?

Это потому, что первое предложение возвращает ?accи можно предположить, что из ?acc + (1::Int)во втором пункте.

"в... правой стороне"

означает часть после =, который имеет тип Intкак и выше, который является мономорфным. len_acc1 :: (?acc :: Int) => [a] -> pбыл бы полиморфным .

Или, может быть, это означает, что тип len_acc1 :: [a] -> Int, но каждый случай относится к неявному значению ?acc, поэтому я считаю, что тип должен упоминать ограничение (?acc :: Int).

Вот что он, кажется, говорит мне; что, по крайней мере, временно он рассматривается как имеющий этот тип. Но тогда я не понимаю, почему он вообще компилируется.

Я пытался прочитать статью, где были определены неявные параметры, но не нашел ответа.