Mikst: Новая страница: «==== Уравнения, порождаемые подстановкой фактических параметров вместо формальных S ↪ T ===…»

2014-07-07T11:22:41Z

Новая страница: «==== Уравнения, порождаемые подстановкой фактических параметров вместо формальных S ↪ T ===…»

Новая страница

==== Уравнения, порождаемые подстановкой фактических параметров вместо формальных S ↪ T ====
Рассмотрим подробно, какие уравнения возникают при подстановке фактических параметров вместо формальных S ↪ T.

Далее X - конкретный тип (класс), T - типовая переменная, V - вектор типовых переменных или конкретных типов, C<V> - обобщенный класс, I - интерфейс (возможно, обобщенный, т.е. I<V>).

Возможны следующие варианты:

*'''I ↪ C<V>'''
*'''I ↪ T'''
*'''I ↪ X'''
Ошибка. Интерфейс нельзя подставить вместо типа

*'''X ↪ C<V>'''
Ошибка. Конкретный тип нельзя подставить вместо обобщенного типа

*'''C<V> ↪ X'''
Это сделать можно если C<V> является наследником конкретного типа X (если контекст Γ содержит ограничение C<V> <: X). Никаких уравнений при этом не генерируется.

*'''X ↪ I<V>'''
Ошибка. Конкретный тип нельзя подставить вместо обобщенного интерфейса

*'''T ↪ C<V>'''
Если в ограничениях where есть T <: C<V> (правильнее говорить - если контекст Γ содержит ограничение T <: C<V>), то просто пропускаем эту подстановку - уравнения при этом не генерируются.
В противном случае - ошибка

*'''C<V> ↪ T'''
Обобщенный класс можно подставить вместо типовой переменной. Это дает новое уравнение
T = C<V>

*'''T ↪ I<V>'''
Если контекст Γ содержит ограничение T <: I<V>, то это дает уравнение
T = I<V>
В противном случае - ошибка

*'''C<V> ↪ I<V1>'''

*'''C<V> ↪ C1<V1>'''
Это возможно в двух ситуациях:

если C<V> <: C1<VV> тогда надо положить
V1 = VV (вектор уравнений).
иначе если C = C1, то
V = V1
иначе - ошибка

*'''I ↪ I1'''
Необходимо проверить, есть ли в контексте I <: I1.
Если нет - ошибка.

*'''I<V> ↪ I1<V1>'''
Если I<V> <: I1<VV> то
V1 = VV
иначе если I = I1, то
V = V1
иначе ошибка

Старое неверное в выводе типов - История изменений

Mikst: Новая страница: «==== Уравнения, порождаемые подстановкой фактических параметров вместо формальных S ↪ T ===…»