Как работает "undefined" в Haskell

Ответ 1

Нет ничего особенного в undefined. Это просто исключительная ценность - вы можете представить ее с помощью бесконечного цикла или сбоя или segfault. Один из способов записать это как сбой:

undefined :: a
undefined | False = undefined

Или цикл:

undefined = undefined

Это исключительное значение, которое может быть элементом любого типа.

Поскольку Haskell ленив, вы все равно можете использовать такие значения в вычислениях. Например.

 > length [undefined, undefined]
 2

Но в остальном это просто естественное следствие полиморфизма и нестрочности.

Ответ 2

Интересное свойство, которое вы изучаете, состоит в том, что undefined имеет тип a для любого типа a, который мы выбираем, т.е. undefined :: a без ограничений. Как отмечали другие, undefined можно рассматривать как ошибку или бесконечный цикл. Хотелось бы утверждать, что лучше подумать о нем как о "откровенно истинном заявлении". Это почти неизбежное отверстие в системе любого типа, тесно связанное с проблемой остановки, но интересно думать об этом с точки зрения логики.

Один из способов подумать о программировании с помощью типов - это загадка. Кто-то дает вам тип и просит вас реализовать функцию, которая имеет этот тип. Например,

Question:    fn  ::  a -> a
Answer:      fn  =  \x -> x

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

С undefined эта игра всегда легко

Question:    fn  ::  Int -> m (f [a])
Answer:      fn  =  \i   -> undefined    -- backdoor!

поэтому избавьтесь от него. Понять смысл undefined проще всего, когда вы живете в мире без него. Теперь наша игра становится сложнее. Иногда это возможно

Question:    fn  :: (forall r. (a -> r) -> r) -> a
Answer:      fn  =  \f                        -> f id

Но внезапно это иногда также невозможно!

Question:    fn  ::  a -> b
Answer:      fn  =   ???                  -- this is `unsafeCoerce`, btw.
                                          -- if `undefined` isn't fair game,
                                          -- then `unsafeCoerce` isn't either

Или это?

-- The fixed-point combinator, the genesis of any recursive program

Question:    fix  ::  (a -> a) -> a
Answer:      fix  =   \f       -> let a = f a in a

                                          -- Why does this work?
                                          -- One should be thinking of Russell 
                                          -- Paradox right about now. This plays
                                          -- the same role as a non-wellfounded set.

Это законно, потому что привязка Haskell let является ленивой и (обычно) рекурсивной. Теперь мы золотые.

Question:    fn   ::  a -> b
Answer:      fn   =  \a -> fix id         -- This seems unfair?

Даже без встроенного undefined мы можем перестроить его в нашей игре, используя любой старый бесконечный цикл. Виды проверяются. Чтобы по-настоящему не позволить себе иметь undefined в Haskell, нам нужно решить проблему остановки.

Question:    undefined  ::  a
Answer:      undefined  =   fix id

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

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

Но в Haskell нас больше интересует цикл, чем проверка, поэтому мы предпочли бы иметь fix, чем быть уверенным, что не было undefined.

Ответ 3

Если я попробую undefined в GHCi, я получаю исключение:

Prelude> undefined
*** Exception: Prelude.undefined

Поэтому я предполагаю, что он просто реализован как исключение:
http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Exception.html#g:2

Ответ 4

Как работает undefined? Ну, лучший ответ, IMHO, заключается в том, что он не работает. Но чтобы понять этот ответ, мы должны проработать его последствия, которые не очевидны для новичков.

В принципе, если у нас есть undefined :: a, то для системы типов это означает, что undefined может появляться где угодно. Зачем? Поскольку в Haskell всякий раз, когда вы видите выражение, имеющее некоторый тип, вы можете специализировать этот тип, последовательно подставляя все экземпляры любых своих переменных типа для любого другого типа. Знакомыми примерами будут такие вещи:

map :: (a -> b) -> [a] -> [b]

-- Substitute b := b -> x
map :: (a -> b -> c) -> [a] -> [b -> c]

-- Substitute a := Int
map :: (Int -> b -> c) -> [Int] -> [b -> c]

-- etc.

В случае map, как это работает? Ну, дело сводится к тому, что аргументы map предоставляют все, что необходимо для создания ответа, независимо от того, какие замены и специализации мы делаем для своих переменных типа. Если у вас есть список и функция, которая потребляет значения того же типа, что и элементы списка, вы можете делать то, что делает карта, период.

Но в случае undefined :: a то, что эта сигнатура будет означать, заключается в том, что независимо от того, какой тип a может стать специализированным, undefined может создать значение этого типа. Как это можно сделать? Ну, на самом деле, это невозможно, поэтому, если программа действительно достигает шага, где требуется значение undefined, пути для продолжения нет. Единственное, что программа может сделать в этот момент, - это сбой

История этого другого случая аналогична, но отличается:

loop :: a
loop = loop

Здесь мы можем доказать, что loop имеет тип a этим сумасшедшим аргументом: предположим, что loop имеет тип a. Он должен создать значение типа a. Как это можно сделать? Легко, он просто вызывает loop. Presto!

Это звучит безумно, не так ли? Ну, дело в том, что он действительно ничем не отличается от того, что происходит во втором уравнении этого определения map:

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

В этом втором уравнении f x имеет тип b, а (f x:) имеет тип [b] -> [b]; теперь, чтобы завершить наше доказательство того, что map действительно имеет тип, который требует наша подпись, нам нужно написать a [b]. Итак, как мы это делаем? Предположим, что map имеет тип, который мы пытаемся доказать.

Как работает алгоритм вывода типа Haskell, он сначала догадывается, что тип выражения a, а затем он меняет свое предположение только тогда, когда находит что-то, что противоречит этому предположению. undefined typechecks до a, потому что это плоская ложь. loop typechecks до a, потому что рекурсия разрешена, и все loop выполняет функцию recurse.

РЕДАКТИРОВАТЬ: Что, черт возьми, я мог бы также изложить один пример. Здесь неформальная демонстрация того, как вывести тип map из этого определения:

map f [] = []
map f (x:xs) = f x : map f xs

Это происходит следующим образом:

• Начнем с предположения, что map :: a.
• Но карта принимает два аргумента, поэтому a не может быть типом. Мы пересматриваем наше предположение: map :: a -> b -> c; f :: a.
• Но, как мы видим в первом уравнении, вторым аргументом является список: map :: a -> [b] -> c; f :: a.
• Но, как мы видим в первом уравнении, результатом является также список: map :: a -> [b] -> [c]; f :: a.
• Во втором уравнении мы сопоставляем второй аргумент с конструктором (:) :: b -> [b] -> [b]. Это означает, что в этом уравнении x :: b и xs :: [b].
• Рассмотрим правую часть второго уравнения. Поскольку результат map f (x:xs) должен иметь тип [c], это означает, что f x : map f xs также должен иметь тип [c].
• Учитывая тип конструктора (:) :: c -> [c] -> [c], это означает, что f x :: c и map f xs :: [c].
• В (7) мы пришли к выводу, что map f xs :: [c]. Мы предположили, что в (6), и если бы мы заключили иначе в (7), это было бы ошибкой типа. Мы также можем теперь погрузиться в это выражение и посмотреть, какие типы для этого требуют f и xs, но чтобы сделать более длинную историю коротким, все, что нужно проверить.
• Так как f x :: c и x :: b, мы должны заключить, что f :: b -> c. Итак, теперь мы получаем map :: (b -> c) -> [b] -> [c].
• Мы закончили.

Тот же процесс, но для loop = loop:

• Предположим, что loop :: a.
• loop не принимает аргументов, поэтому его тип соответствует a.
• Правая часть loop - это loop, которую мы условно присвоили type a, чтобы проверить.
• Больше нечего обсуждать; были сделаны. loop имеет тип a.

Ответ 5

Ну, в основном undefined = undefined - если вы попытаетесь оценить его, вы получите бесконечный цикл. Но Haskell является нестрогим языком, поэтому head [1.0, 2.0, undefined] не оценивает все элементы списка, поэтому печатает 1.0 и завершает работу. Но если вы напечатаете show [1.0, 2.0, undefined], вы увидите [1.0,2.0,*** Exception: Prelude.undefined.

Как он может быть из всех типов... Ну, если выражение имеет тип A, это означает, что его оценка либо даст значение типа A, либо оценка будет расходиться, не давая значения вообще. Теперь undefined всегда расходится, поэтому он вписывается в определение для любого воображаемого типа A.

Кроме того, хорошая запись в блоге по смежным темам: http://james-iry.blogspot.ru/2009/08/getting-to-bottom-of-nothing-at-all.html

Ответ 6

Есть две отдельные вещи, которые нужно отметить о undefined:

• Вы можете поместить undefined почти всюду, и typechecker будет счастлив. Это потому, что undefined имеет тип (forall a. A).
• Вы можете поместить undefined почти всюду, и во время выполнения у него будет определенное представление.

Во втором, комментарий GHC четко говорит:

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

Для более подробной информации вы можете прочитать статью Spinless Tagless G-Machine.