31

それで、私は最近、coinduction について少し読んでいて、今疑問に思っています: Haskell リストは帰納的ですか、それとも共帰納的ですか? Haskell ではこの 2 つを区別していないと聞いたことがありますが、もしそうなら、どのように正式に区別しているのでしょうか?

リストは帰納的に定義されますが、同時帰納的data [a] = [] | a : [a]に使用できますones = a:ones。無限リストを作成できます。それでも、有限リストを作成できます。それで、彼らはどれですか？

関連は Idris にあり、型List aは厳密に帰納型であり、したがって有限リストのみです。Haskell での定義と同じように定義されています。ただし、Stream a無限リストをモデル化する共導型です。として定義されています（というか、定義は同等です）codata Stream a = a :: (Stream a)。無限のリストや有限のストリームを作成することはできません。しかし、定義を書くと

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

Haskell のリストに期待する動作が得られます。つまり、有限構造と無限構造の両方を作成できます。

それでは、いくつかの核となる質問に要約してみましょう。

  1. Haskell は誘導型と共誘導型を区別しませんか? もしそうなら、その公式化は何ですか？そうでない場合、[a] はどれですか?

  2. HList は導帰的ですか? もしそうなら、どのようにして帰納型に有限値を含めることができますか?

  3. を定義するとどうなるdata HList' a = L (List a) | R (Stream a)でしょうか? それは何と考えられますか、そして/またはそれはただよりも役に立ちHListますか?

4

3 に答える 3

19

Coq や Agda のような総合言語では、帰納型とは、値が有限時間内に取り壊される可能性がある型のことです。誘導関数は終了する必要があります。一方、結合型は、有限時間で値を構築できる型です。結合関数は生産的でなければなりません。

証明アシスタントとして役立つことを意図したシステム (Coq や Agda など)は完全でなければなりません。しかし、すべての機能が総体的で帰納的であることを要求すると、無限の構造を扱うことが不可能になるため、共帰結が発明されました。

したがって、帰納型および共導型の目的は、終了しない可能性のあるプログラムを拒否することです。生産性条件のために拒否された関数の Agda の例を次に示します。(渡された関数filterはすべての要素を拒否する可能性があるため、結果のストリームの次の要素を永遠に待機する可能性があります。)

filter : {A : Set} -> (A -> Bool) -> Stream A -> Stream A
filter f xs with f (head xs)
... | true = head xs :: filter f (tail xs)
... | false = filter f (tail xs)  -- unguarded recursion

現在、Haskell には帰納型または共帰納型の概念はありません。「このタイプは帰納的ですか、共導的ですか？」という質問。意味のあるものではありません。Haskell はどのように区別せずに逃げるのでしょうか? そもそも、Haskell はロジックとして一貫性を保つことを意図したものではありません。これは部分的な言語です。つまり、非終了および非生産的な関数を記述できます。終了チェッカーも生産性チェッカーもありません。この設計上の決定の賢明さについて議論することはできますが、それは確かに誘導と共誘導を冗長にします.

代わりに、Haskell プログラマーは、プログラムの終了/生産性について非公式に推論することに慣れています。怠惰により、無限のデータ構造を扱うことができますが、関数が完全であることを確認するための機械からの助けは得られません。

于 2016-10-04T17:04:35.437 に答える