28

Haskell の「未定義」値に興味があります。どこにでも置けるので興味深いですし、Haskell も喜ぶでしょう。以下はすべて問題ありません

[1.0, 2.0, 3.0 , undefined]  ::[Float]
[1, 2 ,3 undefined, 102312] :: [Int]
("CATS!", undefined)  :: (String, String)
....and many more

undefined は内部でどのように機能しますか? あらゆるデータ型のデータを持つことを可能にするものは何ですか? どこにでも置くことができるこのような値を定義することは可能でしょうか、それともこれは特別なケースですか?

4

6 に答える 6

34

について本当に特別なことは何もありませんundefined。これは単なる例外的な値です。無限ループ、クラッシュ、またはセグメンテーション違反で表すことができます。それを書く1つの方法は、クラッシュとしてです：

undefined :: a
undefined | False = undefined

またはループ:

undefined = undefined

これは、どのタイプの要素にもなり得る例外的な値です。

Haskell は遅延型であるため、計算でそのような値を引き続き使用できます。例えば

 > length [undefined, undefined]
 2

しかし、それ以外の場合は、ポリモーフィズムと非厳密性の自然な結果です。

于 2013-05-25T10:41:22.057 に答える
29

あなたが調べている興味深いプロパティは、選択した任意の型undefinedの型を持つ、つまり制約がないということです。他の人が指摘しているように、エラーまたは無限ループと見なされる可能性があります。それは「空虚な真実の陳述」と考えたほうがよいと私は主張したい。これは、停止問題に密接に関連する型システムではほぼ避けられない穴ですが、ロジックの観点から考えると楽しいものです。aaundefined :: aundefined

型を使ったプログラミングについて考える 1 つの方法は、それがパズルだということです。誰かがあなたに型を与え、その型の関数を実装するように求めます。例えば

Question:    fn  ::  a -> a
Answer:      fn  =  \x -> x

は簡単です。afor any typeを生成する必要がありaますが、入力として 1 つが与えられているため、それを返すことができます。

でundefined、このゲームはいつも簡単です

Question:    fn  ::  Int -> m (f [a])
Answer:      fn  =  \i   -> undefined    -- backdoor!

だから、それを取り除きましょう。undefinedあなたがそれのない世界に住んでいるときに、それを理解するのは最も簡単です。今、私たちのゲームは難しくなっています。可能な場合もある

Question:    fn  :: (forall r. (a -> r) -> r) -> a
Answer:      fn  =  \f                        -> f id

しかし、突然、それが不可能になることもあります。

Question:    fn  ::  a -> b
Answer:      fn  =   ???                  -- this is `unsafeCoerce`, btw.
                                          -- if `undefined` isn't fair game,
                                          -- then `unsafeCoerce` isn't either

またはそれは？

-- The fixed-point combinator, the genesis of any recursive program

Question:    fix  ::  (a -> a) -> a
Answer:      fix  =   \f       -> let a = f a in a

                                          -- Why does this work?
                                          -- One should be thinking of Russell's 
                                          -- Paradox right about now. This plays
                                          -- the same role as a non-wellfounded set.

letHaskellの束縛は怠惰で（一般的に）再帰的であるため、これは合法です。今、私たちは黄金です。

Question:    fn   ::  a -> b
Answer:      fn   =  \a -> fix id         -- This seems unfair?

組み込みがなくてundefinedも、古い無限ループを使用してゲーム内で再構築できます。タイプをチェックアウトします。本当にundefinedHaskell に取り込まれないようにするには、停止問題を解決する必要があります。

Question:    undefined  ::  a
Answer:      undefined  =   fix id

これまで見てきたundefinedように、 は任意の値のプレースホルダーにできるため、デバッグに役立ちます。残念ながら、無限ループまたは即時のクラッシュにつながるため、操作にはひどいものです。また、チートを可能にするため、ゲームにとっても非常に悪いことです。最後に、言語に (潜在的に無限の) ループがある限り、そうでないことはかなり難しいことを実証できたことを願っています。undefined

真にundefined. 彼らがこれを行うのは、私が発明したこのゲームが、場合によっては実際に非常に価値があるからです。論理のステートメントをエンコードできるため、非常に厳密な数学的証明を形成するために使用できます。型は定理を表し、プログラムはその定理が実証されていることを保証します。の存在はundefined、すべての定理が実証可能であることを意味し、したがってシステム全体が信頼できないものになります。

しかし、Haskell では、プルーフよりもループに関心がfixあるため、undefined.

于 2013-05-25T15:15:32.633 に答える
3

どのように機能しundefinedますか？まあ、私見の最良の答えは、それが機能しないということです。しかし、その答えを理解するには、その結果を理解する必要があります。これは、初心者には明らかではありません。

基本的に、 がある場合undefined :: a、型システムにとってそれが意味することは、undefinedどこにでも出現できるということです。なんで？Haskell では、何らかの型を持つ式を見つけるたびに、その型変数のすべてのインスタンスを一貫して他の型に置き換えることで型を特殊化できます。おなじみの例は、次のようなものです。

map :: (a -> b) -> [a] -> [b]

-- Substitute b := b -> x
map :: (a -> b -> c) -> [a] -> [b -> c]

-- Substitute a := Int
map :: (Int -> b -> c) -> [Int] -> [b -> c]

-- etc.

の場合、mapこれはどのように機能しますか? map結局のところ、の引数は、その型変数にどのような置換や特殊化を行っても、答えを生成するために必要なすべてのものを提供するという事実に帰着します。リストと、リストの要素と同じ型の値を消費する関数がある場合は、map が行うことを行うことができます。

しかし、 の場合、undefined :: aこの署名が意味することは、どの型aに特化されてもundefined、その型の値を生成できるということです。どうすればそれができますか？実際、それはできないので、プログラムが実際に の値undefinedが必要なステップに達した場合、続行する方法はありません。その時点でプログラムができる唯一のことは、失敗することです

この別のケースの背後にある話は似ていますが異なります。

loop :: a
loop = loop

ここで、loopが type を持っていることをa、この狂ったように聞こえる引数によって証明できます。type の値を生成する必要があります。どうすればそれができますか？簡単です。 を呼び出すだけです。プレスト！loopaaloop

それはクレイジーですね。問題は、この の定義の 2 番目の方程式で起こっていることと実際には違いがないということですmap。

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs

その 2 番目の式でf xは、 typebを(f x:)持ち、 type を持ち[b] -> [b]ます。mapここで、署名が主張する型を実際に持つ証明を結論づけるために、 を生成する必要があり[b]ます。では、どうやってそれをやっているのですか？それが型を持っていると仮定することmapで、それが型を持っていることを証明しようとしています!

Haskell の型推論アルゴリズムの仕組みは、最初に式の型がaであると推測し、その仮定に反するものを見つけたときにのみ推測を変更するというものです。 undefinedそれは完全aな嘘だからです。 再帰が許可されており、すべてが再帰であるため、loop型チェックは に行われます。aloop

編集：一体、私は1つの例を綴ったほうがいいかもしれません. mapこの定義からの型を推測する方法の非公式なデモを次に示します。

map f [] = []
map f (x:xs) = f x : map f xs

こんなふうになります：

  1. 暫定的に と仮定することから始めmap :: aます。
  2. ただし、 map は 2 つの引数を取るためa、型にすることはできません。仮定を次のように修正しますmap :: a -> b -> c; f :: a。
  3. しかし、最初の式からわかるように、2 番目の引数はリストですmap :: a -> [b] -> c; f :: a。
  4. しかし、最初の式でもわかるように、結果もリストになりますmap :: a -> [b] -> [c]; f :: a。
  5. 2 番目の式では、constructor に対して 2 番目の引数をパターン マッチングしています(:) :: b -> [b] -> [b]。これは、その式でx :: bとを意味しxs :: [b]ます。
  6. 2 番目の方程式の右辺を考えます。の結果はmap f (x:xs)型でなければならないので、それは型もなければならない[c]ことを意味します。f x : map f xs[c]
  7. コンストラクタの型を考えると(:) :: c -> [c] -> [c]、それはf x :: cとmap f xs :: [c].
  8. （7）では、次のように結論付けましたmap f xs :: [c]。(6) でそれを想定していましたが、(7) で別の結論を下した場合、これは型エラーでした。また、この式に飛び込んで、これが必要fとxsするタイプと持つ必要があるタイプを確認することもできますが、より長い話を短くするために、すべてをチェックアウトします。
  9. f x :: cとから、 とx :: b結論付けなければなりませんf :: b -> c。これで、 が得られmap :: (b -> c) -> [b] -> [c]ます。
  10. 終わったね。

同じプロセスですが、次の場合ですloop = loop。

  1. 仮に としloop :: aます。
  2. loopは引数を取らないので、その型はaこれまでと一貫しています。
  3. の右側loopはloopで、暫定的に type を割り当てaたので、チェックアウトします。
  4. これ以上考慮すべきことはありません。終わったね。 loopタイプがありaます。
于 2013-05-26T00:15:49.413 に答える