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

Ответ 1

Здесь есть еще один фактор, упомянутый в некоторых ссылках, которые включает в себя 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. Naïvely составлен, что рецепт для медленного, который некоторые люди называют мотивацией для MR.

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

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

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

• & lsquo; угадать план & rsquo;, обобщая типы, чтобы назначить схему полиморфного типа определению без подписи типа: это довольно хрупкое, и чем больше вы проходите мимо основной дисциплины Хиндли-Милнера, с типами классов, с полиморфизмом более высокого ранга, с GADT, становятся странными вещи.

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

Ответ 2

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

Обновление: D'oh. Удаленный пример.

Ответ 3

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

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

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

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

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

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

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

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

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

-fno-monomorphism-restriction

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

Я нахожу, что тон статьи к ограничению мономорфизма очень интересен.