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

Question

Howcome in Haskell, когда есть значение, которое будет отбрасываться, вместо ⊥ используется ()?

Примеры (не могу думать ни о чем, кроме действий ввода-вывода на данный момент):

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

Под строгой оценке, это имеет смысл, но в Haskell, он только делает домен больше.

Возможно, есть «не используется параметр» функции d -> a которые являются строго по d (где d является неограниченным параметр типа и не появляется свободно в a)? Пример: seq, const' x y = y след x.

Answer 1

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

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

{-# LANGUAGE EmptyDataDecls #-} 

data Void 

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

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

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

Answer 2

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

Answer 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 результат этих вычислений. Как это хорошо? Все это означает, что люди теперь могут писать программы, которые не могут быть прекращены без уважительной причины, которые невозможно было написать раньше.

Answer 4

() является ⊤, т.е. unit type, не ⊥ (The bottom type).Большая разница в том, что тип устройства заселен, так что она имеет значение (() в 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 является decalred, как пустой тип данных, это нормально. Но

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

это бессмыслица, но нет такого типа, как ⊥ в Haskell.

Answer 5

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

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

Answer 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.