MPS 2019.2ヘルプ

型システム

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


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

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

型システムとは

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

  • 型エラーを見つける

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

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

  • その他

タイプ

任意のMPSノードがタイプとして機能します。MPSがあなたの言語のノードに型を割り当てることができるようにするには、typesystemのための言語アスペクトを作成するべきです。あなたの言語の型システムモデルは型システム言語で書かれるでしょう。

推論ルール

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

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

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

推論規則は上書きブロックを定義することができます。これは、条件で指定された概念のスーパーコンセプトに適用可能な推論規則が他にある場合、この推論規則が優先されることをタイプチェッカーに伝えるブールフラグです。スーパーコンセプトは無視されます。バージョン3.3では、静的フラグの代わりにコードブロックを使用する機能があります。

バージョン3.3以降、ノード属性のインスタンスに適用可能な推論規則には、属性付きノードに適用された規則を上書きまたは修正することを可能にする追加機能があります。たとえば、これを使用して、プロジェクトまたはシステムレベルで指定されたパラメータを考慮に入れることができるプレゼンス条件に基づく代替型推論を実装できます。

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

推論方法

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

上書き

サブコンセプトの型システムルールは、スーパーコンセプトで定義されたルールを上書きできます。上書きフラグがfalseに設定されている場合、ルールはスーパーコンセプトに定義されているルールとともに概念に適用されているルールのリストに追加され、フラグがtrueに設定されている場合上書きルールは次のルールに置き換わります。ルールエンジンのスーパーコンセプトなので、有効にはなりません。これは推論NonTypeSystemの両方の規則に適用されます。

方程式と不等式

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

expr1 :==: expr2、ここで expr1expr2 は式で、ノードに評価されます

次のユースケースを考えてください。ローカル変数参照の型は、それが指す変数宣言の型と同じであると言いたいです。それで、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型の式のメソッドを呼び出すことはできません。ある意味で intInteger はお互いのサブタイプであるが、他の意味ではそうではないと結論しなければならない。

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

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

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

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

サブタイプ規則

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

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

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

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

EqualsExpression(Java、BaseLanguage、および他のいくつかの言語の演算子 == )のルールを記述したいと考えてください:EqualsExpressionの左オペランドと右オペランドを比較可能にしたい、つまり左オペランドのいずれかのタイプが(非厳密)右オペランドのサブタイプ、またはその逆です。これを表現するには、比較式を expr1 :~: expr2の形式で記述します。ここで、expr1expr2は型を表す式です。 expr1expr2 ( 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 + 35に評価され、式 < 2 + 3 > (角括弧は引用符括弧)はノードプラス式に評価され、leftOperand整数定数3rightOperandIntegerConstant 5です。

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

反引用符

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

ただし、良いニュースは、ノードの大部分を静的に知っていて、いくつかの部分だけを動的に評価されたノードに置き換えたい場合には、引用符を使用できます。反引用符は、4つのタイプ( 参照財産、およびリストの 引用符)にすることができます。それらはすべて式を含み、動的に評価されて、引用されたノードの一部をその結果で置き換えます。子および参照の対引用符はノードに評価され、プロパティー対引用符は文字列に評価され、リスト対引用符はノードのリストに評価されます。

たとえば、配列リストクラスでClassifierTypeを作成したいが、その型パラメータは動的にしか認識されません。たとえば、"computeMyTypeParameter()"などのメソッドを呼び出すことによってわかります。

<ArrayList <%(computeMyTypeParameter())%>>という式を書きます。ここでの構成%(...)%は節の逆引用符です。

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

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

そのため、ノードの引用符は、子供、孫、孫、およびその他の引用ノードの子孫を置き換えるために使用されます。antiquotationの内側の式はノードを返すべきです。そのような引用符を書くには、キャレットを子供用のセルに置き、「%」と入力します。

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

c)複数カーディナリティのロールを持つ子(またはさらに深く位置する子孫)を置き換えたい場合、その理由のためにそれを単一のノードではなくむしろ複数のものと置き換えたい場合は、子リスト(簡潔にするために単にリスト)を使用します。半引用符、*( )* . リストantiquotationの内側の式はノードのリストを返すべきです。それはタイプnlist <..>または互換タイプです(たとえば list <node <.. >>もOKです)。このような引用符を書くには、子コレクション内の子のセルにキャレットを置き、「*」と入力します。空の子コレクションには使用できないため、「*」を押す前に、その中に1人の子を入力する必要があります。

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

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

推論規則の例

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

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

    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>(...)) { ... }

上記の両方の例のイテラブルは、反復可能な<String>のサブタイプであるタイプArrayList <文字列>を持ちます。変数のタイプはそれぞれ文字列オブジェクトで、どちらも文字列のサブタイプです。

見てのとおり、イテラブルの型は何かのIterableのサブタイプでなければならず、変数の型はまさしくその何かのスーパータイプであるべきです。しかし、どうやって型システム言語で「そんなこと」を言うのでしょうか。答えは、それがイテラブルの型と変数の型の間のリンクを表現するために使う型変数です。そこで、以下の推論規則を書きます。

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

ミートとジョインの種類

ミート型と結合型は特殊な型で、型システムエンジンでは扱いが異なります。技術的にはミート結合型は、それぞれMeetTypeJoinTypeの概念のインスタンスです。それらは任意の数の引数型を持つことができます。意味的には、結合型はそのすべての引数のスーパータイプである型であり、Join(T1|T2|..Tn)型を持つノードは、それがT1型またはT2型...またはTn型を持っているかのように見なすことができます。ミート型はそのすべての引数のサブタイプである型なので、Meet(T1&T2&..&Tn)型を持つノードはT1型とT2型、.. Tn型に属します。結合型およびミート型の引数のセパレータ(たとえば「|」および「&」)は、それぞれニーモニックとして機能するように選択されます。

MeetおよびJoinタイプは特定の状況では非常に便利です。ミートタイプはMPS BaseLanguage(Javaに非常に近い)でも表示されます。たとえば、そのような式の型

true ? new Integer(1) : "hello"

Integer(新しい整数(1)の型)と文字列( "hello"の型)の両方がSerializableComparableの両方を実装しているため、Meet(Serializable & Comparable)です。

結合型は、たとえば、2つの異なる型(ノードまたはノードのリストなど)の関数のような概念の戻り値が必要な場合に役立ちます。それからその呼び出しのタイプを結合(ノード<> | list <node <>>)にするべきです。

必要に応じて、ミート型と結合型を自分で作成できます。他のタイプや他のノードと同じように、引用符を使って作成します。ミート型と結合型の概念は、前述のとおりMeetTypeJoinTypeです。

"when concrete" ブロック

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

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

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

when concrete ( expr as var ) { body }

ここで、"expr"はインスペクションしたい単なる (インスペクションしたいノード型ではない)に評価される式で、"var"は式が割り当てられる変数です。そして、この変数は "when concrete"ブロックの本体の中で使われるかもしれません。本体は、"expr"で示される型が具象になったときにのみ実行されるステートメントのリストです。必要な場合は、具象ブロックの本体の内部で、その子、プロパティーなどを安全にインスペクションできます。

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

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

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

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

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

それから、インスペクションを書くことができます。そこで、私たちの型が文字列か数値かどうかをチェックし、適切な型の操作を選びます。しかし、ここで問題があるでしょう。行列や日付など、他のエンティティの追加にプラス表現を使用するBaseLanguageの拡張を誰かが書いた場合、プラス表現を使用することはできません。plus expressionは、既存の推論規則にハードコードされています。そのため、言語開発者が既存のバイナリ演算オーバーロードできるようにするための拡張ポイントが必要です。

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

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

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

たとえば、BaseLanguageプラス式の規則は次のように書かれています。

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のルートノード内にあります。各オーバーロード操作ルールは、次の要素で構成されています。

  • 適用可能な操作の概念、すなわち、規則が適用可能な操作の概念への参照(たとえば、プラス式)。

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

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

BaseLanguageにおけるプラス式のオーバーロード操作ルールの一例です。

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、..、a N、rは型です:a KはK番目の関数引数のタイプであり、rは関数の結果のタイプです。次に、関数の型は戻り値の型によって であり、引数の型によって反変であると言いたいと思います。つまり、関数タイプF =(T 1、..、TN)-> Rは、関数タイプG =(S 1、..、SN)-> Q(F <:Gと表記)のサブタイプです。R <:Q(戻り値の型による共変)および1からNまでのKの場合のみ、TK:> SK(つまり、引数の型による反変)。

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

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、..、TN)-> R <:G =(S 1、..、SN)-> Q(F <:Gと表記) R <:Qで、かつ1からNまでのK、TK:> S Kの場合のみ。型システム言語には、「置換ルール」と呼ばれる概念があります。

交換規則は何ですか?

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

サンプル

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

replacement rule FunctionType_subtypeOf_FunctionType applicable for concept = FunctionType as functionSubType <: concept = FunctionType as functionSuperType 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 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 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 + Shift + X / Cmd + Shift + X)から起動します。

TST2

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

TST1

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

TST3

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

TST4

TST5

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

デフォルトタイプノードの上書き

方程式を適用したり不等式を解いたりした結果として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>; } 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; } 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

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

Checking3

重大度

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

  • エラー - 赤で表示

  • 警告 - 黄色で表示

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

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

Checking6

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

Checking7

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

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

  • ルールの適用条件を概念の一部の出現のみに狭める

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

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

checking rule pattern

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

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

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

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

Checking7b

パターン言語

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

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

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

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

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

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

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

Pattern3

クイックフィックス

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

Checking5

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

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

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

Checking4

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

Checking8

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

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

  • 外部メッセージソース - ユーザがエディターで報告されたエラーをクリックすると(Control/Cmd + Alt + click)、そのエラーを引き起こした確認ルールエラー/警告/情報/確認コマンドが表示されます。外部メッセージソースプロパティーを使用すると、この動作をオーバーライドして、エラーをクリックしたときにユーザーに表示される独自のノードを指定できます。

最終更新日: 2019年8月30日

関連ページ:

クックブック - 型システム

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

Using_typesystem

言語の型システムを定義した場合、タイプチェッカーは自動的にそれをエディターで使用して、開いているノードをエラーと警告で強調表示します。また、エディターアクションやジェネレータクエリなど、クエリの型に関する情報を使用することもできます。ノードの型を使用することも、特定の型が別の型のサブタイプかどうかを...

引用符

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

振る舞い

構文木の操作中、タスクを単純化し機能を再利用するために、一般的な操作がユーティリティメソッドに抽出されることがよくあります。そのようなユーティリティを静的メソッドに抽出したり、仮想メソッド内にユーティリティコードを保持するノードラッパーを作成することが可能です。しかし、MPSではより良い解決策が利用...