Старое неверное в выводе типов

Материал из Вики проекта PascalABC.NET
Версия от 14:22, 7 июля 2014; Mikst (обсуждение | вклад) (Новая страница: «==== Уравнения, порождаемые подстановкой фактических параметров вместо формальных 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 

иначе ошибка