タイトルに書いてあること。型シグネチャを記述した場合、その型シグネチャを持つ式をアルゴリズムで生成することは可能ですか?
これを行うことが可能である可能性はもっともらしいと思われます。型がライブラリ関数の型署名の特殊なケースである場合、Hoogle はその関数をアルゴリズムで見つけることができることは既にわかっています。一方、一般式に関連する多くの単純な問題は実際には解決できないため (たとえば、2 つの関数が同じことを行うかどうかを知ることは不可能です)、これがそれらの 1 つであることはほとんど信じられません。
一度にいくつかの質問をするのはおそらく悪い形ですが、私は知りたいです:
それはできますか？
もしそうなら、どのように？
そうでない場合、それが可能になる制限された状況はありますか?
2 つの異なる式が同じ型シグネチャを持つ可能性は十分にあります。それらをすべて計算できますか？それともそれらのいくつかですか？
このようなことを実際に行う作業コードを持っている人はいますか?
Djinnは、1 次ロジックに対応する、Haskell 型の制限されたサブセットに対してこれを行います。ただし、再帰型または再帰を実装する必要がある型を管理することはできません。したがって、たとえば、 「 a が aを意味する場合、a」という命題に対応する型(a -> a) -> a( の型) の項を書くことはできません。これは明らかに誤りです。何でも証明できます。確かに、これが⊥ を生じさせる理由です。fixfix
を許可すれば、fix任意の型の項を与えるプログラムを書くのは簡単です。プログラムはfix idすべてのタイプを単純に出力します。
Djinn はほとんどおもちゃですが、との型を指定しての正しいMonadインスタンスを導出するなど、いくつかの楽しいことを行うことができます。djinnパッケージをインストールするか、それをコマンドとして統合するlambdabotを使用して試すことができます。ReaderContreturn(>>=)@djinn
okmij.orgのOlegがこれを実装しています。ここに短い紹介がありますが、リテラシーのある Haskell ソースには、プロセスの詳細と説明が含まれています。(これがジンの権力にどのように対応するのかはわかりませんが、別の例です。)
固有の機能がない場合があります。
fst', snd' :: (a, a) -> a
fst' (a,_) = a
snd' (_,b) = b
これだけではありません。関数が無数にある場合があります。
list0, list1, list2 :: [a] -> a
list0 l = l !! 0
list1 l = l !! 1
list2 l = l !! 2
-- etc.
-- Or
mkList0, mkList1, mkList2 :: a -> [a]
mkList0 _ = []
mkList1 a = [a]
mkList2 a = [a,a]
-- etc.
（合計関数のみが必要な場合は、などの[a]無限リストに制限されていると考えてください。つまり、）list0list1data List a = Cons a (List a)
実際、再帰型がある場合、これらを含む型は無限の関数に対応します。ただし、少なくとも上記の場合、関数の数は数え切れないほどあるため、それらすべてを含む (無限の) リストを作成することができます。[a] -> [a]しかし、型は数え切れないほどの無限の関数に対応していると思います (ここでも[a]無限のリストに制限されています) ので、それらをすべて列挙することさえできません!
(要約: 有限、可算無限、不可算無限の関数に対応する型があります。)
これは一般的には不可能であり (強力な正規化プロパティさえも持たない Haskell のような言語では)、一部の (非常に) 特殊なケース (およびより制限された言語) でのみ可能です。コンストラクター (たとえば、関数f :: forall a. a -> ()は一意に決定できます)。与えられた署名の可能な定義のセットを 1 つの定義のみを持つシングルトン セットに減らすには、より多くの制限を与える必要があります (たとえば、追加のプロパティの形で、与えずにこれがどのように役立つかを想像することはまだ困難です。使用例です）。
(n-)categorical の観点から、型はオブジェクトに対応し、用語は矢印に対応し (コンストラクターも矢印に対応します)、関数定義は 2-矢印に対応します。この問題は、一連のオブジェクトのみを指定することによって、必要なプロパティを持つ 2 カテゴリを構築できるかどうかという問題に似ています。矢印と 2-矢印の明示的な構成 (つまり、用語と定義の記述)、または特定のプロパティ セット (明示的に定義する必要がある) を使用して必要な構造を推測できる演繹的なシステムのいずれかが必要なため、これは不可能です。
興味深い質問もあります: ADT (つまり、Hask のサブカテゴリ) が与えられた場合、Typeable、Data (はい、SYBを使用)、Traversable、Foldable、Functor、Pointed、Applicative、Monad など (? ）。この場合、必要な署名と追加のプロパティがあります (たとえば、モナドの法則。これらのプロパティは Haskell では表現できませんが、依存型を持つ言語では表現できます)。いくつかの興味深い構造があります:
http://ulissesaraujo.wordpress.com/2007/12/19/catamorphisms-in-haskell
これは、リスト ADT に対して何ができるかを示しています。
タイプファミリーやGADTなどを含むHaskellタイプの完全な栄光について尋ねているのであれば、質問は実際にはかなり深く、私には答えがわかりません.
あなたが求めているのは、プログラムがそのような値を示すことによって、任意の型が存在する (値を含む)ことを自動的に証明できるかどうかです。Curry-Howard Correspondence と呼ばれる原則では、型は数学的命題として解釈でき、その命題が構成的に証明可能である場合に型が存在すると述べています。つまり、特定のクラスの命題が定理であることを証明できるプログラムがあるかどうかを尋ねています。Agda のような言語では、型システムは任意の表現を行うのに十分強力です。ゲーデルの不完全性定理では、任意の命題を証明することはできません。一方、(たとえば) 純粋な Hindley-Milner に落とし込むと、はるかに弱く、(私が思うに) 決定可能なシステムになります。Haskell 98 では、型クラスは GADT と同等になるはずなので、よくわかりません。
GADT の場合、それが決定可能かどうかはわかりませんが、ここに詳しい知識のある人ならすぐにわかるでしょう。たとえば、特定のチューリング マシンの停止問題を GADT としてエンコードできる可能性があるため、マシンが停止した場合にそのタイプの値が存在します。その場合、居住性は明らかに決定的ではありません。しかし、型ファミリーであっても、そのようなエンコーディングはおそらく不可能です。私は現在、このテーマについて十分に堪能ではないので、どちらにしても明らかではありませんが、私が言ったように、ここにいる他の誰かが答えを知っているかもしれません.
(更新:)ああ、あなたの質問のはるかに単純な解釈が思い浮かびます. 答えは明らかにそうではありません。ポリモーフィック型を考慮する
a -> b
その署名を持つ関数はありません (型システムを矛盾させる unsafeCoerce のようなものは数えません)。