Понимание проблемы. Вывод типа C#, как описано в спецификации языка.

Question

C# language specification описывает вывод типа в разделе §7.5.2. В нем есть детали, которые я не понимаю. Рассмотрим следующий случай:

// declaration 
void Method<T>(T obj, Func<string, T> func); 

// call 
Method("obj", s => (object) s); 

И Microsoft и Mono C# компилятор правильно вывести T = object, но мое понимание алгоритма в спецификации даст T = string, а затем терпят неудачу. Вот как я это понимаю:

Первой фаза

• Если Ei является анонимной функцией, явного типа параметра умозаключение (§7.5.2.7) изготовлен из Ei в Ti

  ⇒ не имеет никакого эффекта, поскольку выражение лямбда не имеет явных типов параметров. Правильно?

• В противном случае, если Ei имеет тип U и xi является параметром значения, то нижний вывод выполнен из U-Ti.

  ⇒ первый параметр имеет статический тип string, поэтому это добавляет string к нижним границам для T, справа?

Вторая фаза

• Все нефиксированной переменные типа Xi, которые не зависят от (§7.5.2.5) любой Xj являются фиксированными (§7.5.2.10).

  ⇒ T нефиксирован; T не зависит ни о чем ... так что T следует исправить, не так ли?

§7.5.2.11 Крепление

• Множество типов кандидатов Uj начинается как совокупность всех типов в наборе оценок для Xi.

  ⇒ {string (нижняя граница)}

• Затем мы рассмотрим каждый связан на Xi, в своей очереди: [...] Для каждого нижней грани U Си всех типов Uj, к которым не существует неявное преобразование из U удаляются из набора кандидатов. [...]

  ⇒ не удаляет что-либо из набора кандидатов, не так ли?

• Если среди оставшихся типов кандидатов Uj существует уникальный тип V, из которого происходит неявное преобразование ко всем другим типам кандидатов, то Xi фиксируется на V.

  ⇒ Поскольку существует только один тип кандидата, это пусто, правда, поэтому Xi зафиксирован на string. Правильно?

---

Итак, где я буду неправильно?

Answer 1

ОБНОВЛЕНИЕ: Мое начальное расследование на автобусе сегодня утром было неполным и неправильным. Текст спецификации первой фазы верен. Реализация верна.

Спецификация ошибочна в том, что на втором этапе порядок событий неверен. Мы должны указать, что мы делаем вывод выходного типа до, мы фиксируем независящие параметры.

Человек, этот материал сложный. Я переписал этот раздел спецификации больше раз, чем я помню.

Я видел эту проблему раньше, и я отчетливо вспоминаю создание ревизий таким образом, что неверный термин «переменная типа» везде заменялся «параметром типа». (Параметры типа не являются местами хранения, содержимое которых может меняться, поэтому нет смысла называть их переменными.) Я думаю, что в то же время я заметил, что порядок был неправильным. Вероятно, случилось то, что мы случайно отправили более старую версию спецификации в Интернете. Много извинений.

Я буду работать с Mads, чтобы обновить спецификацию в соответствии с реализацией. Я считаю, что правильная формулировка второго этапа должна идти что-то вроде этого:

• Если нет нефиксированных параметров типа не существуют, то типа логического вывода успешно.
• В противном случае, если существует один или более аргументов Ei с соответствующего типа параметра Ti такие, что выходного типа Ei с типом Ti содержит, по меньшей мере, один нефиксированной параметр типа Xj и ни один из типов входных ЭИ с тип Ti содержит произвольный параметр типа Xj, , тогда вывод выходного типа производится из всех таких Ei-Ti.

ли не предыдущий шаг на самом деле сделал вывод, мы теперь должны исправить по крайней мере, один параметр, а именно:

• Если существует один или несколько параметров типа Xi такие, что Xi не имеет значения, а Xi имеет непустую набор границ, а Xi не зависит от любого Xj , тогда каждый такой Xi фиксирован. Если какая-либо операция фиксации завершается неудачей, то вывод типа не выполняется.
• В противном случае, если существует один или более параметры типа Xi, такие, что Си является нефиксированным и Сов имеют непустое множество границ, и существует, по крайней мере, один параметр Xj типа, который зависит от Xi то каждое такое Xi фиксировано. Если какая-либо операция фиксации завершается неудачей, то вывод типа не выполняется.
• В противном случае мы не сможем добиться прогресса и есть незафиксированные параметры. Ошибка ввода типа.

Если вывод типа не терпит неудачу или не удастся, повторите вторую фазу.

Идея состоит в том, что мы хотим гарантировать, что алгоритм никогда не переходит в бесконечный цикл. При каждом повторении второй фазы он либо преуспевает, либо терпит неудачу, либо добивается прогресса. Он не может цикл больше времени, чем есть параметры типа для исправления типов.

Спасибо, что привлекли это к моему вниманию.