Что такое ограничение мономорфизма?

Я озадачен тем, как компилятор haskell иногда выводит типы, которые менее полиморфны, чем я ожидал, например, при использовании бессмысленных определений.

Похоже, проблема заключается в "ограничении мономорфизма", которое включено по умолчанию в более старых версиях компилятора.

Рассмотрим следующую программу на haskell:

{-# LANGUAGE MonomorphismRestriction #-}

import Data.List(sortBy)

plus = (+)
plus' x = (+ x)

sort = sortBy compare

main = do
  print $ plus' 1.0 2.0
  print $ plus 1.0 2.0
  print $ sort [3, 1, 2]

Если я скомпилирую это с ghc Я не получаю ошибок и вывод исполняемого файла:

3.0
3.0
[1,2,3]

Если я изменю main тело к:

main = do
  print $ plus' 1.0 2.0
  print $ plus (1 :: Int) 2
  print $ sort [3, 1, 2]

Я не получаю ошибок времени компиляции и вывод становится:

3.0
3
[1,2,3]

как и ожидалось. Однако, если я попытаюсь изменить его на:

main = do
  print $ plus' 1.0 2.0
  print $ plus (1 :: Int) 2
  print $ plus 1.0 2.0
  print $ sort [3, 1, 2]

Я получаю ошибку типа:

test.hs:13:16:
    No instance for (Fractional Int) arising from the literal ‘1.0’
    In the first argument of ‘plus’, namely ‘1.0’
    In the second argument of ‘($)’, namely ‘plus 1.0 2.0’
    In a stmt of a 'do' block: print $ plus 1.0 2.0

То же самое происходит при попытке позвонить sort дважды с разными типами:

main = do
  print $ plus' 1.0 2.0
  print $ plus 1.0 2.0
  print $ sort [3, 1, 2]
  print $ sort "cba"

выдает следующую ошибку:

test.hs:14:17:
    No instance for (Num Char) arising from the literal ‘3’
    In the expression: 3
    In the first argument of ‘sort’, namely ‘[3, 1, 2]’
    In the second argument of ‘($)’, namely ‘sort [3, 1, 2]’
  • Почему ghc вдруг подумать, что plus не полиморфен и требует Int аргумент? Единственная ссылка на Int находится в приложении plusкак это может иметь значение, когда определение явно полиморфное?
  • Почему ghc вдруг подумать, что sort требует Num Char пример?

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

{-# LANGUAGE MonomorphismRestriction #-}

module TestMono where

import Data.List(sortBy)

plus = (+)
plus' x = (+ x)

sort = sortBy compare

Я получаю следующую ошибку при компиляции:

TestMono.hs:10:15:
    No instance for (Ord a0) arising from a use of ‘compare’
    The type variable ‘a0’ is ambiguous
    Relevant bindings include
      sort :: [a0] -> [a0] (bound at TestMono.hs:10:1)
    Note: there are several potential instances:
      instance Integral a => Ord (GHC.Real.Ratio a)
        -- Defined in ‘GHC.Real’
      instance Ord () -- Defined in ‘GHC.Classes’
      instance (Ord a, Ord b) => Ord (a, b) -- Defined in ‘GHC.Classes’
      ...plus 23 others
    In the first argument of ‘sortBy’, namely ‘compare’
    In the expression: sortBy compare
    In an equation for ‘sort’: sort = sortBy compare
  • Почему нет ghc в состоянии использовать полиморфный тип Ord a => [a] -> [a] за sort?
  • И почему ghc лечить plus а также plus' по-другому? plus должен иметь полиморфный тип Num a => a -> a -> a и я действительно не вижу, как это отличается от типа sort и пока только sort выдает ошибку.

И последнее: если я прокомментирую определение sort файл компилируется. Однако, если я попытаюсь загрузить его в ghci и проверьте типы, которые я получаю:

*TestMono> :t plus
plus :: Integer -> Integer -> Integer
*TestMono> :t plus'
plus' :: Num a => a -> a -> a

Почему не тип для plus полиморфный?

Это канонический вопрос об ограничении мономорфизма в Хаскеле, как обсуждалось в мета-вопросе.

Источник

1 ответ

Решение

Что такое ограничение мономорфизма?

Ограничение мономорфизма, как заявлено в вики Haskell:

нелогичное правило в выводе типа Haskell. Если вы забыли предоставить сигнатуру типа, иногда это правило будет заполнять переменные свободного типа определенными типами, используя правила "тип по умолчанию".

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

Как мне это исправить?

Прежде всего вы всегда можете явно указать сигнатуру типа, и это позволит избежать срабатывания ограничения:

plus :: Num a => a -> a -> a
plus = (+)    -- Okay!

-- Runs as:
Prelude> plus 1.0 1
2.0

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

plus x y = x + y

Выключить его

Можно просто отключить ограничение, чтобы вам не пришлось ничего делать со своим кодом, чтобы это исправить. Поведение контролируется двумя расширениями: MonomorphismRestriction включит его (по умолчанию), пока NoMonomorphismRestriction отключит это.

Вы можете поместить следующую строку в самый верх вашего файла:

{-# LANGUAGE NoMonomorphismRestriction #-}

Если вы используете GHCi, вы можете включить расширение, используя :set команда:

Prelude> :set -XNoMonomorphismRestriction

Вы также можете сказать ghc чтобы включить расширение из командной строки:

ghc ... -XNoMonomorphismRestriction

Примечание: вы действительно должны предпочесть первый вариант, а не выбирать расширение через параметры командной строки.

Обратитесь к странице GHC для объяснения этого и других расширений.

Полное объяснение

Ниже я постараюсь обобщить все, что вам нужно знать, чтобы понять, что такое ограничение мономорфизма, почему оно было введено и как оно ведет себя.

Пример

Примите следующее тривиальное определение:

plus = (+)

можно подумать, что сможет заменить каждое вхождение + с plus, В частности с (+) :: Num a => a -> a -> a вы ожидаете также иметь plus :: Num a => a -> a -> a,

К сожалению, это не случай. Например, в GHCi мы попробуем следующее:

Prelude> let plus = (+)
Prelude> plus 1.0 1

Мы получаем следующий вывод:

<interactive>:4:6:
    No instance for (Fractional Integer) arising from the literal ‘1.0’
    In the first argument of ‘plus’, namely ‘1.0’
    In the expression: plus 1.0 1
    In an equation for ‘it’: it = plus 1.0 1

Вам может понадобиться :set -XMonomorphismRestriction в более новых версиях GHCi.

И на самом деле мы можем видеть, что тип plus это не то, что мы ожидали:

Prelude> :t plus
plus :: Integer -> Integer -> Integer

Случилось так, что компилятор увидел, что plus имел тип Num a => a -> a -> a полиморфный тип. Более того, бывает так, что приведенное выше определение подпадает под правила, которые я объясню позже, и поэтому он решил сделать тип мономорфным, установив по умолчанию переменную типа a, По умолчанию Integer как мы можем видеть.

Обратите внимание, что если вы попытаетесь скомпилировать приведенный выше код, используя ghc вы не получите никаких ошибок. Это связано с тем, как ghci обрабатывает (и должен обрабатывать) интерактивные определения. В основном каждое заявление, введенное в ghci должен быть полностью проверен на тип, прежде чем будет рассмотрено следующее; другими словами, это как если бы каждое утверждение было в отдельном модуле. Позже я объясню, почему это так.

Какой-то другой пример

Рассмотрим следующие определения:

f1 x = show x

f2 = \x -> show x

f3 :: (Show a) => a -> String
f3 = \x -> show x

f4 = show

f5 :: (Show a) => a -> String
f5 = show

Мы ожидаем, что все эти функции будут вести себя одинаково и иметь одинаковый тип, то есть тип show: Show a => a -> String,

Тем не менее, при составлении приведенных выше определений мы получаем следующие ошибки:

test.hs:3:12:
    No instance for (Show a1) arising from a use of ‘show’
    The type variable ‘a1’ is ambiguous
    Relevant bindings include
      x :: a1 (bound at blah.hs:3:7)
      f2 :: a1 -> String (bound at blah.hs:3:1)
    Note: there are several potential instances:
      instance Show Double -- Defined in ‘GHC.Float’
      instance Show Float -- Defined in ‘GHC.Float’
      instance (Integral a, Show a) => Show (GHC.Real.Ratio a)
        -- Defined in ‘GHC.Real’
      ...plus 24 others
    In the expression: show x
    In the expression: \ x -> show x
    In an equation for ‘f2’: f2 = \ x -> show x

test.hs:8:6:
    No instance for (Show a0) arising from a use of ‘show’
    The type variable ‘a0’ is ambiguous
    Relevant bindings include f4 :: a0 -> String (bound at blah.hs:8:1)
    Note: there are several potential instances:
      instance Show Double -- Defined in ‘GHC.Float’
      instance Show Float -- Defined in ‘GHC.Float’
      instance (Integral a, Show a) => Show (GHC.Real.Ratio a)
        -- Defined in ‘GHC.Real’
      ...plus 24 others
    In the expression: show
    In an equation for ‘f4’: f4 = show

Так f2 а также f4 не компилировать Более того, при попытке определить эти функции в GHCi мы не получаем никаких ошибок, но тип для f2 а также f4 является () -> String!

Ограничение мономорфизма - это то, что делает f2 а также f4 требуют мономорфного типа, и различное поведение между ghc а также ghci из-за различных правил по умолчанию.

Когда это происходит?

В Haskell, как определено в отчете, есть два разных типа привязок. Функциональные привязки и привязки к шаблону. Привязка функции - это не что иное, как определение функции:

f x = x + 1

Обратите внимание, что их синтаксис:

<identifier> arg1 arg2 ... argn = expr

Модуло охранников и where деклараций. Но они на самом деле не имеют значения.

где должен быть хотя бы один аргумент.

Привязка к шаблону - это объявление формы:

<pattern> = expr

Опять по модулю охранников.

Обратите внимание, что переменные являются шаблонами, поэтому связывание:

plus = (+)

это шаблон привязки. Это обязательный шаблон plus (переменная) в выражении (+),

Когда привязка шаблона состоит только из имени переменной, это называется простой привязкой шаблона.

Ограничение мономорфизма применяется к простым привязкам к шаблону!

Ну, формально мы должны сказать, что:

Группа объявлений - это минимальный набор взаимозависимых привязок.

Раздел 4.5.1 отчета.

А затем (раздел 4.5.5 отчета):

данная группа объявлений является неограниченной, если и только если:

  1. каждая переменная в группе связана функцией привязки (например, f x = x) или простая привязка шаблона (например, plus = (+); Раздел 4.4.3.2) и

  2. явная сигнатура типа дается для каждой переменной в группе, которая связана простой привязкой к шаблону. (например plus :: Num a => a -> a -> a; plus = (+)).

Примеры, добавленные мной.

Таким образом, группа с ограниченным объявлением - это группа, в которой либо существуют непростые привязки к шаблону (например, (x:xs) = f something или же (f, g) = ((+), (-))) или существует какая-то простая привязка шаблона без сигнатуры типа (как в plus = (+)).

Ограничение мономорфизма влияет на ограниченные группы объявлений.

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

Что оно делает?

Ограничение мономорфизма описывается двумя правилами в разделе 4.5.5 отчета.

Первое правило

Обычное ограничение Хиндли-Милнера на полиморфизм состоит в том, что только переменные типа, которые не встречаются свободно в среде, могут быть обобщены. Кроме того, переменные ограниченного типа в группе ограниченного объявления не могут быть обобщены на этапе обобщения для этой группы. (Напомним, что переменная типа ограничена, если она должна принадлежать некоторому классу типа; см. Раздел 4.5.2.)

Выделенная часть - это то, что вводит ограничение мономорфизма. Это говорит о том, что если тип полиморфный (то есть содержит некоторую переменную типа) и эта переменная типа ограничена (то есть имеет ограничение класса: например, тип Num a => a -> a -> a полиморфен, потому что содержит a а также противоречил, потому что a имеет ограничение Num над этим.) тогда это не может быть обобщено.

Проще говоря, не обобщение означает, что использование функции plus может изменить свой тип.

Если у вас были определения:

plus = (+)

x :: Integer
x = plus 1 2

y :: Double
y = plus 1.0 2

тогда вы получите ошибку типа. Потому что когда компилятор видит это plus называется над Integer в декларации x это унифицирует переменную типа a с Integer и, следовательно, тип plus будет выглядеть так:

Integer -> Integer -> Integer

но потом, когда он наберет, проверь определение y он увидит что plus применяется к Double аргумент, и типы не совпадают.

Обратите внимание, что вы все еще можете использовать plus без получения ошибки:

plus = (+)
x = plus 1.0 2

В этом случае тип plus первый вывод, чтобы быть Num a => a -> a -> a но затем его использование в определении x, где 1.0 требует Fractional ограничение, изменит его на Fractional a => a -> a -> a,

обоснование

В отчете говорится:

Правило 1 требуется по двум причинам, обе из которых довольно тонки.

  • Правило 1 предотвращает неожиданное повторение вычислений. Например, genericLength это стандартная функция (в библиотеке Data.List) тип которого определяется

    genericLength :: Num a => [b] -> a

    Теперь рассмотрим следующее выражение:

    let len = genericLength xs
in (len, len)

    Это выглядит, как если бы len должен вычисляться только один раз, но без правила 1 он может вычисляться дважды, по одному при каждой из двух разных перегрузок. Если программист действительно хочет, чтобы вычисление повторялось, можно добавить явную сигнатуру типа:

    let len :: Num a => a
    len = genericLength xs
in (len, len)

На данный момент, пример из вики, на мой взгляд, более понятен. Рассмотрим функцию:

f xs = (len, len)
  where
    len = genericLength xs

Если len был полиморфный тип f было бы:

f :: Num a, Num b => [c] -> (a, b)

Таким образом, два элемента кортежа (len, len) на самом деле могут быть разные значения! Но это означает, что вычисления сделаны genericLength необходимо повторить, чтобы получить два разных значения.

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

С ограничением мономорфизма тип f будет выглядеть так:

f :: Num a => [b] -> (a, a)

Таким образом, нет необходимости выполнять вычисления несколько раз.

  • Правило 1 предотвращает двусмысленность. Например, рассмотрим группу объявлений

    [(n,s)] = читает т

    Напомним, что reads стандартная функция, тип которой определяется сигнатурой

    читает:: (Читать a) => Строка -> [(a, Строка)]

    Без правила 1 n будет назначен тип ∀ a. Read a ⇒ a а также s тип ∀ a. Read a ⇒ String, Последний является недопустимым типом, потому что он по своей сути неоднозначен. Невозможно определить, какую перегрузку использовать s, и это не может быть решено путем добавления сигнатуры типа для s, Следовательно, когда используются непростые привязки к шаблону (раздел 4.4.3.2), выведенные типы всегда мономорфны в своих переменных ограниченного типа, независимо от того, предоставляется ли сигнатура типа. В этом случае оба n а также s мономорфны в a,

Ну, я считаю, что этот пример говорит сам за себя. Существуют ситуации, когда неприменение правила приводит к неоднозначности типа.

Если вы отключите расширение, как предложено выше, вы получите ошибку типа при попытке скомпилировать вышеуказанное объявление. Однако это на самом деле не проблема: вы уже знаете, что при использовании read Вы должны как-то сказать компилятору, какой тип он должен пытаться проанализировать...

Второе правило

  1. Любые переменные мономорфного типа, которые остаются, когда вывод типа для всего модуля завершен, считаются неоднозначными и разрешаются к определенным типам с использованием правил по умолчанию (раздел 4.3.4).

Это означает, что. Если у вас есть обычное определение:

plus = (+)

Это будет иметь тип Num a => a -> a -> a где a является переменной мономорфного типа в соответствии с правилом 1, описанным выше. После вывода всего модуля компилятор просто выберет тип, который заменит a в соответствии с правилами по умолчанию.

Окончательный результат: plus :: Integer -> Integer -> Integer,

Обратите внимание, что это делается после вывода всего модуля.

Это означает, что если у вас есть следующие объявления:

plus = (+)

x = plus 1.0 2.0

внутри модуля, перед типом по умолчанию тип plus будет: Fractional a => a -> a -> a (см. правило 1, почему это происходит). На данный момент, следуя правилам по умолчанию, a будет заменен на Double и так у нас будет plus :: Double -> Double -> Double а также x :: Double,

Дефолт

Как указывалось ранее, существуют некоторые правила по умолчанию, описанные в Разделе 4.3.4 Отчета, которые может принять эксперт, который заменит полиморфный тип на мономорфный. Это происходит всякий раз, когда тип неоднозначен.

Например, в выражении:

let x = read "<something>" in show x

здесь выражение неоднозначно, потому что типы для show а также read являются:

show :: Show a => a -> String
read :: Read a => String -> a

Итак x имеет тип Read a => a, Но это ограничение удовлетворяется многими типами: Int, Double или же () например. Какой выбрать? Там нет ничего, что может сказать нам.

В этом случае мы можем устранить неоднозначность, сообщив компилятору, какой тип нам нужен, добавив сигнатуру типа:

let x = read "<something>" :: Int in show x

Теперь проблема в том, что, поскольку Haskell использует Num Тип класса для обработки чисел, во многих случаях числовые выражения содержат неоднозначности.

Рассматривать:

show 1

Каким должен быть результат?

Как прежде 1 имеет тип Num a => a и есть много типов номеров, которые могут быть использованы. Какой выбрать?

Наличие ошибки компилятора почти каждый раз, когда мы используем число, не очень хорошая вещь, и поэтому были введены правила по умолчанию. Правила можно контролировать с помощью default декларация. Указав default (T1, T2, T3) мы можем изменить способ вывода по умолчанию различных типов.

Переменная неоднозначного типа v по умолчанию, если:

  • v появляется только в таких ограничениях C v мы C это класс (то есть если он выглядит так: Monad (m v) тогда это не дефолт).
  • по крайней мере, один из этих классов Num или подкласс Num,
  • все эти классы определены в Prelude или стандартной библиотеке.

Переменная типа по умолчанию заменяется первым типом в default список, который является экземпляром всех классов неоднозначной переменной.

По умолчанию default декларация default (Integer, Double),

Например:

plus = (+)
minus = (-)

x = plus 1.0 1
y = minus 2 1

Предполагаемые типы будут:

plus :: Fractional a => a -> a -> a
minus :: Num a => a -> a -> a

которые по умолчанию нарушают правила:

plus :: Double -> Double -> Double
minus :: Integer -> Integer -> Integer

Обратите внимание, что это объясняет, почему в примере в вопросе только sort определение вызывает ошибку. Тип Ord a => [a] -> [a] не может быть по умолчанию, потому что Ord не числовой класс.

Расширенные настройки по умолчанию

Обратите внимание, что GHCi поставляется с расширенными правилами по умолчанию (или для GHC8), которые также можно включить в файлах, используя ExtendedDefaultRules расширения.

Переменные типа по умолчанию должны появляться не только в тех ограничениях, где все классы являются стандартными, и должен быть хотя бы один класс из числа Eq, Ord, Show или же Num и его подклассы.

Кроме того, по умолчанию default декларация default ((), Integer, Double),

Это может привести к странным результатам. Возьмем пример из вопроса:

Prelude> :set -XMonomorphismRestriction
Prelude> import Data.List(sortBy)
Prelude Data.List> let sort = sortBy compare
Prelude Data.List> :t sort
sort :: [()] -> [()]

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

Полезные ссылки

Есть много ресурсов и дискуссий об ограничении мономорфизма.

Вот некоторые ссылки, которые я считаю полезными и которые могут помочь вам понять или углубиться в тему:

Источник
Другие вопросы по тегам