Исследования по выводу типа вызовов?

9

Я пытаюсь узнать больше о проверке типов в целых программах и системах вывода типов, которые используют информацию с сайтов вызова функций для вычисления информации о типах (в дополнение к стандартному подходу использования тела функции). Например, такой алгоритм может использовать вызов функции, например, foo(1)чтобы сделать вывод, что функция fooпринимает целочисленные аргументы. Очевидно, это сильно усложнит вывод и сделает проверку немодулярной.

В любом случае, мне не повезло найти какое-либо исследование этого подхода, возможно, потому что я не знаю правильной терминологии, чтобы описать то, о чем я говорю. Есть указатели?

pl.programming-languages type-theory type-inference type-systems Дерек Турн
источник
То, что вы описываете, имеет подсказки двунаправленного вывода типа, если я не ошибаюсь. Однако описание того, что вы пытаетесь сделать, может прояснить ситуацию.
Доминик Маллиган
Вы спрашиваете, потому что вы ищете способ специализировать полиморфные функции?
nponeccop
В основном я просто пытаюсь больше узнать о системах типов, и да, я думал в основном о том, как обрабатывать полиморфные функции (и вызовы методов в ОО-языках, то же самое). Я пытаюсь определить правильные термины для этого, чтобы я мог прочитать об этом.
Дерек Турн

Ответы:

11

Почти все системы с выводом типа используют для этого информацию сайта вызова. Примеры включают в себя Standard ML, OCaml, F # и Haskell. Многие другие языки используют информацию о сайте вызова для определения реализации параметров типа, например Java, C #, Scala и Typed Racket. Это часто называется «Вывод локального типа».

Я бы просто описал то, что вы ищете, как «Вывод типа», и вы, вероятно, должны начать с поиска так называемой системы «Хиндли-Милнера». Википедия страница дает разумное введение и указатели на оригинальные работы.

Начать локальный вывод типов можно с оригинальной статьи Пирса и Тернера, которую лучше всего прочитать в версии TOPLAS 2000 ( ACM , PDF ).

Сэм Тобин-Хохштадт
источник
Спасибо, бумага Пирса и Тернера была очень поучительной. Вам известна минимальная реализация алгоритма, который они описывают в коде? Я думаю, что было бы очень интересно посмотреть, если оно существует.
Дерек Турн
Я не знаю ни одной минимальной реализации. Один в Typed Racket и один в Scala, но оба реализуют существенно более сложные алгоритмы.
Сэм Тобин-Хохштадт
0

Вы можете взглянуть на системы типов для типов пересечений, которые могут дать вам что-то похожее a :: Int -> Int | Bool -> Bool, так что вы знаете, что двух специализаций достаточно Intи Boolдостаточно, или использовать обычный вывод типа для вывода наиболее общих типов, за которым следует анализ потока управления для сбора фактических данных. введите аргументы. На самом деле существуют гибридные подходы (CFA выражается в виде системы типов и наоборот).

Могут существовать исследовательские работы по выводу наименее общих типов вместо большинства общих типов, но я не знаю о них.

Что касается методов реализации полиморфизма, существуют два решения: 1) специализация (представьте шаблоны C ++) 2) предположение о равномерном представлении (представьте коллекции в стиле C с void *).

Для 2 вам не нужен тип из call-site во время проверки типов, и вы можете легче поддерживать отдельную компиляцию.

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

nponeccop
источник
1
«Вызовы виртуальных методов OO - это совершенно другая вещь, называемая специальным полиморфизмом». Специальный полиморфизм - это еще одно название для перегрузки. Вы, кажется, путаете это с полиморфизмом подтипа.
Раду GRIGore
Но подклассы не обязательно являются подтипами, не так ли? Например, для подтипов LSP предполагается провести.
nponeccop
1
Правда, но не в этом суть. «Подтип полиморфизма» является стандартным термином. Подробности смотрите в en.wikipedia.org/wiki/Subtype_polymorphism .
Раду GRIGore