haskell - Haskellで破棄された値が⊥ではなく（）であるのはなぜですか？

Answer 1

これは、破棄する値の型を指定する必要があるためだと思います。Haskell-98 では()、当然の選択です。そして、タイプが であることがわかっている限り()、値()を作成することもできます (評価がそこまで進むと仮定します)。ほとんどのプログラマーは余分な ⊥ をコードに導入することを好まないと思います。私は確かにそれを避けます。

の代わりに()、無人型を作成することも可能です (もちろん ⊥ を除く)。

{-# LANGUAGE EmptyDataDecls #-}

data Void

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

Voidコンストラクターがないため、パターン マッチを実行することさえできません。これが頻繁に行われない理由は、EmptyDataDecls 拡張機能が必要なため、Haskell-98 と互換性がないためだと思います。

編集: Void でパターン マッチを行うことはできませんがseq、1 日が台無しになります。これを指摘してくれた@sacundimに感謝します。

Answer 2

ええと、bottom 型は文字通り非終了計算を意味し、unit 型はまさにその通りです - 単一の値が存在する型です。明らかに、モナド計算は通常、終了することを意図しているため、それらを返すようにすることは単に意味がありませんundefined。もちろん、これは単なる安全対策です。John L が言ったように、モナドの結果で誰かのパターンが一致したらどうなるでしょうか? そのため、モナド計算は (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

問題の関数を再実装して、zinm zまたはIO zをバインドしようとすると、変数がundefinedまたは 他のボトムにバインドされるようにします。

私たちは何を得ますか？undefined今では、これらの計算結果を強制するプログラムを書くことができます。それはどのように良いことですか？それが意味するのは、以前は書くことが不可能だった、正当な理由もなく終了に失敗するプログラムを人々が書くことができるようになったことだけです。

Answer 4

Answer 5

⊥ を返す特定の形式を書くことの重大な欠点を1 つ指摘したいと思います: このような型を書くと、悪いプログラムになります:

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!"

エラーは明らかで単純です: 括弧がありません。

• 型チェックします。これはまさに、型システムが簡単にキャッチできるはずの種類のエラーです。
• 実行時に無言で無限ループします(何も出力せずに)。デバッグするのは苦痛です。

なんで？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。

Answer 6