6

GHC発生チェックは、無限の型を構築することを防ぎます。コードの一般的なエラーを防ぐこと、またはタイプチェッカーが無期限にループすることを防ぐこと、あるいはその両方を目的としていますか？

それはどのようなケースを識別し、悪意のあるユーザーがそれをだまして（Safe Haskellコンテキストのように）ループさせる可能性がありますか？型システムがチューリング完全である場合（そうですか？）、GHCが計算の停止を保証する方法がわかりません。

4

4 に答える 4

10

型推論は、連立方程式を解くことと考えてください。例を見てみましょう：

f x = (x,2)

どうすればタイプを推測できfますか？これが関数であることがわかります。

f :: a -> b

さらに、の構造からf、次の方程式がシミュレート的に成り立つことがわかります。

b = (c,d)
d = Int
c = a

この連立方程式を解くことにより、のタイプがであることがわかりfますa -> (a, Int)。次に、次の（誤った）関数を見てみましょう。

f x = x : x

のタイプ(:)はa -> [a] -> [a]、であるため、次の連立方程式が生成されます（簡略化）。

a = a
a = [a]

したがって、方程式が得られます。この方程式a = [a]から、この連立方程式には解がないため、コードは適切に型指定されていないと結論付けることができます。方程式を棄却しなかった場合a = [a]、実際に無限ループに入り、方程式、、、などをシステムに追加しa = [a]ます（または、ダニエルが彼の回答で述べているように、型システムで無限型を許可することもできますが、タイプチェックなどの誤ったプログラム）。a = [[a]]a = [[[a]]]f x = x : x

ghciでこれをテストすることもできます：

> let f x = x : x

<interactive>:2:15:
    Occurs check: cannot construct the infinite type: a0 = [a0]
    In the second argument of `(:)', namely `x'
    In the expression: x : x
    In an equation for `f': f x = x : x

他の質問について：GHC Haskellの型システムはチューリング完全ではなく、タイプチェッカーは停止することが保証されています-有効UndecidableInstancesにしない限り、有効にすると、理論的には無限ループに入る可能性があります。ただし、GHCは、固定深度の再帰スタックを持つことで終了を保証するため、停止しないプログラムを構築することはできません（編集： CAMcCannのコメントによると、結局のところ可能です-末尾再帰の類似物がありますスタックの深さを増やさずにループできるタイプレベル）。

ただし、Hindley-Milner型推論の複雑さは、最悪の場合（平均ではありません！）では指数関数的であるため、コンパイルに任意の長い時間をかけることができます。

dup x = (x,x)

bad = dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup
      . dup . dup . dup . dup . dup . dup . dup . dup

安全なHaskellはこれからあなたを保護しません-潜在的に悪意のあるユーザーがあなたのシステムでHaskellプログラムをコンパイルすることを許可したいなら、 muevalを見てください。

于 2012-09-19T13:43:18.833 に答える
8

GHC発生チェックは、無限の型を構築することを防ぎます。

これは、構文的に無限である型を防ぐという非常に文字通りの意味でのみ当てはまります。ここで実際に行われているのは、ある意味で再帰をインライン化するために統合アルゴリズムが必要となる再帰型です。

再帰を明示的にすることで、まったく同じ型を定義することが常に可能です。これは、タイプレベルバージョンのfix：を使用して、一般的に行うこともできます。

newtype Fix f = Fix (f (Fix f))

例として、タイプFix ((->) a)は。と統合するのと同じbです(a -> b)。

ただし、実際には、「無限タイプ」エラーは、ほとんどの場合、コード内のエラーを示します（したがって、壊れている場合は、おそらくそうすべきではありませんFix）。通常のシナリオは、引数の順序を混同するか、明示的な型シグネチャを使用しないコードの間違った場所に式を配置することです。

正しい方法で非常に素朴な型推論システムは、メモリがなくなるまで再帰を拡張する可能性がありますが、停止性問題は発生しません-型がそれ自体の一部と統合する必要がある場合、それは決して起こりません動作するように（少なくともHaskellでは、代わりにnewtype上記の明示的に再帰的なものと同等として扱う言語が存在する可能性があります）。

GHCの型チェックも型推論も、有効にしない限りチューリング完全ではありません。有効UndecidableInstancesにすると、関数従属性または型族を介して任意の計算を実行できます。

Safe Haskellは、実際にはまったく登場しません。有限であるにもかかわらずシステムメモリを使い果たす非常に大きな推論型を生成するのは簡単です。メモリが役立つ場合、SafeHaskellはUndecidableInstancesとにかく使用を制限しません。

于 2012-09-19T14:04:50.607 に答える
7

ブックマークに次のすばらしいメールがあります。無限のタイプに問題はありません。無限のタイプであっても、タイプチェッカーをループさせる危険性はありません。UndecidableInstances型システムはチューリング完全ではありません（拡張機能のようなものであるように明示的に要求しない限り）。

于 2012-09-19T13:36:21.663 に答える
4

（Haskellコンパイラーの）目的は、コードの一般的なエラーを防ぐことです。型の無限再帰をサポートする型チェッカーと推論エンジンを構築することが可能です。この質問にはさらにいくつかの情報があります。

OCamlはで再帰型を実装し-rectypesているので、それは間違いなく可能です。OCamlコミュニティは、発生する問題のいくつかに精通しています（動作はデフォルトでオフになっています）。

発生チェックは、無限の型拡張を識別します。たとえば、次のコードは次のとおりです。

Prelude> let a = [a]
<interactive>:2:10:
    Occurs check: cannot construct the infinite type: t0 = [t0]
    In the expression: a
    In the expression: [a]
    In an equation for `a': a = [a]

手作業でタイプを計算しようとすると、タイプは[ [ [ [ ... ] ] ] ]です。そのような型は無限であるため、手で書くことは不可能です。

発生チェックは、型推論とは別の段階である型推論中に発生します。無限の型は手動で注釈を付けることができないため、推測する必要があります。Haskell-98型推論は決定可能であるため、コンパイラーをだましてループさせることは不可能です（もちろん、この例が悪用していると思われるバグを除いて）。GHCはデフォルトで、型推論も決定可能なシステムFの制限されたサブセットを使用します。などの一部の拡張機能ではRankNTypes、GHCは型推論が決定不可能なコードを許可しますが、型アノテーションが必要になるため、型推論ステージがループする危険はありません。

チューリング完全言語は決定不可能であるため、デフォルトの型システムをチューリング完全にすることはできません。GHCの型システムが拡張機能のいくつかの組み合わせを有効にしてチューリング完全になるかどうかはわかりませんが、特定の拡張機能（たとえばUndecidableInstances）では、スタックオーバーフローでコンパイラをクラッシュさせるコードを記述できます。

ちなみに、発生チェックを無効にすることの主な問題は、多くの一般的なコーディングミスが無限のタイプエラーを引き起こすことです。したがって、無効にすると、通常、解決するよりも多くの問題が発生します。無限型を使用する場合は、newtypeラッパーを使用すると、余分な表記をあまり使用せずに使用できます。

于 2012-09-19T14:58:36.117 に答える