catch違反了語義逼近順序？

語義近似順序規定，如果函數f是在其參數不是其中的一個時定義的，那麼f在該參數中是常量（它不使用它）。但考慮這個功能，catch違反了語義逼近順序？

import Control.Exception 

handleAll :: SomeException -> IO() 
handleAll e = putStrLn "caught" 

f :: String -> IO() 
f x = catch (putStrLn x) handleAll

f undefined顯示在GHCI caught，所以看起來定義。但是f在它的論點中並不是不變的，因爲f "test"顯示爲test。

某處有錯嗎？

來源

2017-03-04 V. Semeria

沒有錯誤 - 此原則僅適用於純功能。（注意，即使這是不正確的，由於seq和朋友）。你只能看到區別，因爲你正在執行'IO'動作，'技術上'只能在'main'中使用' - 所有其他的'IO'操作只是建立新的術語，或者你不能觀察術語輸入'IO x'。 – user2407038

'seq'不違反這裏討論的原則。 –

'catch'事實上很難找到正確的答案。實際上，我在過去的一兩週內一直在努力修復相關的GHC錯誤。 – dfeuer

爲了正確建模異常和catch，術語需要更豐富的指稱語義，區分異常和非定義（並區分不同的異常）。有關GHC實現的語義，請參閱A semantics for imprecise exceptions (pdf)。

請注意，這對Haskell的「純片段」的指稱語義沒有影響，因爲您無法觀察純代碼中的IO a值（除了底部與非底部之間的區別）。

要澄清我的哈斯克爾的「純片段」的意思是，想象定義IO類型

data IO a = MkIO

和catch作爲

catch a h = MkIO

現在有沒有問題與您f，因爲f undefined和f "test"都等於MkIO。從指稱語義的角度來看，這對應於解釋

[IO t] = {⊥<⊤}

由於操作只有我們可以用IO操作都被seq荷蘭國際集團他們並結合他們進入其他的IO動作，這是一個完全一致的指稱語義，不會影響你談論length :: [Bool] -> Integer等語義的能力。對於理解執行IO操作時發生的情況恰好是沒用的。但是如果你想用指稱語義來對待它，除了例外之外，你會遇到很多困難。

來源

2017-03-04 16:25:51

如果你寫的只有一個'IO a'（只有一個構造函數'MkIO'沒有參數），編譯器會優化'f'，強制它不變，等於這個唯一'IO a'。 GHCi的執行結果表明，這並非如此。我從文章中瞭解到不準確的例外情況，GHC區分了幾種底部：可以捕捉的底部，其他底部，如無限循環，不能。我想知道如何通過庫裏霍華德翻譯，底部與數學錯誤有關，只有一個。 –

當然，我明確指出，這種指稱語義（異常識別爲非終止，IO視爲單例）並不能幫助您預測執行IO操作時會發生什麼情況。 –

catch違反了語義逼近順序？

回答

相關問題