静的に型付けされた完全な Lisp バリアントは可能ですか? このようなものが存在することに意味さえありますか？Lisp 言語の長所の 1 つは、その定義の単純さにあると私は信じています。静的型付けは、このコア原則を損なうでしょうか?
29343 次
4 に答える
61
はい、それは非常に可能ですが、標準的なHMスタイルの型システムは通常ほとんどの慣用的なLisp/Schemeコードにとって間違った選択です。静的型付けを使用する「FullLisp」（実際にはSchemeに似ています）である最近の言語については、TypedRacketを参照してください。
于 2010-07-24T17:51:03.257 に答える
41
Lisp に似た静的に型付けされた言語だけが必要な場合は、言語を表す抽象構文ツリーを定義し、その AST を S 式にマッピングすることで、かなり簡単に実現できます。しかし、私はその結果を Lisp とは呼ばないと思います。
構文以外に実際に Lisp の特性を備えたものが必要な場合は、静的に型付けされた言語でこれを行うことができます。しかし、Lisp には多くの有用な静的型付けを得るのが難しい特徴があります。説明するために、Lisp の主要な構成要素を形成するconsと呼ばれるリスト構造自体を見てみましょう。
コンスをリストと呼ぶのは、リストの(1 2 3)ように見えますが、少し間違った名前です。たとえば、C++std::listや Haskell のリストのような静的に型付けされたリストとはまったく比較できません。これらは、すべてのセルが同じタイプの 1 次元リンク リストです。Lisp は喜んで を許可します(1 "abc" #\d 'foo)。さらに、リストのリストをカバーするために静的型付きリストを拡張したとしても、これらのオブジェクトの型では、リストのすべての要素がサブリストである必要があります。それらの中であなたはどのように表現((1 2) 3 4)しますか？
Lisp コンスは、葉 (アトム) と枝 (コンス) を持つ二分木を形成します。さらに、そのようなツリーの葉には、アトミックな (cons ではない) Lisp 型が含まれている可能性があります! この構造の柔軟性により、Lisp は記号計算、AST、および Lisp コード自体の変換をうまく処理できます!
では、そのような構造を静的に型付けされた言語でどのようにモデル化しますか? 非常に強力で正確な静的型システムを持つ Haskell で試してみましょう。
type Symbol = String
data Atom = ASymbol Symbol | AInt Int | AString String | Nil
data Cons = CCons Cons Cons
| CAtom Atom
最初の問題は、Atom タイプのスコープになります。明らかに、conses で使用したいすべてのタイプのオブジェクトをカバーするのに十分な柔軟性を備えた Atom タイプを選択していません。上記のように Atom データ構造を拡張しようとするのではなく (明らかに壊れやすいことがわかります)、Atomicアトミックにしたいすべての型を区別する魔法の型クラスがあるとしましょう。次に、次のことを試してみましょう。
class Atomic a where ?????
data Atomic a => Cons a = CCons Cons Cons
| CAtom a
ただし、ツリー内のすべてのアトムが同じタイプである必要があるため、これは機能しません。葉ごとに異なるようにしたいのです。より良いアプローチでは、Haskell の存在量指定子を使用する必要があります。
class Atomic a where ?????
data Cons = CCons Cons Cons
| forall a. Atomic a => CAtom a
しかし今、あなたは問題の核心に来ています。この種の構造の原子で何ができますか? でモデル化できる共通の構造は何Atomic aですか? そのような型でどのレベルの型安全性が保証されていますか? 型クラスに関数を追加していないことに注意してください。これには正当な理由があります。Lisp ではアトムに共通点はありません。Lisp でのそれらのスーパータイプは単純に呼び出されtます (つまり、トップ)。
それらを使用するには、アトムの値を実際に使用できるものに動的に強制するメカニズムを考え出す必要があります。その時点で、動的に型付けされたサブシステムを静的に型付けされた言語内に基本的に実装しました! ( Greenspun のプログラミングの第 10 規則の可能な結果に注意せずにはいられません。)
Haskell は、型とTypeable クラスと組み合わせてクラスを置き換えるために使用される、型を持つ動的サブシステムのサポートを提供することに注意してください。これは、Lisp の cons 構造を完全に一般的に扱うために使用する必要のある種類のシステムです。ObjDynamicAtomic
逆に、静的に型付けされたサブシステムを本質的に動的に型付けされた言語に埋め込むこともできます。これにより、より厳しい型要件を利用できるプログラムの部分の静的型チェックの利点が得られます。これは、たとえば、CMUCL の限られた形式の正確な型チェックで採用されているアプローチのようです。
最後に、動的および静的に型付けされた 2 つの別個のサブシステムを持つ可能性があります。これらは、コントラクト スタイルのプログラミングを使用して、2 つの間の移行をナビゲートするのに役立ちます。そうすれば、言語は、静的型チェックが助けになるというよりも障害となるような Lisp の使用法や、静的型チェックが有利になるような使用法に対応できます。以下のコメントからわかるように、これはTyped Racketが採用したアプローチです。
于 2010-07-24T19:55:52.007 に答える
10
私の答えは、自信がなくてもおそらくです。たとえば、SML のような言語を見て、それを Lisp と比較すると、それぞれの機能のコアはほとんど同じです。その結果、ある種の静的型付けを Lisp のコア (関数適用とプリミティブ値) に適用するのにそれほど苦労することはないように思われます。
あなたの質問は完全ですが、問題のいくつかが発生していると私が見ているのは、データとしてのコードのアプローチです。型は、式よりも抽象的なレベルで存在します。Lisp にはこの区別がありません。すべての構造が「フラット」です。ある式 E : T (ここで T はその型の何らかの表現) を考え、この式を単純な古いデータと見なすと、ここでの T の型は正確には何になるでしょうか? まあ、それは一種です！kind は高次の型です。コードでそれについて何か言いましょう。
E : T :: K
これで私がどこに向かっているのかわかるかもしれません。型情報をコードから分離することで、この種の型の自己参照性を回避できると確信していますが、それでは型の風味があまり「Lisp」ではなくなります。これにはおそらく多くの方法がありますが、どれが最良の方法であるかは私には明らかではありません。
編集: ああ、少しグーグルで調べたところ、Qiが見つかりました。これは、静的に型付けされていることを除いて、Lisp に非常に似ているように見えます。おそらく、静的型付けを取得するためにどこに変更を加えたかを確認するのに適した場所です。
于 2010-07-24T02:45:52.760 に答える
5
于 2010-07-24T18:34:14.010 に答える