Почему сброшенные значения:() вместо ⊥ в Haskell?

Ответ 1

Я думаю, это потому, что вам нужно указать тип значения, которое нужно отбросить. В Haskell-98, () - очевидный выбор. И до тех пор, пока вы знаете, что тип (), вы также можете сделать значение () (предполагая, что оценка продолжается так далеко), на случай, если кто-то попытается сопоставить шаблон с ним или что-то в этом роде. Я думаю, что большинству программистов не нравится вводить лишние ⊥ в код, потому что это просто дополнительная ловушка. Я, конечно, избегаю этого.

Вместо () можно создать неинжинированный тип (за исключением, конечно, ⊥).

{-# LANGUAGE EmptyDataDecls #-}

data Void

mapM_ :: (Monad m) => (a -> m b) -> [a] -> m Void

Теперь это даже не возможно совпадение шаблона, потому что нет конструктора Void. Я подозреваю, что причина этого не делается чаще всего потому, что она не совместима с Haskell-98, поскольку для нее требуется расширение EmptyDataDecls.

Изменить: вы не можете сопоставлять шаблоны с Void, но seq испортит ваш день. Спасибо @sacundim за это.

Ответ 2

Ну, нижний тип буквально означает неисчерпаемое вычисление, а тип единицы - это то, что он есть - тип, населенный единым значением. Очевидно, что монадические вычисления обычно должны быть закончены, поэтому просто не имеет смысла заставить их вернуться undefined. И, конечно же, это просто мера безопасности - точно так же, как сказал Джон Л, что, если кто-то из шаблонов совпадает с монадическим результатом? Таким образом, монадические вычисления возвращают "самый низкий" возможный (в Haskell 98) тип - единица.

Ответ 3

Итак, возможно, у нас могли бы быть следующие подписи:

mapM_     :: (Monad m) => (a -> m b) -> [a] -> m z
foldM_    :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m z
writeFile :: FilePath -> String -> IO z

Мы переопределили бы эти функции, чтобы любая попытка привязать z в m z или IO z привязывала переменную к undefined или к любому другому дну.

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

Ответ 4

Вы путаетесь между типами и значениями.

В writeFile :: FilePath -> String -> IO (), () - тип единицы. Значение, которое вы получаете для x, делая x <- writeFile foo bar в блоке do, является (обычно) значением (), которое является единственным недревесным обитателем типа ().

⊥ OTOH - значение. Поскольку ⊥ является членом любого типа, он также может использоваться как значение для типа (). Если вы отбрасываете это x выше, не используя его (мы обычно даже не извлекаем его в переменную), вполне может быть ⊥, и вы никогда не узнаете. В этом смысле у вас уже есть то, что вы хотите; если вы когда-либо пишете функцию, результат которой вы всегда будете игнорировать, вы можете использовать ⊥. Но так как ⊥ - это значение каждого типа, нет типа ⊥, и поэтому не существует типа IO ⊥.

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

⊥ в некотором смысле не имеет значения. 1 `div` 0 дает ⊥, потому что нет значения, которое могло бы быть использовано в результате этого выражения, которое удовлетворяет законам целочисленного деления. Выбрасывание исключения дает ⊥, потому что функции, содержащие исключения исключений, не дают вам значения их типа. Non-term дает ⊥, потому что выражение никогда не заканчивается значением. ⊥ - способ лечения всех этих незначений, как если бы они были ценностью для некоторых целей. Насколько я могу сказать, это в основном полезно, потому что Haskell лень означает, что ⊥ и структура данных, содержащая ⊥ (т.е. [⊥]), различаются.

Значение () не похоже на случаи, когда мы используем ⊥. writeFile foo bar не имеет "невозможного значения", такого как return $ 1 `div` 0, он просто не имеет информации в своем значении (кроме того, что содержится в монадической структуре). Есть совершенно разумные вещи, которые я могу сделать с (), которые я получаю от выполнения x <- writeFile foo bar; они просто не очень интересны, и поэтому никто их не делает. Это явно отличается от x <- return $ 1 `div` 0, где выполнение чего-либо с этим значением должно дать мне другое неправильное значение.

Ответ 5

() ⊤, т.е. тип устройства, а не ⊥ (нижний тип). Большая разница заключается в том, что тип единицы заселен, так что он имеет значение (() в Haskell), с другой стороны, нижний тип необитаем, так что вы не можете писать такие функции:

absurd : ⊥
absurd = -- no way

Конечно, вы можете сделать это в Haskell, поскольку "нижний тип" (конечно, нет такой вещи) здесь обитает undefined. Это делает Haskell непоследовательным.

Функции вроде этого:

disprove : a → ⊥
disprove x = -- ...

может быть записано, это то же самое, что и

disprove : ¬ a
disprove x = -- ...

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

В любом случае вы можете видеть, как тип единицы используется на разных языках, как () :: () в Haskell, () : unit в ML, () : unit в Scala и tt : ⊤ в Agda. В таких языках, как Haskell и Agda (с модой IO), такие функции, как putStrLn, должны иметь тип String → IO ⊤, а не String → IO ⊥, поскольку это абсурд (логически он утверждает, что нет строк, которые могут быть напечатаны, это просто не так).

ОТКАЗ ОТ ОТВЕТСТВЕННОСТИ: предыдущий текст использует Agda обозначение, и это больше касается Agda, чем Haskell.

В Haskell, если мы имеем

data Void

Это не означает, что Void необитаем. Он заселен undefined, не заканчивающимися программами, ошибками и исключениями. Например:

data Void

instance Show Void where
  show _ = "Void"

data Identity a = Identity { runIdentity :: a }

mapM__ :: (a -> Identity b) -> [a] -> Identity Void
mapM__ _ _ = Identity undefined

затем

print $ runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3]
-- ^ will print "Void".
case runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3] of _ -> print "1"
-- ^ will print "1".
let x = runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3]
x `seq` print x
-- ^ will thrown an exception.

Но это также не означает, что Void есть ⊥. Так

mapM_ :: Monad m => (a -> m b) -> [a] -> m Void

где Void декалируется как пустой тип данных, это нормально. Но

mapM_ :: Monad m => (a -> m b) -> [a] -> m ⊥

- это бессмысленность, но в Haskell такого типа, как., не существует.

Ответ 6

Я хотел бы указать на один серьезный недостаток, чтобы написать одну конкретную форму возврата ⊥: если вы пишете такие типы, вы получаете плохие программы:

mapM_ :: (Monad m) => (a -> m b) -> [a] -> m z

Это слишком полиморфно. В качестве примера рассмотрим forever :: Monad m => m a -> m b. Я столкнулся с этой ошибкой давным-давно, и я все еще горький:

main :: IO ()
main = forever putStrLn "This is going to get printed a lot!"

Ошибка очевидна и проста: отсутствующие круглые скобки.

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

Почему? Хорошо, потому что r -> - монада. Таким образом, m b соответствует практически любому. Например:

forever :: m a -> m b
forever putStrLn :: String -> b
forever putStrLn "hello!" :: b -- eep!
forever putStrLn "hello" readFile id flip (Nothing,[17,0]) :: t -- no type error.

Подобные вещи склоняют меня к мнению, что forever следует ввести m a -> m Void.