76

他の潜在的な貢献者への注意: 抽象的な表記法や数学的な表記法を使用して主張を主張することを躊躇しないでください。あなたの答えが不明な場合は、説明を求めますが、それ以外の場合は、快適な方法で自由に表現してください.

明確にするために：私は「安全な」を探しているわけではなく、特に例外的に意味のあるhead選択でもありません。head質問の本質は、コンテキストを提供するのに役立つheadとの議論に続きます。head'

私は数か月前から Haskell をハッキングしてきました (Haskell が私のメイン言語になるまで) が、より高度な概念や言語の哲学の詳細について十分な情報を得ていないことは確かです (ただし、私は学びたいと思っています）。私の質問は、哲学の 1 つであるため、あまり技術的なものではありません (そうであり、私がそれに気付いていない場合を除きます)。

この例では、 について話していheadます。

ご存知かと思いますが、

Prelude> head []    
*** Exception: Prelude.head: empty list

これは から続きますhead :: [a] -> a。けっこうだ。明らかに、(手を振って) no 型の要素を返すことはできません。しかし同時に、定義するのは簡単です (自明ではないにしても)。

head' :: [a] -> Maybe a
head' []     = Nothing
head' (x:xs) = Just x

これについては、特定のステートメントのコメント セクションで少し議論されているのを見ました。特に、あるアレックス・スタングルは次のように述べています。

「すべてを「安全」にせず、前提条件に違反した場合に例外をスローする正当な理由があります。」

私は必ずしもこの主張に疑問を抱くわけではありませんが、これらの「正当な理由」が何であるかについては興味があります.

さらに、ポール・ジョンソンは次のように述べています。

たとえば、「safeHead :: [a] -> Maybe a」を定義できますが、空のリストを処理したり、それが起こり得ないことを証明したりする代わりに、「Nothing」を処理するか、それが起こり得ないことを証明する必要があります.'

そのコメントから私が読んだトーンは、これが難易度/複雑さ/何かの顕著な増加であることを示唆していますが、彼がそこに何を出しているのか理解できません.

あるスティーブン・プルジナは、（2011年も同様に）次のように述べています。

「たとえば、「head」がクラッシュプルーフにならないのには、もっと深い理由があります。ポリモーフィックでありながら空のリストを処理するには、「head」は常に、特定の空のリストに存在しない型の変数を返さなければなりません。 Haskell がそれを行うことができれば Delphic...".

空のリストの処理を許可すると、ポリモーフィズムが失われますか? もしそうなら、どのように、そしてなぜですか？これを明らかにする特定のケースはありますか？このセクションは、@Russell O'Connor によって十分に回答されています。もちろん、それ以上の考えは大歓迎です。

明確さと提案が示すように、これを編集します。あなたが提供できる考え、論文などは、非常に高く評価されます。

4

6 に答える 6

104

空のリストの処理を許可すると、ポリモーフィズムが失われますか? もしそうなら、どのように、そしてなぜですか？これを明らかにする特定のケースはありますか？

head状態の自由定理

f . head = head . $map f

この定理を適用[]すると、

f (head []) = head (map f []) = head []

この定理はすべてfの について成立しなければならないので、特にconst Trueおよびについて成立しなければなりませんconst False。これは

True = const True (head []) = head [] = const False (head []) = False

したがって、headが適切にポリモーフィックでありhead []、合計値である場合、 はTrueと等しくなりFalseます。

PS。リストが空ではないという前提条件がある場合は、リストを使用する代わりに関数シグネチャで空でないリスト型を使用して強制する必要があるという質問の背景について、他にもいくつかコメントがあります。

于 2011-06-15T22:05:35.510 に答える
24

head :: [a] -> aパターン マッチングの代わりに使用するのはなぜですか? 理由の 1 つは、引数を空にすることはできないことがわかっているため、引数が空の場合を処理するコードを記述したくないためです。

もちろん、あなたhead'の型[a] -> Maybe aは標準ライブラリで として定義されていData.Maybe.listToMaybeます。しかし、 の使用を に置き換えるheadとlistToMaybe、空のケースを処理するコードを作成する必要があり、 を使用するこの目的が無効になりheadます。

head使用することが良いスタイルだと言っているのではありません。例外が発生する可能性があるという事実を隠しており、その意味では良くありません。でも便利な時もある。ポイントは、 がhead提供できないいくつかの目的を提供することlistToMaybeです。

質問の最後の引用（ポリモーフィズムについて）は[a] -> a、空のリストの値を返す型の関数を定義できないことを意味します（ラッセル・オコナーが彼の答えで説明したように）。

于 2011-06-15T22:28:48.130 に答える
8

次のことが当てはまると期待するのは当然xs === head xs : tail xsです。-リストは最初の要素と同じで、その後に残りの要素が続きます。論理的に見えますよね？

:ここで、実際の要素を無視して、conses（の適用）の数を数えましょう[]。：に「法則」と称するものを適用する場合は、[]と同じである必要がありますfoo : barが、前者のconsesは0で、後者のconsesは（少なくとも）1つです。ええと、何かがここにありません！

Haskellの型システムは、そのすべての長所のために、head空でないリストのみを呼び出す必要があるという事実を表現することはできません（そして、「法則」は空でないリストに対してのみ有効です）。を使用headすると、立証責任がプログラマーに移ります。プログラマーは、空のリストで使用されていないことを確認する必要があります。Agdaのような依存型言語がここで役立つと思います。

最後に、もう少し運用哲学的な説明：どのhead ([] :: [a]) :: aように実装する必要がありますか？薄い空気からタイプの価値をa引き出すことは不可能であり（のような無人のタイプを考えてdata Falsumください）、（カリーハワード同形を介して）何かを証明することになります。

于 2011-06-15T22:21:13.333 に答える
4

これについて考えるには、いくつかの異なる方法があります。だから私は賛成と反対の両方を議論するつもりですhead'：

に対してhead'：

必要はありませんhead'：リストは具体的なデータ型であるためhead'、パターンマッチングによって実行できることはすべて実行できます。

さらに、head'あるファンクターを別のファンクターと交換しているだけです。ある時点で、真ちゅう製の鋲に取り掛かり、基になるリスト要素でいくつかの作業を実行したいとします。

を守るためにhead'：

しかし、パターンマッチングは、何が起こっているのかを曖昧にします。Haskellでは、関数の計算に関心があります。これは、コンビネータとコンビネータを使用してポイントフリースタイルで関数を記述することでより適切に実行されます。

[]さらに、とMaybeファンクターについて考えるとhead'、それらの間を行ったり来たりすることができます（特にwithのApplicativeインスタンス）。[]pure = replicate

于 2011-06-15T21:32:31.973 に答える
3

ユースケースで空のリストがまったく意味をなさない場合は、いつでも安全に使用できるNonEmpty代わりに使用することを選択できます。neHeadその角度から見ると、head安全でないのは関数ではなく、リストのデータ構造全体です (繰り返しますが、そのユース ケースの場合)。

于 2011-06-16T06:56:52.830 に答える
1

これはシンプルさと美しさの問題だと思います。もちろん、それは見る人の目にあります。

Lisp のバックグラウンドを持っている場合、リストはコンス セルで構成されており、各セルにはデータ要素と次のセルへのポインターがあることに気付いているかもしれません。空のリストはそれ自体がリストではなく、特別なシンボルです。そして、Haskell はこの推論に従います。

私の見解では、空のリストとリストが2つの異なるものである場合、それはよりクリーンで、推論がより簡単で、より伝統的です。

...追加できます- head が安全でないことを心配している場合は、使用しないでください。代わりにパターンマッチングを使用してください:

sum     [] = 0
sum (x:xs) = x + sum xs
于 2011-06-15T21:23:00.110 に答える