Полиморфизм высшего ранга над неупакованными типами

10

У меня есть язык, на котором типы распакованы по умолчанию, с выводом типов на основе Хиндли-Милнера. Я хотел бы добавить полиморфизм более высокого ранга, в основном для работы с экзистенциальными типами.

Я думаю, что понимаю, как проверить эти типы, но я не уверен, что делать при компиляции. В настоящее время я компилирую полиморфные определения, генерируя специализации, очень похожие на шаблоны C ++, чтобы они могли работать с распакованными значениями. Например, если дано определение f<T>, если программа вызывает только f<Int32>и f<Char>, то в скомпилированной программе появляются только эти специализации. (Я предполагаю компиляцию всей программы на данный момент.)

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

Моей первой мыслью было как-то кодировать полиморфизм ранга n как ранг 1, но я не верю, что это вообще возможно, потому что формула в конструктивной логике не обязательно имеет пренекс-нормальную форму.

Джон Перди
источник
Альтернатива состоит в том, чтобы уменьшить объем бокса, необходимый для хранения растровых изображений, для которых аргументы функции и слова в памяти являются указателями. Тогда полиморфная функция / структура на самом деле полиморфна над указателем или произвольным словом данных, и структуры могут хранить свое последнее поле (даже если оно полиморфное) внутри строки. Эти битовые карты также могут использоваться GC, чтобы избежать необходимости использования теговых слов для несуммированных типов.
fread2281
@ fread2281: Я действительно делал что-то подобное в старой версии языка. В настоящее время я не генерирую теги для несуммированных типов, и там нет GC. Я думаю, что это совместимо с подходом Нила К.
Джон Пурди,

Ответы:

6

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

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

Kindsκ::=nType constructorsA::=a:κ.A|α|A×B|A+B|AB|refA|Pad(k)|μα:κ.A

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

Правила сортировки превращают этот английский в математику и должны выглядеть примерно так:

α:nΓΓα:nΓ,α:nA:mΓα:n.A:m
ΓA:nΓB:mΓA×B:n+mΓA:nΓB:nΓA+B:n+1
ΓA:mΓB:nΓAB:1ΓA:nΓrefA:1
ΓPad(k):kΓ,α:nA:nΓμα:n.A:n

Таким образом, полный квантификатор требует, чтобы вы дали вид, на который вы попадаете. Аналогично, спаривание - это распакованный тип пары, который просто размещает рядом с в памяти (как тип структуры C). Несвязанные объединения принимают два значения одинакового размера, а затем добавляют слово для тега дискриминатора. Функции - это замыкания, представленные, как обычно, указателем на запись среды и кода.A×BAB

Ссылки интересны - указатели - это всегда одно слово, но они могут указывать на значения любого размера. Это позволяет программистам реализовывать полиморфизм для произвольных объектов с помощью бокса, но не требует от них этого. Наконец, когда в игру вступают явные размеры, часто полезно ввести тип заполнения, который использует пробел, но ничего не делает. (Поэтому, если вы хотите взять несвязанное объединение целого и пары целых чисел, вам нужно добавить отступ первого целого, чтобы макет объекта был равномерным.)

У рекурсивных типов есть стандартное правило формирования, но обратите внимание, что рекурсивные вхождения должны быть одинакового размера, что означает, что вы обычно должны вставлять их в указатель, чтобы сортировка работала. Например, тип данных списка может быть представлен как

μα:1.ref(Pad(2)+int×α)

Таким образом, это указывает на пустое значение списка или пару int и указатель на другой связанный список.

Проверка типа для подобных систем также не очень сложна; алгоритм в моей работе ICFP с Джошуа Данфилдом, « Полная и простая двунаправленная проверка типов для более высокого ранга полиморфизма» применяется к этому случаю практически без изменений.

Нил Кришнасвами
источник
Круто, я думаю, что это аккуратно охватывает мой случай использования. Я знал об использовании видов для рассуждения о представлении значений (например, GHC *против #), но не думал об этом. Представляется разумным ограничить квантификаторы с более высоким рейтингом типами известного размера, и я думаю, что это также позволило бы мне генерировать специализации для размера статически, без необходимости знать фактический тип. Теперь время перечитать эту статью. :)
Джон Перди
1

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

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

Например, низкоуровневое представление неупакованных аргументов обычно можно разделить на несколько вариантов, например, целочисленное или похожее, с плавающей точкой или указатель. Таким образом, для функции f<T>, может быть, вам действительно нужно сгенерировать только 3 разные реализации без упаковки, и вы можете представить полиморфную реализацию как кортеж из этих трех функций, поэтому создание экземпляра T для Int32 просто выбирает первый элемент кортежа, ...

Стефан
источник
Спасибо за вашу помощь. Я не был уверен, где спросить, так как компилятор охватывает теорию высокого уровня и низкоуровневую инженерию, но я полагал, что у людей здесь будут некоторые идеи. Похоже, бокс действительно может быть самым гибким подходом здесь. После прочтения вашего ответа и обдумывания его, единственное разумное решение, которое мне удалось найти, - это отказаться от некоторой гибкости и потребовать, чтобы полиморфные аргументы были известны статически, например, передавая их в качестве параметров типа. Это компромиссы полностью вниз. : P
Джон Пёрди,
4
Вопрос ОП содержит вполне допустимые проблемы TCS, например, как сделать вывод типа, когда Дамас-Хиндли-Милнер расширен типами более высокого ранга. В общем случае полиморфизм ранга 2 имеет разрешимый вывод типа, но для ранга k> 2 вывод типа неразрешим. Изменит ли это ограничение Дамаса-Хиндли-Милнера, я не знаю. Наконец, почти все, что делают современные компиляторы, должно быть частью TCS, но обычно это не потому, что разработчики компиляторов опережают теоретиков.
Мартин Бергер