13

与えられた型シグネチャに対して、この型の Haskell 式を再構築するプログラムを書いてa -> b -> aいます\x -> \_ -> x。この問題の背後にある理論について読んだことがありますが、このハワード・カリー同形性があることを知っています。私のプログラムが入力を解析し、それを用語として表現することを想像します。次に、特定のタイプの項を構築できるかどうかを教えてくれる SLD 解決を起動します (たとえば、Pierce の場合は不可能です)。私がまだ知らないのは、この解決中に Haskell 式を実際に作成する方法です。djinn のコードを見たことがありますが、少し複雑です。これがどのように機能するかについての一般的な考え方を把握したいと思います。

4

1 に答える 1

1

Curry-Howard を使用して Haskell のサブセットをいくつかの直観的なロジックに接続すると、証明項から Haskell プログラムを抽出するのは非常に簡単になるはずです。基本的に、証明項は既に Haskell プログラムとまったく同じ構造を持っているはずですが、異なるコンストラクタ名を使用しているだけです。コンストラクター名を頭の中で適切に変換すれば、証明用語と Haskell 用語の両方に同じ代数データ型を使用することもできると思います。例えば：

type Name = String

data Type                  -- aka. Formula
  = Function Type Type     -- aka. Implication
  | TypeVar Name           -- aka. PropositionalVar

data Term                  -- aka. Proof
  = Lambda Name Type Term  -- aka. ImplicationIntroduction
  | Apply Term Term        -- aka. ImplicationElimination
  | TermVar Name           -- aka. Start / Identity / Axiom / Copy

スコープ内の変数のコンテキストを使用する必要があります (別名、想定できる仮説)。

type TypingContext = Map Name Type -- aka. Hypotheses

このような型が与えられた場合、関数を「ただ」書く必要があります。

termOf :: Type -> TypingContext -> Maybe Term

しかし、おそらく最初のステップとして、演習として逆関数を最初に書く方が良いでしょう:

typeOf :: Term -> TypingContext -> Maybe Type

これら 2 つの関数の基本的な構造は似ているはずです: 持っているもののパターン マッチ、適用可能な型付け規則 (別名、証明規則) の決定、部分的な結果を構築するために自分自身を再帰的に呼び出し、コンストラクターでラップして部分的な結果を完成させるこれは、型付け規則 (別名、証明規則) に対応します。違いは、typeOf用語全体を歩いてすべてを把握できることtermOfですが、推測がうまくいかない場合は、おそらく推測して後戻りする必要があります。したがって、おそらく、実際には のリストモナドが必要ですtermOf。

typeOf最初に書くことの利点は次のとおりです。

  1. 用語には型よりも多くの情報が含まれる傾向があるため、その追加情報を作成する必要があるときにtermOfその追加情報を使用できるため、より簡単になるはずです。typeOf
  2. typeOf多くの人が演習として実装しますが、演習として実装する人はほとんどいないため、より多くのヘルプが利用できますtermOf。
于 2013-09-09T06:46:33.470 に答える