Почему 3 и x (которому было присвоено 3) имеют разные предполагаемые типы в Haskell?

Вывод типа в Haskell имеет некоторую кривую обучения (если не сказать больше!). Хороший способ начать обучение с простых примеров. Итак, следующее - это "привет мир" для вывода типов.

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

Prelude> :t 3
3 :: (Num t) => t
Prelude> let x = 3
Prelude> :t x
x :: Integer

Вопрос в следующем: почему 3 и x имеют разные типы?

Сводка ссылки:

Прочитайте ответы ниже для полной истории; вот только краткое изложение ссылки:

  1. Значение по умолчанию для типа GHC: раздел 4.3.4 отчета на Haskell
  2. По умолчанию расширенный тип GHCi: Использование GHCi, раздел 2.4.5
  3. Мономорфное ограничение: Haskell wiki
Источник

3 ответа

Решение

Здесь есть еще один фактор, упомянутый в некоторых ссылках, которые включает в себя acfoltzer, но, возможно, здесь стоит остановиться прямо. Вы сталкиваетесь с эффектом ограничения мономорфизма. Когда ты сказал

let x = 5

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

> :t 3
3 :: (Num t) => t

так как 3 действительно перегружен: он допускается любым числовым типом. Правила по умолчанию выбирают Integer как числовой тип по умолчанию, так

> let x = 3
> :t x
x :: Integer

Но теперь давайте выключим MR.

> :set -XNoMonomorphismRestriction
> let y = 3
> :t y
y :: (Num t) => t

Без MR определение настолько полиморфно, насколько это возможно, так же перегружено, как 3, Просто проверяю...

> :t y * (2.5 :: Float)
y * (2.5 :: Float) :: Float
> :t y * (3 :: Int)
y * (3 :: Int) :: Int

Обратите внимание, что полиморфный y = 3 по-разному специализируется на этих видах использования, в соответствии с fromInteger метод поставляется с соответствующими Num пример. То есть, y не связано с конкретным представлением 3, а скорее схема для построения представлений 3, Наивно скомпилированный, это рецепт медленного, который некоторые люди приводят в качестве мотивации для MR.

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

При попытке узнать, как работает система типов, действительно полезно отделить аспекты вывода типов, которые

  1. "следовать плану", специализируя полиморфные определения для конкретных случаев использования: довольно надежный вопрос решения ограничений, требующий базовой унификации и разрешения экземпляров с помощью обратной цепочки; а также

  2. "угадать план", обобщая типы, чтобы назначить схему полиморфного типа определению без сигнатуры типа: это довольно хрупко, и чем больше вы продвигаетесь мимо базовой дисциплины Хиндли-Милнера, с классами типов, с полиморфизмом более высокого ранга, с ГАДЦ, странными становятся вещи.

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

Источник

Это происходит из-за дефолта типа в GHCi, как обсуждалось здесь, здесь, здесь, и здесь, среди других. К сожалению, это кажется чем-то сложным для поиска, так как существует множество способов описать это поведение, прежде чем вы узнаете фразу "тип по умолчанию".

Обновление: D'Oh. Убран плохой пример.

Источник

Поскольку никто больше не упомянул, почему существует ограничение мономорфизма, я подумал, что добавлю этот бит из "Истории Хаскелла: быть ленивым с классом".

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

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

Теперь рассмотрим это определение:

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

Это выглядит, как если бы len должен быть вычислен только один раз, но на самом деле он может быть вычислен дважды. Зачем? Потому что мы можем вывести тип len :: (Num a) => a; когда desugared с переводом словаря, len становится функцией, которая вызывается один раз для каждого вхождения len, каждый из которых может использоваться в другом типе.

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

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

Ограничение мономорфизма явно бородавка на языке. Кажется, он кусает каждого нового программиста на Haskell, вызывая неожиданное или неясное сообщение об ошибке. Было много дискуссий об альтернативах. Компилятор Glasgow Haskell (GHC, раздел 9.1) предоставляет флаг:

-fno-monomorphism-restriction

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

Я нахожу тон бумаги в сторону ограничения мономорфизма очень интересным.

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