MPS 2024.1 ヘルプ

型システム

言語のための型システムを定義する

このページでは、MPS 型システムについて詳しく説明します。最初の型システムの規則を定義する際に、さらに簡単に導入したい場合は、型システムクックブックをチェックしてください。

コードから型システムを使用する方法をよく知りたい場合は、型システムを使うの章も参照してください。

型システムとは

型システムは、言語を使用して書かれたモデル内のノードに型を割り当てる言語定義の一部です。型システム言語は、ノードとそのタイプに対する特定の制約をチェックするためにも使用されます。ノードの種類に関する情報は、次の場合に役立ちます。

  • 型エラーを見つける

  • 適切なジェネレータールールのみを適用するために生成中にノードの型の条件をチェックする

  • 特定に必要な情報を提供するリファクタリング (たとえば、「変数の導入」リファクタリングの場合)

  • およびその他

タイプ

MPS が言語のノードに型を割り当てることができるようにするには、型システムの言語アスペクトを作成する必要があります。ご使用の言語の型システムモデルは、型システム言語で記述されます。

タイプの概念

MPS では、型は通常の概念として定義されています。式 (ノード) は、typeof(thisNode) :==: new node<MyType> などの型推論規則で型の概念をインスタンス化することによって型を示します。一部の概念は、子として型情報を持ちます (例: BaseLanguage の VariableDeclaration)。型は、型システムが割り当てるノード上のマーカーと考えてください。

型は、より大きな型（型パラメーターなど）に自由に組み合わせることができます。ただし、すべての概念が型として機能するわけではありません。型自体ではない型の概念では、子を避けることをお勧めします。これは、型システムが 2 つの型を比較するときに、それらの内容が等しいかどうかを比較し、一致が完全である場合にのみ、ノードを同じ型として扱うためです。型も一般的にストレージから独立していますが、通常のノードはいくつかのモデルに属しています。

一部のタイプは、追加情報を保持する必要はありません。例: BaseLanguage の IntegerType は、式が数値の値を表すことを示す単なるインジケーターです - int a = 5;

一部のタイプは、プロパティ、子、または他のノードへの参照を保持する必要がある場合があります。たとえば、BaseLanguage の ClassifierType は、クラスによって定義されたタイプを表します。

ClassifierTypex1.png

事実上、ClassifierType は、それを使用して型指定された式が評価された後、そのクラスのインスタンスであるというアサーションとして機能する用語（ノード）です。

推論ルール

型システム言語の主な概念は推論規則です。ある概念の推論規則は、主にその概念のインスタンスの型を計算する責任があります。

推論規則は、条件と本体で構成されています。条件は、ルールが特定のノードに適用可能かどうかを判断するために使用されます。条件には、概念参照またはパターンの 2 種類があります。概念参照の形式の条件付き規則は、その概念のすべてのインスタンスおよびそのサブコンセプトに適用できます。パターン付きルールは、そのパターンに一致するノードに適用できます。ノードがパターンと同じプロパティと参照を持ち、その子がパターンの子と一致する場合、そのノードはパターンと一致します。パターンは、すべてに一致するいくつかの変数を含むこともあります。

推論規則の本体は、規則がノードに適用されたときに実行されるステートメントのリストです。型システム言語の主な種類のステートメントは、方程式間の作成およびタイプ間の不等式に使用されるステートメントです。

推論ルールは、overrides ブロックを定義できます。これは、条件で指定された概念のスーパーコンセプトに適用できる他の推論ルールがある場合に、この推論ルールが優先され、条件に指定された概念のすべてのルールが優先されることをタイプチェッカーに指示するブールフラグです。超概念は無視されます。バージョン 3.3 では、静的フラグの代わりにコードブロックを使用できるようになりました。バージョン 2021.3.3 では、2 つの新しいオプションが導入されています。

  • 推論ルールは拡張言語で定義でき、拡張言語の概念に適用できます。

  • オーバーライドフラグは、拡張言語のそのような推論ルールに対して機能します。これにより、ルールは、スーパーコンセプトに対して定義されたすべてのルールと、特定の概念に対して拡張言語で定義されたルールをオーバーライドします。

また、拡張中の言語で同じ概念に対して推論ルールが定義されている状況もカバーしています。この場合、これらの元のルールも無視されます。

ノード属性のインスタンスに適用できる推論ルールには、属性付きノードに適用されるルールを修正できる追加機能があります。これらは、属性付きノードの推論ルールと一緒に適用することも、完全に置き換えることもできます。たとえば、これを使用して、プロジェクトまたはシステムレベルで指定されたパラメーターを考慮できる、存在条件に基づく代替型推論を実装できます。

推論規則がノード属性に適用可能である場合、この規則 supercedes 属性付きノードに適用可能な規則であるとタイプチェッカに伝える可能性もあり、無視されます。また、属性付きノードは、attributedNode として、すべてのルールのコードブロック内でアクセス可能です。

推論方法

重複を避けるために、いくつかの推論規則のコードの同一部分をメソッドに抽出することをお勧めします。推論メソッドは、アノテーション "@InferenceMethod" でマークされた単なる基本言語メソッドです。推論規則、置換規則、推論方法の中でのみ使用できる言語構成がいくつかあります。具体的なステートメント、型変数の宣言と型変数の参照、推論メソッドの呼び出しの場合は、typeof 式、方程式と不等式です。これは、そのような構造を任意のメソッドで使用しないために行われます。任意のメソッドは、型チェック中ではなく、任意のコンテキストで呼び出すことができます。

方程式と不等式

型システムエンジンによって実行される主なプロセスは、すべてのタイプの間で方程式と不等式を解くプロセスです。言語設計者は、推論規則で書くことによってどの方程式を解くべきかをエンジンに伝えます。エンジンに方程式を追加するには、次のステートメントを使用します。

expr1 :==: expr2 ここで、expr1 と expr2 は式であり、ノードに評価されます。

次のユースケースを考えてください。ローカル変数参照の型は、それが指す変数宣言の型と同じであると言いたいです。それで、typeof (varRef) :==: typeof (varRef.localVariableDeclaration) を書き、すべてです。型システムエンジンはそのような方程式を自動的に解きます。

上記の式 typeof(expr) （expr は MPS ノードに評価される必要があります）は、そのノードの型として機能する、いわゆる型変数を返す言語構造です。型変数は、方程式を解く過程で徐々に具体的な型になります。

特定の状況では、特定の型が別の型と完全に一致する必要はなく、その型のサブ型またはスーパー型である可能性があると言いたい場合があります。たとえば、メソッド呼び出しの実パラメーターの型は、必ずしもそのメソッドの仮パラメーターの型と同じ型である必要はありません - サブ型にすることもできます。例: パラメーターとして Object を必要とするメソッドは、String にも適用できます。

このような制約を表現するには、方程式の代わりに不等式を使用することができます。不等式は、ある型が別の型のサブタイプである必要があるという事実を表現します。次のように記述されます: expr1 :<=: expr2

弱くて強いサブタイピング

サブ型の関係は、いくつかの異なる場合に役立ちます。実パラメーターの型を仮パラメーター型のサブ型にするか、割り当て値の型を変数の宣言型のサブ型にする必要があります。メソッド呼び出しやフィールドアクセス操作では、オペランドの型をメソッドの宣言クラスのサブ型にする必要があります。

そのような要求はやや物議を醸すことがあります。たとえば、int と Integer の 2 つの型を考えてみましょう。これらの型のパラメーターをメソッドに渡すときに交換可能にします。メソッドが doSomething（int i）の場合、doSomething（1）および doSomething（new Integer（1））を呼び出します。ただし、これらの型をメソッド呼び出しなどのオペランドの型として使用する場合は、状況が異なります。たとえば、整数定数など、int 型の式のメソッドを呼び出すことはできません。 したがって、ある意味では int と Integer は相互のサブ型であり、別の意味ではそうではないと結論付ける必要があります。

そのような論争を解決するために、サブタイプの 2 つの関係、すなわち弱いサブタイプと強いサブタイプを紹介します。弱いサブタイプは強いサブタイプあるノードが別のノードの強いサブタイプであれば、また弱いサブタイプですから続きます。

それでは、この例について、int と Integer は互いに弱いサブタイプだが、強いサブタイプではないと言うことができます。代入とパラメーターの受け渡しには弱いサブ型化のみが必要で、メソッド呼び出しには強いサブ型化が必要です

型システムに不等式を作成するときは、それを強いまたは弱い不等式にすることを選択できます。また、サブタイプルール、つまりサブタイプの関係を示すルール（下記参照）は、弱いものでも強いものでもかまいません。弱い不等式は :<=: のように見え、強い不等式は :<<=: のように見えます。

ほとんどの場合、強いサブタイプを述べ、弱いサブタイプをチェックします。どのサブタイプが必要か分からない場合は、不等式に弱いものを、サブタイプ規則に強いものを使ってください。

サブタイプ規則

型システムエンジンが不等式を解くときには、型が別の型のサブタイプかどうかについての情報が必要です。しかし、型システムエンジンはそれをどのように認識しているためしょうか。それはサブタイプ規則を使います。サブタイプ規則は、タイプ間のサブタイプ関係を表すために使用されます。実際、サブタイプ規則は、型が与えられるとその直接のスーパータイプを返す関数です。

サブタイプ規則は、条件（概念参照またはパターンのいずれか）と、ノードを計算して戻すステートメントのリスト、または指定されたノードの直接のスーパータイプであるノードのリストである本体から構成されます。あるタイプ A が別のタイプ B のスーパータイプであるかどうかをチェックするとき、型システムエンジンはサブタイプ規則を B に適用してその直接のスーパータイプを計算し、次にそれらのスーパータイプにサブタイプ規則を適用します。タイプ A がタイプ B の計算されたスーパータイプに含まれている場合、答えは "yes" です。

デフォルトでは、サブタイピング規則で述べられているサブタイプは強力なものです。弱いサブタイプ化だけを述べたい場合は、ルールの「弱い」プロパティを「true」に設定します。

比較不等式および比較規則

EqualsExpression（Java、BaseLanguage およびいくつかの他の言語の演算子 ==）のためのルールを記述したい考えてみましょう: 左オペランドと EqualsExpression の右オペランドが同等になりたい、それが左オペランドのいずれかのタイプである（非する必要があります。strict）右オペランドのサブタイプ、またはその逆。これを表現するには、比較不等式を expr1: 〜: expr2 の形式で記述します。ここで、expr1 と expr2 は、型を表す式です。expr1 が expr2 のサブタイプである場合、このような不等式は満たされます。

( expr1 <: expr2 )

または

expr2 <: expr1

次に、たとえば、Java インターフェースは、そのようなインターフェースが互いにサブ型でなくても、比較可能でなければならないことを考慮してください。これは、両方のインターフェースを実装するクラスを常に作成できるため、インターフェース型の変数に同じノードを含めることができ、インターフェース型の変数を他のインターフェースにキャストできるためです。両方の型がインターフェース型である方程式、キャスト、または instanceof 式は合法である必要があります（たとえば、Java では合法です）。

サブタイプの関係から生じない、このような比較可能性を述べるには、比較規則を使用する必要があります。比較規則は、2 つの適用可能な型に対する 2 つの条件と、型が比較可能であれば true を返し、そうでなければ false を返します。

これがインターフェース型の比較規則です。

比較規則 interfaces_are_comparable

applicable for concept = ClassifierType as classifierType1 , concept = ClassifierType as classifierType2 applicable always overrides false rule { if (classifierType1.classifier.isInstanceOf(Interface) && classifierType2.classifier.isInstanceOf(Interface)) { return true; } else { return false; } }

引用符

引用は、必要な構造を持つノードを簡単に作成できるようにする言語構造です。もちろん、smodelLanguage を使用してノードを作成し、同じ smodelLanguage を使用して、適切な子、プロパティ、参照を手動で入力することができます。ただし、これを実現するためのより簡単で視覚的な方法があります。

引用は式であり、その値は引用内に記述された MPS ノードです。引用は「ノードリテラル」、つまり数値定数や文字列リテラルに似た構造であると考えてください。つまり、意味する値が静的にわかっている場合はリテラルを記述します。引用内にはノードに評価される式を記述するのではなく、ノード自体を記述します。たとえば、式 2 + 3 は 5 に評価され、式 < 2 + 3 > (山括弧は引用符の括弧) はノード PlusExpression に評価され、leftOperand は IntegerConstant 3、rightOperand は IntegerConstant 5 になります。

（引用語句、反引用符、軽い引用符の詳細については、引用符のドキュメントを参照してください）

反引用符

それはリテラルなので、引用符の値は静的に知るべきです。一方、ノードの一部（子、参照先、プロパティ）だけを動的に知っている場合、つまり実行時にしか評価できず、設計時にはわからない部分は、使用できません。そのような部分を含むノードを作成するための単なる引用です。

ただし、ノードの大部分を静的に知っていて、動的に評価されたノードでいくつかの部分だけを置き換えたい場合は、引用符を使用できます。アンチクォーテーションには、子 、参照、プロパティ、リストのアンチクォーテーションの 4 つのタイプがあります。それらはすべて、引用されたノードの一部をその結果で置き換えるために動的に評価される式を含んでいます。子と指示対象の反引用はノードに評価され、プロパティの反引用は文字列に評価され、リストの反引用はノードのリストに評価されます。

たとえば、ArrayList クラスを使用して ClassifierType を作成したいが、その型パラメーターは、たとえば「computeMyTypeParameter()」メソッドを呼び出すことによってのみ動的に認識されます。

次の式を記述します: <ArrayList <%（computeMyTypeParameter()）%>>。ここでの構文 %（...）% は、ノードの逆引用です。

また、それぞれ ^（...）^ と $（...）$ を使用して、参照ターゲットとプロパティ値を引用符で囲むこともできます。または、*（...）* を使用した 1 つのロールの子のリスト。

a）引用符で囲まれたノード内のどこかにあるノードを式で評価されたノードに置き換える場合は、ノードの引用符を使用します。つまり、%()% です。ご想像のとおり、引用符で囲まれたノード全体を内部で式を含む引用符で置き換えることは意味がありません。そのような場合は、代わりにそのような式をプログラムに直接記述することができます。

ノードの逆引用符は、引用符で囲まれたノードの子、孫、ひ孫、その他の子孫を置き換えるために使用されます。逆引用符内の式はノードを返す必要があります。このような逆引用符を記述するには、子のセル内にキャレットを置き、「%」と入力します。

b) 引用符で囲まれたノード内のどこかからの参照先を、式によって評価されたノードに置き換える場合は、参照の逆引用符、つまり ^(...)^ を使用します。このような逆引用符を記述するには、参照先のセル内にキャレットを置き、「^」と入力します。

c) 複数の基数ロールを持つ子 (またはより深く位置する子孫) を置き換えたい場合、およびその理由から、単一のノードではなく複数のノードで置き換えたい場合は、子リスト (簡潔にするために単にリスト) の逆引用符、*( )* を使用します。リスト逆引用符内の式は、nlist<..> 型または互換性のある型 (つまり、list<node<..>> も、その他の型も OK) のノードのリストを返す必要があります。このような逆引用符を記述するには、子コレクション内の子のセルにキャレットを置き、「*」と入力します。空の子コレクションで使用することはできないため、「*」を押す前に、その中に単一の子を入力する必要があります。

d) 引用符で囲まれたノードのプロパティ値を動的に計算された値に置き換える場合は、プロパティの逆引用符 $()$ を使用します。引用符内の式は文字列を返す必要があり、この文字列が引用符で囲まれたノードの逆引用符で囲まれたプロパティの値になります。このような逆引用符を記述するには、プロパティのセル内にキャレットを置き、「$」と入力します。

（引用語句、反引用符、軽い引用符の詳細については、引用符のドキュメントを参照してください）

推論規則の例

推論規則の最も簡単な基本的な使用例は次のとおりです。

  • 概念のすべてのインスタンスに同じ型を割り当てる（主にリテラルに役立ちます）。

    applicable to concept = StringLiteral as nodeToCheck { typeof (nodeToCheck) :==: <String> }

  • 宣言の型とそれへの参照を同等にします（たとえば、変数とその使用箇所の場合）。

    applicable to concept = VariableReference as nodeToCheck { typeof (nodeToCheck) :==: typeof (nodeToCheck.variableDeclaration) }

  • 型アノテーションを付けてノードに型を与えるには（たとえば、変数宣言の型）:

    applicable to concept = VariableDeclaration as nodeToCheck { typeof (nodeToCheck) :==: nodeToCheck.type }

  • 特定のノードの型に対する制限を設定するために使用します。メソッドの実パラメーター、型変数の初期化子、代入の右側部分などに役立ちます。

    applicable to concept = AssignmentExpression as nodeToCheck { typeof (nodeToCheck.rValue) :<=: typeof (nodeToCheck.lValue) }

型変数

型評価中の型システムエンジン内部では、型は具象型（ノード）またはいわゆる型変数のどちらかです。また、子として子孫として子孫を持つか、それ以上の子孫として子孫を持つノードである可能性があります。型変数は未定義型を表し、この型変数を含む方程式を解いた結果、具体型になることがあります。

型変数は主に "typeof" 操作の結果として実行時に表示されますが、必要に応じて手動で作成することもできます。これを行うには、型システム言語に TypeVarDeclaration というステートメントがあります。「var T」や「var X」や「var V」のように記述します。つまり、「var」の後に型変数の名前が続きます。次に、たとえば引用符で変数を使用して、内部に型変数を含むノードを作成できます。

例: "for each" ループの推論規則。Java の "for each" ループは、ループ本体、反復する反復可能オブジェクト、次の反復の前に反復可能オブジェクトの次のメンバーが割り当てられる変数で構成されます。反復可能オブジェクトは、Iterable インターフェースのサブクラスのインスタンスか、配列のいずれかである必要があります。例を簡略化するために、反復可能オブジェクトが配列である場合は考慮しません。次のことを表現する必要があります。反復可能オブジェクトの型は、何かの Iterable のサブ型である必要があり、変数の型は、まさにその何かのスーパー型である必要があります。たとえば、次のように記述できます。

for (String s : new ArrayList<String>(...)) { ... }

また

for (Object o : new ArrayList<String>(...)) { ... }

上記の両方の例の Iterable は、Iterable <String> のサブ型である型 ArrayList <String> を持っています。変数の型はそれぞれ String と Object で、どちらも String のサブ型です。

ご覧のとおり、反復可能オブジェクトの型は何かの反復可能オブジェクトのサブ型である必要があり、変数の型はまさにその何かのスーパー型である必要があります。しかし、型システム言語で「まさにその何か」をどのように表現するのでしょうか。答えは、反復可能オブジェクトの型と変数の型の間のリンクを表現するために使用する型変数です。そのため、次の推論規則を記述します。

applicable for concept = ForeachStatement as nodeToCheck { var T; typeof(nodeToCheck.iterable) :<=: Iterable < %( T )% >; typeof(nodeToCheck.variable) :>=: T; }

ミートとジョインの種類

Meet 型と Join 型は特殊な型であり、型システムエンジンによって異なる方法で処理されます。技術的には、Meet 型と Join 型はそれぞれ MeetType と JoinType の概念のインスタンスです。これらの型には任意の数の引数型があり、任意のノードである可能性があります。意味的には、Join 型はすべての引数のスーパー型である型であり、Join(T1|T2|..Tn) 型を持つノードは、T1 型、T2 型、または ... または Tn 型を持つものと見なすことができます。Meet 型はすべての引数のサブ型である型であるため、Meet(T1&T2&..&Tn) 型を持つノードは、T1 型、T2 型、... 型 Tn 型に存在すると言えます。Join 型と Meet 型の引数の区切り文字 (つまり "| "と"&") は、それぞれニーモニックとして機能するように選択されます。

ミートアンドジョインタイプは、特定の状況で非常に役立ちます。ミートタイプは、MPS BaseLanguage （Java に非常に近い）でも表示されます。たとえば、そのような式のタイプは次のとおりです。

true ? new Integer(1) : "hello"

これは Meet(Serializable & Comparable) です。Integer (new Integer(1) の型) と String ("hello" の型) の両方が Serializable と Comparable の両方を実装しているためです。

結合タイプは、たとえば、2 つの異なるタイプ（ノードまたはノードのリストなど）の関数のような概念の戻り値が必要な場合に役立ちます。次に、その呼び出しのタイプを Join（node <> | list <node <>>）にする必要があります。

必要に応じて、Meet および Join タイプを自分で作成できます。他のタイプや他のノードと同様に、引用符を使用して作成します。上で記述されていたように、Meet および Join タイプの概念は MeetType および JoinType です。

"when concrete" ブロック

場合によっては、特定の型について方程式や不等式を記述するだけでなく、型構造を使用して複雑な分析を実行したいことがあります。つまり、具体的な型の内部構造を調べます。その子、子の子、指示対象など。

ただ typeof（何らかの表現）を書いてからこの型を分析しているように見えるかもしれません。しかし、問題は、"typeof" 式の結果をその時点では型変数になる可能性があるため、インスペクションできないことです。型変数は通常、ある時点で具象型になりますが、型システムコードの特定の点で具体的であることは保証できません。

このような問題を解決するために、"when concrete" ブロックを使用できます。

when concrete ( expr as var ) { body }

ここで、「expr」は、インスペクションしたい単なる型（インスペクションしたいノード型ではない）に評価される式であり、「var」は式が割り当てられる変数です。次に、この変数を「when concrete」ブロックの本体内で使用できます。本体は、「expr」で示される型が具象になった場合にのみ実行されるステートメントのリストです。when concrete ブロックの本体内では、必要に応じてその子、プロパティなどを安全にインスペクションできます。

具体的なブロックを作成してそのインスペクタを調べると、「浅い」と「エラーをスキップ」という 2 つの選択肢があります。"is shallow" を "true" に設定すると、式が浅く具体化したとき、つまり具象変数そのものではなく、子または参照先として型変数を持つ可能性があるときに、具象ブロックの本体が実行されます。通常、具象ブロックが具象化されていないという条件の表現であれば、エラーが報告されます。式で示された型が具体的な型にならないのが普通の場合は、"skip error" を true に設定することでそのようなエラー報告を無効にすることができます。

オーバーロードされた演算子

演算子（+、- など）は、異なる値に適用されたときに異なるセマンティクスを持つ場合があります。例: Java の + は、数値に適用される場合の加算を意味し、オペランドの 1 つが String 型の場合は文字列の連結を意味します。演算子のセマンティクスがそのオペランドのタイプに依存する場合、演算子のオーバーロードと呼ばれます。実際、同じ構文構造で示される多くの異なる演算子があります。

プラス式の推論規則を書いてみましょう。まず、オペランドのタイプを調べる必要があります。オペランドのタイプ（数値または文字列）がわからない場合、演算のタイプを選択できないためです（数値または文字列のいずれかになります）。オペランドのタイプが具体的であることを確認するために、コードを 2 つの具体的なブロックで囲みます。1 つは左のオペランドのタイプ用で、もう 1 つは右のオペランドのタイプ用です。

when concrete(typeof(plusExpression.leftExpression) as leftType) { when concrete(typeof(plusExpression.rightExpression) as rightType) { ... }

}

次に、いくつかのインスペクションを記述して、タイプが文字列か数値かを確認し、適切なタイプの操作を選択します。ただし、ここで問題が発生します。誰かが BaseLanguage の拡張を記述し、行列や日付などの他のエンティティを追加するためにプラス式を使用したい場合、プラス式は、既存の推論規則にハードコードされています。言語開発者が既存の二項演算をオーバーロードできるようにするための拡張ポイントが必要です。

型システム言語はそのような拡張ポイントを持っています。それは構成されています:

  • 運用ルールのオーバーロード

  • 操作ごとの操作の種類とそのオペランドの種類を提供する構文。

次のようにたとえば、BaseLanguage で PlusExpression のためのルールが書かれています:

when concrete(typeof(plusExpression.leftExpression) as leftType) { when concrete(typeof(plusExpression.rightExpression) as rightType) { node<> opType = operation type( plusExpression , leftType , rightType ); if (opType.isNotNull) { typeof(plusExpression) :==: opType; } else { error "+ can't be applied to these operands" -> plusExpression; } } }

ここで、「演算種別」とは、演算の左オペランドの種別、右オペランドの種別、演算そのものに応じて演算の種別を提供する構成体です。このような目的のために、オーバーロード操作ルールを使用します。

オーバーロード操作ルール

オーバーロードされた操作ルールは、概念 OverloadedOpRulesContainer のルートノード内にあります。オーバーロードされた各操作ルールは、次のもので構成されます。

  • 適用可能な操作の概念、つまり、ルールが適用可能な操作の概念への参照（例: PlusExpression）。

  • 左右のオペランド型の制限。それぞれ左右のオペランドの型を制限する型を含みます。制限は厳密でもそうでなくてもかまいません。つまり、そのようなものに適用可能な規則では、オペランドの型は厳密に制限内の型、または厳密でない場合はそのサブタイプになります。オペランド型

  • この関数は、操作の概念と左右のオペランドの型を知っている操作の型を返します。

ここで BaseLanguage に PlusExpression ための運用ルールをオーバーロードの 1 の例を示します。

operation concept: PlusExpression left operand type: <Numeric>.descriptor is exact: false right operand type: <Numeric>.descriptor is exact: false operation type: (operation, leftOperandType, rightOperandType)->node< > { if (leftOperandType.isInstanceOf(NullType) || rightOperandType.isInstanceOf(NullType)) { return null; } else { return Queries.getBinaryOperationType(leftOperandType, rightOperandType); } }

交換ルール

目的

次のユースケースを考えてみましょう。たとえば、（a 1、a 2、... a N）-> r のように、自分の言語で関数の型があります。ここで、a 1、a 2、..、N、および r は型です。: K は K 番目の関数引数の型であり、r は関数の結果の型です。次に、関数型は戻り型によって共変であり、引数型によって反変であると言いたいと思います。つまり、関数型 F =（T 1、..、T N）-> R は、関数型 G =（S 1、..、S N）-> Q（F <:G と表記）のサブ型です。）R <:Q（戻り値の型による共変）および 1 から N までの任意の K の場合に限り、T K :> S K （つまり、引数の型による反変）。

問題は、型システム言語で共分散と逆分散をどのように表現するかです。サブタイプ規則を使用すると、次のように書くことで共分散を表現できます。

nlist<> result = new nlist<>; for (node<> returnTypeSupertype : immediateSupertypes(functionType.returnType) ) { node <FunctionType> ft = functionType.copy; ft.returnType = returnTypeSupertype; result.add(ft); } return result;

関数の戻り型のためのすべての直接のスーパー型を集めましたそしてそれらの集められた型を戻り型としてそして元の引数型を持つ関数型のリストを作成しました。しかし、最初に戻り型のスーパー型が多数ある場合、不等式を解く必要があるたびにそのようなアクションを実行することはあまり効率的ではありません。次に、関数の戻り型による共分散がありますが関数の引数の型による反変サブ型規則によってサブ型ではなくスーパー型が指定されるため、特定の型の即時サブ型を収集することはできません。

実際、表現したいのは、上記のプロパティです。F = (T 1 , .., T N) -> R <: G = (S 1 , .., S N) -> Q (F <: G と表記) は、R <: Q かつ 1 から N までの任意の K について T K :> S K の場合に限ります。この目的および同様の目的のために、型システム言語には「置換ルール」という概念があります。

置換ルールは、同じ言語または拡張言語のいずれかで定義された、より具体的な別の置換ルールによって上書きできます。特定の左型と右型のペアに適用できる候補置換ルールが 2 つある場合、左型または右型のどちらかに対してより具体的な概念で指定されたルールが優先されます。さらに、2 つ以上のルールが一致し、すべてがまったく同じ概念を指定している場合、より具体的な言語で定義されたルールが優先されます。「上書き」条件は、特定の右型と左型の概念の組み合わせに対してルールが選択される前にチェックされ、デフォルトでは false と定義されています。true の場合、より具体的な一致条件に該当するすべてのルールは適用範囲から除外されます。

交換規則は何ですか？

置換規則は、不等式を解決するための便利な方法を提供します。標準的な方法では、スーパータイプが結果に含まれる（または結果に含まれない）までサブタイプ規則を推移的にサブタイプに適用しますが、不等式に適用できる場合は置換ルールを削除します。不等式を実行してから、その本体（通常は "create Equation" および "create inequation" ステートメントを含む）を実行します。

置換ルールの適用性は、以下に基づいて決定されます。

  • 適用可能なセクションでは、2 つの概念間の一致するサブタイプ関係を定義します。

  • カスタム条件セクション。これは、処理される 2 つのタイプから適用性を任意に計算するブール関数です。

  • オーバーライドフラグ。これにより、ルールはサブコンセプトに定義されたルールをオーバーライドできます。true の場合、あまり具体的でない一致条件に対応するすべてのルールは適用範囲から除外されます。

サンプル

上記の例の置換規則は次のように書かれています。

replacement rule FunctionType_subtypeOf_FunctionType applicable for concept = FunctionType as functionSubType <: concept = FunctionType as functionSuperType custom condition: true overrides: false rule { if (functionSubType.parameterType.count != functionSuperType.parameterType.count) { error " different parameter numbers " -> equationInfo.getNodeWithError(); return; } functionSubType.returnType :<=: functionSuperType.returnType; foreach (node<> paramType1 : functionSubType.parameterType; node<> paramType2 : functionSuperType.parameterType ) { paramType2 :<=: paramType1; } }

ここでは、規則はサブ型でなければならない概念 FunctionType と、スーパー型でなければならない概念 FunctionType に適用可能であると言います。ルールの本体は、関数型のパラメーター型の数が等しいことを確認し、そうでなければエラーを報告して戻ります。両方の関数型のパラメーター型の数が等しい場合、ルールは戻り型と適切なパラメーター型の適切な不等式で不等式を作成します。

置換規則の使用箇所のもう 1 つの単純な例は、Null 型（null リテラルの型）がプリミティブ型を除くすべての型のサブタイプであることを示す規則です。もちろん、すべての型のリストを返す Null 型のためのサブタイプ規則を書くことはできません。代わりに、次の置換規則を書きます。

replacement rule any_type_supertypeof_nulltype applicable for concept = NullType as nullType <: concept = BaseConcept as baseConcept custom condition: true overrides: false rule { if ( baseConcept.isInstanceOf ( PrimitiveType ) ) { error "null type is not a subtype of primitive type " -> equationInfo.getNodeWithError(); } }

この規則は、すべてのスーパータイプおよび Null タイプのサブタイプに適用可能です。この規則がする唯一のことは、あるべきスーパータイプが PrimitiveType 概念のインスタンスであるかどうかをチェックすることです。そうである場合、ルールはエラーを報告します。そうでなければ、ルールは何もしないため、解決するための不等式は単に型システムエンジンから削除され、それ以上の効果はありません。

異なる意味

置換規則の意味は、上で説明したように、不等式を他の式や不等式に置き換えるか、適用したときに他のアクションを実行することです。この意味論は、特定の型がある条件下で別の型のサブタイプであることを実際には述べていません。それはこれら二つのタイプの不等式をどのように解くかを定義するだけです。

例: 生成中に、静的に未知のタイプが String のサブタイプかどうかを調べる必要があるとします。インスペクションする型が Null 型の場合、エンジンはどのように答えますか。不等式があるとき、置き換え規則はそれが真実であると言うことができますが、この場合その上で述べられた意味論は役に立たないです: 不等式がない、イエスかノーと答える質問をします。関数型の場合は、いくつかの不等式を作成する必要があるとルールに記載されているため、さらに悪くなります。それでは、私たちのユースケースでどう扱うべきでしょうか。

ある型が別の型のサブタイプであるかどうかを調べたいときに置換規則を使用可能にするために、そのような場合には置換規則に異なる意味が与えられます。

この意味は次のとおりです。各「式の追加」ステートメントは、2 つのノードが一致するかどうかのインスペクションとして扱われます。各「不等式の追加」ステートメントは、あるノードが別のノードのサブタイプであるかどうかのインスペクションとして扱われます。各レポートエラーステートメントは「return false」として扱われます。

関数型に関する上記の置換規則を考えてください。

replacement rule FunctionType_subtypeOf_FunctionType applicable for concept = FunctionType as functionSubType <: concept = FunctionType as functionSuperType custom condition: true overrides: false rule { if (functionSubType.parameterType.count != functionSuperType.parameterType.count) { error " different parameter numbers " -> equationInfo.getNodeWithError(); return; } functionSubType.returnType :<=: functionSuperType.returnType; foreach (node<> paramType1 : functionSubType.parameterType; node<> paramType2 : functionSuperType.parameterType ) { paramType2 :<=: paramType1; } }

別の意味では、次のように扱われます。

boolean result = true; if ( functionSubType.parameterType.count != functionSuperType.parameterType.count ) { result = false; return result; } result = result && isSubtype( functionSubType.returnType <: functionSuperType.returnType ); foreach ( node<> paramType1 : functionSubType.parameterType; node<> paramType2 : functionSuperType.parameterType ) { result = result && isSubtype (paramType2 <: paramType1); } return result;

それで、見ることができるように、他の意味論は方程式 / 不等式を作成することとインスペクションを実行することの間のかなり直観的なマッピングです。

型システム、トレース

MPS は、型システムエンジンが特定の問題に関する型システムルールを評価し、型を計算する方法についてのインサイトを提供する便利なデバッグツールを提供します。コンテキストメニューから、またはキーボードショートカットの Control/Cmd + Shift + X で呼び出します。

TST2.png

コンソールには 2 つのパネルがあります。左側のものは適用された順序または規則を示し、右側のものは左側のパネルで選択された規則を評価するときの型システムエンジンの作業メモリのスナップショットを示します。

TST1.png

タイプエラーは、Type-system Trace パネル内に赤い色でマークされています。

TST3.png

さらに、コードでエラーを見つけた場合は、Control + Alt + クリック /Cmd + Alt + クリックを使用して、タイプの検証に失敗したルールにすばやく移動します。

TST4.png
TST5.png

型システム言語の高度な機能

デフォルトタイプノードの置き換え

方程式を適用したり不等式を解いたりした結果として type がプログラムノードに割り当てられると、type を表すノードはデフォルトでそのままとされます。つまり、プログラム内のノードであるか、引用付きで作成されている可能性があります。どちらの場合も、式または不等式ステートメントのいずれかによって割り当てられるタイプを指定する式を評価した結果は、文字通りターゲットタイプを表します。この機能により、代わりに別のノードを使用してタイプを表すことができます。

例: タスクが 1 つのタイプを使用するのか別のタイプを使用するのかに応じて、int または long を使用するなど、プログラム構成ごとに異なるタイプを使用することを決定する場合があります。これは、タイプチェックの実行時に置換が行われるため、単純にジェネレーターを使用して正しい「実装」タイプを生成するのとは異なるため、発生する可能性のあるエラーを早期に発見できます。

最も単純な形式では、型システムモデルで Substitute Type Rule のインスタンスを作成することによって型置換を使用できます。

substitute type rule substituteType_MyType { applicable for concept = MyType as mt substitute { if (mt.isConditionSatisfied()) { return new node<IntegerType>; } return null; } }

Substitute Type Rule は型を表すノードに適用可能です。タイプチェッカによって新しい型が導入されるときはいつでも、適切な代入規則を検索して実行します。この規則は、置換として `node <>` のインスタンス、または null 値を返さなければなりません。その場合、元のノードが型を表すのに使われます（デフォルトの振る舞い）。

タイプチェッカーによって使用される型をオーバーライドするもう 1 つの可能性は、ノード属性の使用にあります。元のタイプノードに含まれるノード属性がある場合、タイプチェッカーは最初にその属性に適用可能な代替タイプルールを見つけようとします。このようにして、言語が実装されていても型ノードを上書きすることができます。

substitute type rule substituteType_SubstituteAnnotation { applicable for concept = SubstituteAnnotation as substituteAnnotation substitute { if (substituteAnnotation.condition.isSatisfied(attributedNode)) { return substituteAnnotation.substitute; } return null; } }

上記のルールは属性ノードに対して定義されており、明示的なパラメーターとしてルールに渡されるのは属性ノードです。この規則は、型ノードを置換するための条件が満たされているかどうかをチェックでき、attributedNode 式を介して元の型を表す属性付きノードにもアクセスできます。

メンションすべき 1 つの注意点は、置換ルールから返されたばかりの型ノードが、それ自体が別の置換の対象である場合に関するものです。タイプチェッカーは、使用可能な置換がなくなるまで、一致するすべての置換ルールを徹底的に適用しようとします。その場合のみ、タイプチェッカーの内部モデルにタイプが表示されます。タイプチェッカーが A-> B-> A のような無限の置換サイクルに入るのを防ぐためにいくつかの予防措置が取られますが、これらは完全ではなく、無限のサイクルを導入しないように注意する必要があります。

チェックのみの不等式

基本的に、不等式はノードの型に影響を与える可能性があります。たとえば、不等式部分の 1 つが型変数の場合、この不等式のために具体的な型になる可能性があります。しかし、時には、そのような不等式が満たされているかどうかを確認するためだけに、型を作成するための特定の不等式を望まないことがあります。そのような不等式をチェックオンリー不等式と呼びます。不等式をチェック専用としてマークするには、この不等式のインスペクタに移動し、"check-only" フラグを "true" に設定する必要があります。このような不等式を視覚的に区別するために、チェック専用の不等式の「小なりまたは等しい」記号は灰色ですが、通常のものは黒です。インスペクタを見なくても不一致がチェック専用かどうかを確認できます。

依存関係

特定の言語用のジェネレーターを書くとき（generator を参照）、ジェネレータークエリで特定のノードの型を尋ねたいと思うかもしれません。generator がモデルを生成するとき、そのような問い合わせは型システムエンジンに必要な型を見つけるために何らかの型検査をさせるでしょう。ノードの型を取得するためにノードの包含ルートを完全に型チェックすることは、コストがかかり、ほとんどの場合不要です。ほとんどの場合、型チェッカーは与えられたノードだけをチェックするべきです。さらに難しい場合には、与えられたノードの型を取得するためには、その親あるいはおそらくさらなる先祖をチェックする必要があります。計算された型が完全に具体的ではない（たとえば、1 つ以上の型変数を含む）場合、型検査エンジンは所与のノードを検査します。その後、型チェッカーはノードの親をチェックします。

さらに複雑な場合があります。単独で計算されている特定のノードのタイプは完全に具体的です。また、同じノードの種類（特定の環境における）も完全に具体的ですが、最初のものとは異なります。そのような場合、上記のアルゴリズムは壊れて、あたかも孤立しているかのようにノードのタイプを返しますが、これは与えられたノードの正しいタイプではありません。

この種の問題を解決するために、タイプチェッカーにいくつかのヒントを与えることができます。そのようなヒントは依存関係と呼ばれます - それらはノードのタイプが他のノードに依存するという事実を表します。生成中に特定のノードのタイプを計算するとき、このノードに依存関係がある場合はそれらもチェックされるため、ノードは適切な環境でタイプチェックされます。依存関係は、ノード上の typeOf 式を使用して表現されます。その型は、要求された型を正しく計算するために必要です。

上書き型のリテラルまたは式

型にのみ適用可能な型置換規則に加えて、推論規則における属性のサポートを紹介します。

推論ルール

リテラルや式には通常、型チェックに問題のノードの型が必要なときにトリガーされる、関連付けられた型推論規則があります。ルールには、サブコンセプトが事前定義済みルールを拡張または上書きできるようにするメカニズムがあります。

rule typeof_IntLiteral { applicable for concept = IntLiteral as nodeToCheck applicable always overrides true do { typeof(nodeToCheck) :==: <integer>; } }

ノード属性の推論規則

ノードに 1 つ以上の属性がある場合、これらの属性に適用可能な推論規則は、ノード自体に適用可能な規則よりも先に適用されます。推論規則を適用するプロセスは、疑似コードで記述できます。

lookup-inference-rules(node) : let skipAttributed = false foreach a in attributesOf(node) do if hasInferenceRuleFor(a) then let rule = getInferenceRuleFor(a) yield rule if isSuperceding(rule) then let skipAttributed = true end if if isOverriding(rule) then break foreach loop end if end if end do if skipAttributed then return end if /* proceed as usual */ end

ノード属性に適用可能な推論規則の使用例は、プレゼンス条件がリテラルの型をどのように変更できるかを示しています。この例では、アノテーション付きリテラルの型は、この推論規則とノードに適用可能な他の推論規則の両方の影響を受けます。

rule typeof_Literal { applicable for concept = PresenceConditionAnnotation as pca applicable always overrides false supercedes attributed false do { typeof(pca.parent) :<=: pca.alternativeNode } }

条件付きオーバーライド型推論

ユーザーが属性を介して型推論をオーバーライドする場合の条件は構成によって異なることに注意してください。常にデフォルトの型をオーバーライドしたくはありません。

rule typeof_Literal { applicable for concept = PresenceConditionAnnotation as pea applicable always supercedes attributed { isConditionSatisfied(pca); } do { typeof(attributedNode) :==: pca.replacementType } }

チェックルール

チェック（または非型システム）規則は、コード内の既知のエラーパターンを検索するモデルを調べて、ユーザーに報告します。この種のコンパイル前コードインスペクションは、一般に静的コード分析として知られています。静的コード分析用の一般的なツールのエラーパターンは、正確性の問題、マルチスレッドの正確性、国際化の問題、脆弱性の増大するエラー、スタイルの問題、パフォーマンスの問題など、いくつかのカテゴリに分類できます。対話型レポートによるオンデマンド

Checking1.png

カラフルなシンボルとコードの下線を使用して、エディター内で直接またはオンザフライモードで直接実行できます。

Checking3.png

重大度

MPS は重大度によって問題を区別します。

  • エラー - 赤で表示

  • 警告 - 黄色で表示

  • 情報 - 灰色がかった表示

jetbrains.mps.lang.typesystem 言語は、これらの問題カテゴリを説明とハイライトするノードとともに出力する対応するステートメントを提供します。追加の ensure ステートメントは、条件が満たされない場合にエラーを報告するためのより簡潔な構文をユーザーに提供します。

Checking6.png

通常、チェックルールは、特定のノードまたはモデルのごく一部で 1 つまたはいくつかの関連する問題をチェックし、問題が発見された場合はユーザーに報告します。チェック規則は、具体的な概念に添付されています。

Checking7.png

ルールは、そのコンセプトのインスタンスであるすべてのノードに対して呼び出されます。

ルールの適用可能性は、パターン言語を使用して指定されたパターンに制限できます。これは、主に次の 2 つの理由で便利です。

  • ルールの適用条件を概念の一部の出現箇所のみに絞り込む

  • ノードのプロパティ、子、孫の便利な命名

両方のゴールは、ルールの本体内でパターン言語を使用することによって、特に match ステートメントを使用することによって達成できます。

checking_rule_pattern.png

パターンには、モデル内の任意の値、ノード、参照と一致する可変部分（ノード、プロパティ、参照）を含めることができ、ユーザーは変数名を使用して参照できます。

チェックルールのオーバーライドオプションは、現在のルールがノードに適用可能な他のチェックルールをオーバーライドするかどうかを定義します。

Checking7a.png

一部の概念に対して定義されたチェックルールは、デフォルトでそのすべてのサブ概念に継承されます。ノードのチェックには、ノードの概念に対して定義されたすべてのルールと、そのスーパーコンセプトに対して定義されたルールの実行が含まれます。このようなチェックルールの継承を回避する必要がある非常にまれな状況では、オーバーライドオプションがその手段を提供します。オーバーライドするルールのリストを明示的に指定できます。

複数のオーバーライドされたルールを選択できます。

Checking7b.png

パターン言語

パターン言語により、ユーザーは目的のパターンを指定するための妥当な柔軟性を得ることができます。インテンションを使用すると、パターンのさまざまな部分にパターン固有の属性を付けてアノテーションを付けることができるため、特別な意味を持たせることができます。

  • パターン変数 - ノードまたはパターンの参照を変数に変換するために使用できます。それは与えられた位置のどんな値とも一致し、ユーザーはパターン変数を参照することによって値を得ることができるでしょう

  • パターンプロパティ変数 - 上記と同じですが、ノードのプロパティに適用されます。

  • リストパターン - ノードのコレクションと一致し、ユーザーが繰り返し処理できるようにします。

  • or パターン - 提供されたいくつかのサブパターンの 1 つと一致します

  • ワイルドカード - 指定された位置にある（存在しない場合でも）ノードと一致します。ユーザーは一致した値を参照できません

match ステートメントを使用して、BaseLanguage コードからノードマッチングを呼び出すことができます。

Pattern3.png

クイックフィックス

クイックフィックスは、報告された問題を自動的に排除する単一のモデル変換関数を提供します。

Checking5.png

クイックフィックス は、apply が true にすぐに設定されている呼び出し元からのみ参照される場合を除き、インテンションコンテキストメニューでそれを表す説明を提供する必要があります。クイックフィックスは、再利用された値を保持するためにフィールドを宣言することもでき、呼び出し元からの引数を受け入れることができます。

クイックフィックスの呼び出し

クイックフィックスは、インテンションを使用してインスペクターツールウィンドウを介して報告された各問題に関連付けることができます。

Checking4.png

通常、ユーザーは Alt+Enter キーショートカットを押した後に表示されるインテンションコンテキストメニューからクイックフィックスを呼び出します。ただし、すぐに適用フラグが設定されている場合、MPS は、ユーザーのトリガーを待たずに、オンザフライ分析中に問題が発見されるとすぐに、関連するクイックフィックスを実行します。

Checking8.png

インスペクターを通して設定された他の 2 つのオプションのプロパティはそれほど頻繁には必要とされません:

  • ハイライトするノード機能 - ノード全体をハイライトするのではなく、問題の原因としてハイライトするノードのプロパティ、参照の子を指定します。

  • 外部メッセージソース - ユーザーがエディターで報告されたエラーをクリック（Control/Cmd + Alt + クリック）すると、そのエラーを発生させた確認ルールの error/warning/info/ensure コマンドが表示されます。外部メッセージソースプロパティを使用すると、この動作をオーバーライドして、エラーをクリックしたときにユーザーが移動する独自のノードを提供できます。

追加の方法

推論ルールの下部にある追加のメソッドセクション、チェックルールおよびクイックフィックスにより、ユーザーは、繰り返しを避けるために、対応するルートノード内から呼び出すことができるユーティリティメソッドを定義できます。通常、追加のメソッドは、計算を実行したり、定義の複数の場所で必要なタスクを実行したりします。追加のメソッドは、含まれているノード内からのみ表示されるようにプライベートにする必要があります。

行動 Using_typesystem

関連ページ：

クックブック

推論ルール：このクックブックは、言語の型を設計する際の簡単な答えとガイドラインを提供するものです。型システムの詳細な説明については、ユーザーガイドの型システムセクションを参照してください。等価ノードのタイプが常に特定の具体的なタイプである必要がある場合は、タイプ方程式を使用します。typeof コマンドを使用して、目的のノードのタイプが特定のタイプと等しくなければならないことを宣言します。rule typeof_StringLiteral { applicable for concept = S...

Using_typesystem

言語の型システムを定義した場合、タイプチェッカーは自動的にそれをエディターで使用して、開いているノードをエラーと警告でハイライトします。また、エディターアクションやジェネレータークエリなど、クエリの型に関する情報を使用することもできます。ノードの型を使用することも、特定の型が別の型のサブタイプかどうかを知りたいこともあります。または、与えられた形式を持つ型のスーパータイプを見つけたいと思うかもしれません。タイプ操作：type 操作を使用して、クエリでノードのタイプを取得できます。<expr...

引用符

引用は、必要な構造を持つノードを簡単に作成できるようにする言語構造です。もちろん、smodelLanguage を使用してノードを作成し、同じ smodelLanguage を使用して、適切な子、プロパティ、参照を手動で入力することができます。ただし、これを実現するためのより簡単で視覚的な方法があります。2 つの以下の構築物は、最初のものは、第二の計画モデルの API を引用を使用して、同じノードを構築します。node<IntegerType> node = <int>; n...

振る舞い

構文ツリーの操作中に、タスクを簡素化し、機能を再利用するために、一般的な操作がユーティリティメソッドに抽出されることがよくあります。このようなユーティリティを静的メソッドに抽出したり、仮想メソッドでユーティリティコードを保持するノードラッパーを作成したりすることができます。ただし、MPS では、より優れたソリューションである動作言語の側面を利用できます。これにより、ノード上に仮想および非仮想インスタンスメソッド、静的メソッド、コンセプトインスタンスコンストラクターを作成できます。Behavior...