Вывод типа мешает ссылочной прозрачности

Ответ 1

Проблема заключается в перегрузке, которая действительно является нарушением ссылочной прозрачности. Вы не представляете, что делает что-то вроде (+) в Haskell; это зависит от типа.

Когда числовой тип не поддерживается в программе Haskell, компилятор использует тип по умолчанию для выбора подходящего типа. Это для удобства и обычно не приводит к неожиданностям. Но в этом случае это привело к неожиданности. В ghc вы можете использовать -fwarn-type-defaults, чтобы увидеть, когда компилятор использовал умолчание, чтобы выбрать тип для вас. Вы также можете добавить строку default () в свой модуль, чтобы остановить все дефолты.

Ответ 2

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

Сеанс GHCi:

> class C a where num :: a
> instance C Int    where num = 0
> instance C Double where num = 1
> num + length []  -- length returns an Int
0
> num + 0          -- GHCi defaults to Double for some reason
1.0

Похоже, что он нарушает реляционную прозрачность, так как length [] и 0 должны быть равны, но под капотом это num используется при разных типах.

Кроме того,

> "" == []
True
> [] == [1]
False
> "" == [1]
*** Type error

где можно было ожидать False в последней строке.

Итак, я считаю, что ссылочная прозрачность выполняется только тогда, когда для разрешения полиморфизма заданы точные типы. Явное применение параметра типа à la System F позволит всегда подставлять переменную с ее определением без изменения семантики: насколько я понимаю, GHC внутренне делает именно это во время оптимизации, чтобы гарантировать, что семантика не затронута. В самом деле, GHC Core имеет явные аргументы типа, которые передаются.

Ответ 3

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

Выражение mod (7^7^7) 5 имеет тип Integral a, поэтому есть два общих способа их преобразования в Int:

• Выполните всю арифметику с помощью операций и типов Integer, а затем преобразуйте результат в Int.
• Выполнять всю арифметику с помощью операций Int.

Если выражение используется в контексте Int, Haskell выполнит метод # 2. Если вы хотите заставить Haskell использовать № 1, вы должны написать:

fromInteger (mod (7^7^7) 5)

Это обеспечит выполнение всех арифметических операций с использованием операций и типов Integer.

Когда вы вводите его выражение в ghci REPL, правила по умолчанию набирают выражение как Integer, поэтому был использован метод # 1. Когда вы используете выражение с оператором !!, оно было напечатано как Int, поэтому оно было вычислено методом # 2.

Мой оригинальный ответ:

В Haskell оценка выражения типа

(7^7^7`mod`5`mod`2)

полностью зависит от того, какой экземпляр Integral используется, и это то, что каждый программист Haskell учит принимать.

Вторая вещь, о которой должен знать каждый программист (на любом языке), - это то, что числовые операции подвержены переполнению, недопущению, потере точности и т.д., и поэтому законы для арифметики могут не всегда выполняться. Например, x+1 > x не всегда истинно; добавление и кратное действительных чисел не всегда ассоциативно; закон распределения не всегда выполняется; и т.д. Когда вы создаете переполняющее выражение, вы вводите область поведения undefined.

Кроме того, в этом конкретном случае есть более эффективные способы оценить это выражение, которое сохраняет больше нашего ожидания того, каким должен быть результат. В частности, если вы хотите эффективно и точно вычислить a ^ b mod c, вы должны использовать алгоритм "power mod".

Обновление. Запустите следующую программу, чтобы увидеть, как выбор экземпляра Integral влияет на то, что выражение оценивает:

import Data.Int
import Data.Word
import Data.LargeWord -- cabal install largeword

expr :: Integral a => a
expr = (7^e `mod` 5)
  where e = 823543 :: Int

main :: IO ()
main = do
  putStrLn $ "as an Integer: " ++ show (expr :: Integer)
  putStrLn $ "as an Int64:   " ++ show (expr :: Int64)
  putStrLn $ "as an Int:     " ++ show (expr :: Int)
  putStrLn $ "as an Int32:   " ++ show (expr :: Int32)
  putStrLn $ "as an Int16:   " ++ show (expr :: Int16)
  putStrLn $ "as a Word8:    " ++ show (expr :: Word8)
  putStrLn $ "as a Word16:   " ++ show (expr :: Word16)
  putStrLn $ "as a Word32:   " ++ show (expr :: Word32)
  putStrLn $ "as a Word128:  " ++ show (expr :: Word128)
  putStrLn $ "as a Word192:  " ++ show (expr :: Word192)
  putStrLn $ "as a Word224:  " ++ show (expr :: Word224)
  putStrLn $ "as a Word256:  " ++ show (expr :: Word256)

и вывод (скомпилированный с GHC 7.8.3 (64-разрядный):

as an Integer: 3
as an Int64:   2
as an Int:     2
as an Int32:   3
as an Int16:   3
as a Word8:    4
as a Word16:   3
as a Word32:   3
as a Word128:  4
as a Word192:  0
as a Word224:  2
as a Word256:  1

Ответ 4

Каково точное обещание/гарантия, предоставляемая языком Haskell в отношении ссылочной прозрачности? По крайней мере, в докладе Haskell не упоминается это понятие.

Haskell не дает четких обещаний или гарантий. Существует множество функций, таких как unsafePerformIO или traceShow, которые не являются ссылочно прозрачными. Расширение под названием Safe Haskell, однако, обеспечивает следующее обещание:

Ссылочная прозрачность. Функции на безопасном языке детерминированы, их оценка не вызывает никаких побочных эффектов. Функции в монаде IO все еще допускаются и ведут себя как обычно. Любая чистая функция, хотя, по ее типу, гарантированно будет чистой. Это свойство позволяет пользователю безопасного языка доверять типам. Это означает, например, что функция unsafePerformIO:: IO a → a запрещена на безопасном языке.

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

Очевидно, что это выражение теперь по-видимому непрозрачно. Как я могу узнать, зависит ли программа от такого поведения? Я могу нагрузить программу с помощью:: на всем протяжении, но это не делает ее очень читаемой. Существует ли какой-либо другой класс программ Haskell, который я пропустил? Это между полностью аннотированным и неаннотированным?

Как говорили другие, проблема возникает из этого поведения:

Prelude> ( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(True,False)
Prelude> 7^7^7`mod`5`mod`2 :: Integer
1
Prelude> 7^7^7`mod`5`mod`2 :: Int
0

Это происходит потому, что 7^7^7 - огромное количество (около 700 000 десятичных цифр), которое легко переполняет 64-разрядный тип Int, но проблема не будет воспроизводиться в 32-битных системах:

Prelude> :m + Data.Int
Prelude Data.Int> 7^7^7 :: Int64
-3568518334133427593
Prelude Data.Int> 7^7^7 :: Int32
1602364023
Prelude Data.Int> 7^7^7 :: Int16
8823

Если использовать rem (7^7^7) 5, остаток для Int64 будет представлен как -3, но поскольку -3 эквивалентен +2 по модулю 5, mod сообщает +2.

Ответ Integer используется слева из-за правил по умолчанию для классов Integral; специфический для платформы тип Int используется справа из-за типа (!!) :: [a] -> Int -> a. Если вы используете соответствующий оператор индексирования для Integral a, вместо этого вы получите что-то непротиворечивое:

Prelude> :m + Data.List
Prelude Data.List> ((7^7^7`mod`5`mod`2) == 1, genericIndex [False,True] (7^7^7`mod`5`mod`2))
(True,True)

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

Ответ 5

Был выбран другой тип, потому что !! требует Int. Теперь полное вычисление использует Int вместо Integer.

λ> ( (7^7^7`mod`5`mod`2 :: Int)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(False,False)

Ответ 6

Как вы думаете, что это имеет отношение к ссылочной прозрачности? Ваши применения 7, ^, mod, 5, 2 и == являются приложениями этих переменных к словарям, да, но я не понимаю, почему вы думаете, что факт делает Haskell ссылочно непрозрачный. Часто применение одной и той же функции к различным аргументам приводит к различным результатам, в конце концов!

Реляционная прозрачность связана с этим выражением:

let x :: Int = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

x - это одно значение и всегда должно иметь одно и то же значение.

В отличие от этого, если вы скажете:

let x :: forall a. Num a => a; x = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

(или используйте выражение inline, которое эквивалентно), x теперь является функцией и может возвращать разные значения в зависимости от аргумента Num, который вы ему предоставляете. Вы можете также пожаловаться, что let f = (+1) in map f [1, 2, 3] - [2, 3, 4], но let f = (+3) in map f [1, 2, 3] - [4, 5, 6], а затем говорит: "Haskell дает разные значения для map f [1, 2, 3] в зависимости от контекста, поэтому он ссылочно непрозрачен"!

Ответ 7

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

Пример, из "История Хаскелла":
Рассмотрим функцию genericLength, от Data.List

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

И рассмотрим функцию:

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

len имеет тип Num a => a и, без ограничения мономорфизма, его можно было бы вычислить дважды.

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