45

Haskellのリストが無限であるかどうかを知る方法はありますか？lengthその理由は、無限リストなどの関数を適用したくないからです。

4

6 に答える 6

32

未知のリストに適用するlengthことは、実際には無限のリストのため、そして概念的には、とにかく実際には長さを気にしないことがしばしば判明するため、一般的に悪い考えです。

あなたはコメントで言った：

私はHaskellに非常に慣れていないので、今では、無限の構造が私のプログラムを非常に脆弱にしませんか？

あまり。必然的に有限のデータと必然的に無限のデータを区別するためのより良い方法があることを望む人もいますが、怠惰な構造を段階的に作成、処理、および調査するときは常に安全です。長さの計算は明らかに増分ではありませんが、長さがカットオフ値を上回っているか下回っているかを確認することは、とにかくやりたいことのすべてです。

些細なケースは、空でないリストのテストです。isNonEmpty xs == length xs > 0単一の要素を調べるだけで十分な場合、無制限の数の要素を調べるため、これは悪い実装です。これを比較してください：

isNonEmpty [] = False
isNonEmpty (_:_) = True

これは無限リストに安全に適用できるだけでなく、有限リストでもはるかに効率的です。リストの長さが線形である時間ではなく、一定の時間しかかかりません。また、標準ライブラリ関数のnull実装方法でもあります。

カットオフに関連する長さテストのためにこれを一般化するには、明らかに、比較している長さと同じくらい多くのリストを調べる必要があります。標準ライブラリ関数を使用して、これを正確に行うことができますが、それ以上はできませんdrop。

longerThan :: Int -> [a] -> Bool
longerThan n xs = isNonEmpty $ drop n xs

n長さと（おそらく無限の）リストが与えられると、これは存在する場合の最初の要素をxs削除し、結果が空でないかどうかを確認します。リストの長さよりも大きい場合は空のリストが生成されるため、これはすべての正の整数に対して正しく機能します（つまり、標準ライブラリには、自然数などの非負の整数型はありません）。nxsdropnn

ここで重要な点は、ほとんどの場合、リストを単純なデータ構造ではなく、反復ストリームと考える方がよいということです。可能であれば、変換、累積、切り捨てなどを実行し、リスト全体を一度に処理しようとするのではなく、出力として別のリストを作成するか、リストの既知の有限量のみを調べます。

このアプローチを使用すると、関数は有限リストと無限リストの両方で正しく機能するだけでなく、怠惰とGHCのオプティマイザーの恩恵を受け、より高速に実行され、より少ないメモリを使用する可能性があります。

于 2011-09-10T16:26:49.777 に答える
27

停止問題は、最初に停止オラクルが存在すると仮定し、次にそのオラクルが起こると言ったのとは逆のことをする関数を書くことによって解決できないことが証明されました。ここでそれを再現しましょう：

isInfinite :: [a] -> Bool
isInfinite ls = {- Magic! -}

今、私たちはそれがすべきだと言っていることimpossibleListの反対をするリストを作りたいと思いisInfiniteます。したがって、impossibleListが無限大の場合は実際には[]であり、無限大でない場合はですsomething : impossibleList。

-- using a string here so you can watch it explode in ghci
impossibleList :: [String]
impossibleList =
    case isInfinite impossibleList of
        True -> []
        False -> "loop!" : impossibleList

isInfinite = const Trueとでghciでこれを試してみてくださいisInfinite = const False。

于 2011-09-10T13:48:26.767 に答える
13

「長さ」を安全に呼び出すために停止性問題を解く必要はありません。保守的である必要があります。有限性の証明があるものはすべて受け入れ、そうでないものはすべて拒否します（多くの有限リストを含む）。これはまさに型システムの目的であるため、次の型を使用します（tは要素型であり、無視します）。

terminatingLength :: (Finite a) => a t -> Int
terminatingLength = length . toList

Finiteクラスには有限リストのみが含まれるため、タイプチェッカーは有限の引数があることを確認します。Finiteのメンバーシップは、有限性の証明になります。「toList」関数は、有限値を通常のHaskellリストに変換するだけです。

class Finite a where
  toList :: a t -> [t]

今、私たちのインスタンスは何ですか？空のリストは有限であることがわかっているので、それらを表すデータ型を作成します。

-- Type-level version of "[]"
data Nil a = Nil
instance Finite Nil where
  toList Nil = []

要素を有限リストに「cons」すると、有限リストが得られます（たとえば、「xs」が有限の場合、「x：xs」は有限です）。

-- Type-level version of ":"
data Cons v a = Cons a (v a)

-- A finite tail implies a finite Cons
instance (Finite a) => Finite (Cons a) where
  toList (Cons h t) = h : toList t -- Simple tail recursion

terminationLength関数を呼び出す人は、リストが有限であることを証明する必要があります。そうしないと、コードがコンパイルされません。これは停止性問題の問題を取り除くものではありませんが、実行時ではなくコンパイル時にシフトしました。Finiteのメンバーシップを判別しようとしているときにコンパイラーがハングする場合がありますが、予期しないデータが与えられたときに実動プログラムをハングさせるよりも優れています。

注意：Haskellの「アドホック」ポリモーフィズムでは、コード内の他のポイントで有限のほぼ任意のインスタンスを宣言できます。terminationLengthは、そうでない場合でも、これらを有限性の証明として受け入れます。しかし、これはそれほど悪くはありません。誰かがあなたのコードの安全メカニズムを迂回しようとすると、彼らは彼らが値するエラーを受け取ります;）

于 2012-09-19T13:05:42.630 に答える
11 
isInfinite x = length x `seq` False
于 2011-09-10T19:52:34.200 に答える
7

いいえ-せいぜい見積もりかもしれません。停止性問題を参照してください。

于 2011-09-10T12:44:28.977 に答える
1

設計によって有限リストと無限リストを分離し、それらに異なるタイプを使用する可能性もあります。

残念ながら、Haskell（たとえばAgdaとは異なり）では、データ構造が常に有限であることを強制することはできません。それを確実にするために、完全な関数型プログラミングの手法を採用できます。

そして、無限リスト（別名ストリーム）を次のように宣言できます

data Stream a = Stream a (Stream a)

これには、シーケンスを終了する方法がありません（基本的にはなしのリスト[]です）。

于 2014-05-23T05:54:05.330 に答える