Haskell 言語が参照透過性に関して提供する正確な約束/保証は何ですか? 少なくとも Haskell のレポートでは、この概念について言及されていません。
表現を考える
(7^7^7`mod`5`mod`2)
そして、この式が 1 かどうかを知りたいのです。安全のために、これを 2 回実行します。
( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(True,False)GHCi 7.4.1で提供されるようになりました。
明らかに、この式は今や参照的に不透明です。プログラムがそのような動作の対象であるかどうかをどのように判断できますか? 私はプログラム全体を氾濫させることができます::が、それは非常に読みやすいものにはなりません。私が見逃しているHaskellプログラムの他のクラスはありますか? それは完全に注釈付きのものと注釈なしのものの間ですか?
（私がSOで見つけた唯一の関連する質問とは別に、これには何か他のものがあるに違いありません）
5「互換性」の合理的な定義については、さまざまな型などで多形的に型指定された式を評価すると、「互換性のある」結果が生成されるという保証はないと思います。
GHCi セッション:
> class C a where num :: a
> instance C Int where num = 0
> instance C Double where num = 1
> num + length [] -- length returns an Int
0
> num + 0 -- GHCi defaults to Double for some reason
1.0
これは参照透過性を壊しているように見えますが、length []と0は等しいはずですが、内部でnumはさまざまな型で使用されています。
また、
> "" == []
True
> [] == [1]
False
> "" == [1]
*** Type error
False最後の行で期待できる場所。
したがって、参照透過性は、ポリモーフィズムを解決するために正確な型が指定されている場合にのみ有効だと思います。System F 風の明示的な型パラメータの適用は、セマンティクスを変更することなく、常に変数をその定義に置き換えることを可能にします: 私の理解する限り、GHC はセマンティクスが影響を受けないようにするために、最適化中にこれを内部的に行います。実際、GHCコアには、渡される明示的な型引数があります。
問題はオーバーロードです。これは、参照透過性に実際に違反しています。(+)Haskell でlike が何をするかはわかりません。タイプによって異なります。
Haskell プログラムで数値型が制約されていない場合、コンパイラは型のデフォルト設定を使用して適切な型を選択します。これは便宜上のものであり、通常は驚くようなことにはなりません。しかし、この場合、それは驚きにつながりました。ghc では-fwarn-type-defaults、コンパイラがデフォルト設定を使用して型を選択した時期を確認するために使用できます。default ()モジュールに行を追加して、すべてのデフォルト設定を停止することもできます。
物事を明確にするのに役立つかもしれない何かを考えました...
式mod (7^7^7) 5には型Integral aがあるため、式を に変換する一般的な方法が 2 つありますInt。
Integer、結果を に変換しIntます。Intます。式がIntコンテキストで使用されている場合、Haskell は方法 #2 を実行します。Haskell に #1 を強制的に使用させたい場合は、次のように記述する必要があります。
fromInteger (mod (7^7^7) 5)
これにより、すべての算術演算が演算Integerと型を使用して実行されることが保証されます。
ghci REPL で式を入力すると、デフォルト ルールによって式が として入力されたIntegerため、方法 1 が使用されました。演算子で式を使用すると、!!として入力されたIntので、方法 2 で計算されました。
私の元の答え：
Haskell では、次のような式の評価
(7^7^7`mod`5`mod`2)
使用されているインスタンスに完全に依存しIntegral、これはすべての Haskell プログラマーが受け入れることを学ぶものです。
すべてのプログラマーが (言語を問わず) 認識しなければならない 2 番目のことは、数値演算はオーバーフロー、アンダーフロー、精度の低下などの影響を受けやすいため、算術の法則が常に成り立つとは限らないということです。たとえば、x+1 > x常に真であるとは限りません。実数の足し算と倍数は常に結合するとは限りません。分配法則が常に成り立つわけではありません。オーバーフロー式を作成すると、未定義の動作の領域に入ります。
また、この特定のケースでは、この式を評価するためのより良い方法があります。これにより、結果がどうあるべきかについての期待がより維持されます。特に、a^b mod c を効率的かつ正確に計算したい場合は、「power mod」アルゴリズムを使用する必要があります。
更新: 次のプログラムを実行して、Integralインスタンスの選択が式の評価にどのように影響するかを確認します。
import Data.Int
import Data.Word
import Data.LargeWord -- cabal install largeword
expr :: Integral a => a
expr = (7^e `mod` 5)
where e = 823543 :: Int
main :: IO ()
main = do
putStrLn $ "as an Integer: " ++ show (expr :: Integer)
putStrLn $ "as an Int64: " ++ show (expr :: Int64)
putStrLn $ "as an Int: " ++ show (expr :: Int)
putStrLn $ "as an Int32: " ++ show (expr :: Int32)
putStrLn $ "as an Int16: " ++ show (expr :: Int16)
putStrLn $ "as a Word8: " ++ show (expr :: Word8)
putStrLn $ "as a Word16: " ++ show (expr :: Word16)
putStrLn $ "as a Word32: " ++ show (expr :: Word32)
putStrLn $ "as a Word128: " ++ show (expr :: Word128)
putStrLn $ "as a Word192: " ++ show (expr :: Word192)
putStrLn $ "as a Word224: " ++ show (expr :: Word224)
putStrLn $ "as a Word256: " ++ show (expr :: Word256)
出力 (GHC 7.8.3 (64 ビット) でコンパイル):
as an Integer: 3
as an Int64: 2
as an Int: 2
as an Int32: 3
as an Int16: 3
as a Word8: 4
as a Word16: 3
as a Word32: 3
as a Word128: 4
as a Word192: 0
as a Word224: 2
as a Word256: 1
Haskell 言語が参照透過性に関して提供する正確な約束/保証は何ですか? 少なくとも Haskell のレポートでは、この概念について言及されていません。
Haskell は正確な約束や保証を提供しません。unsafePerformIOorのような、traceShow参照透過でない関数が多数存在します。ただし、 Safe Haskellと呼ばれる拡張機能は、次の約束を提供します。
参照透過性 — 安全な言語の関数は決定論的であり、それらを評価しても副作用は発生しません。IO モナド内の関数は引き続き許可され、通常どおりに動作します。ただし、純粋な関数は、その型に応じて、実際に純粋であることが保証されています。このプロパティにより、安全な言語のユーザーは型を信頼できます。これは、たとえば、 unsafePerformIO :: IO a -> a 関数が安全な言語では許可されていないことを意味します。
Haskell は、これ以外の非公式な約束を提供します。Prelude と基本ライブラリには副作用がない傾向があり、Haskell プログラマーは、副作用をそのようにラベル付けする傾向があります。
明らかに、この式は今や参照的に不透明です。プログラムがそのような動作の対象であるかどうかをどのように判断できますか? プログラム全体を :: で埋め尽くすことはできますが、それでは非常に読みやすくなりません。私が見逃しているHaskellプログラムの他のクラスはありますか? それは完全に注釈付きのものと注釈なしのものの間ですか?
他の人が言ったように、問題はこの動作から生じます。
Prelude> ( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(True,False)
Prelude> 7^7^7`mod`5`mod`2 :: Integer
1
Prelude> 7^7^7`mod`5`mod`2 :: Int
0
これ7^7^7は、64 ビット型では簡単にオーバーフローする膨大な数 (10 進数で約 700,000 桁)が原因でInt発生しますが、32 ビット システムでは問題を再現できません。
Prelude> :m + Data.Int
Prelude Data.Int> 7^7^7 :: Int64
-3568518334133427593
Prelude Data.Int> 7^7^7 :: Int32
1602364023
Prelude Data.Int> 7^7^7 :: Int16
8823
rem (7^7^7) 5Int64 に剰余を使用すると、次のように報告されます-3が、-3 は 5 を法とする +2 と同等であるため、+2 と報告されmodます。
クラスのIntegerデフォルト規則により、答えは左側で使用されます。Integralのタイプのため、プラットフォーム固有のIntタイプが右側で使用され(!!) :: [a] -> Int -> aます。代わりに適切なインデックス演算子を使用すると、Integral a一貫したものが得られます。
Prelude> :m + Data.List
Prelude Data.List> ((7^7^7`mod`5`mod`2) == 1, genericIndex [False,True] (7^7^7`mod`5`mod`2))
(True,True)
ここでの問題は、参照の透過性ではありません^。なぜなら、呼び出している関数は実際には2 つの異なる関数(型が異なるため) だからです。つまずいたのは型クラスです。これは、Haskellで制約付きのあいまいさを実装したものです。このあいまいさ (制約のないあいまいさ、つまりパラメトリック型とは異なり) が直感に反する結果をもたらす可能性があることを発見しました。これはそれほど驚くべきことではありませんが、確かに少し奇妙です。
!!が必要なため、別のタイプが選択されましたInt。完全な計算では、Intの代わりに を使用するようになりIntegerました。
λ> ( (7^7^7`mod`5`mod`2 :: Int)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(False,False)
これが参照透過性とどう関係していると思いますか? あなたの7, ^, mod, ,5の使用は2、これらの変数を辞書==に適用したものですが、その事実が Haskell を参照的に不透明にする理由がわかりません。結局のところ、同じ関数を異なる引数に適用すると、結果が異なることがよくあります。
参照透過性は、次の式と関係があります。
let x :: Int = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)
xここでは単一の値であり、常に同じ単一の値を持つ必要があります。
対照的に、あなたが言うなら：
let x :: forall a. Num a => a; x = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)
(または同等の式 inline を使用します)は関数になり、指定した引数にx応じて異なる値を返すことができます。isNumと文句を言ったほうがいいかもしれませんが、「Haskell はコンテキストに応じて に異なる値を与えるので、参照的に不透明です」!let f = (+1) in map f [1, 2, 3][2, 3, 4]let f = (+3) in map f [1, 2, 3][4, 5, 6]map f [1, 2, 3]
おそらく、型推論と参照透過性に関連するもう 1 つのことは、「恐ろしい」モノモーフィズムの制限です (正確には、その欠如)。直接引用：
「Haskell の歴史」からの例:
genericLength 関数を考えてみましょう。Data.List
genericLength :: Num a => [b] -> aそして、関数を考えてみましょう:
f xs = (len, len) where len = genericLength xs
lenには型がNum a => aあり、単相性の制限がなければ、2 回計算できます。
この場合、両方の式の型が同じであることに注意してください。結果も同様ですが、代替が常に可能であるとは限りません。