У меня есть язык, на котором типы распакованы по умолчанию, с выводом типов на основе Хиндли-Милнера. Я хотел бы добавить полиморфизм более высокого ранга, в основном для работы с экзистенциальными типами.
Я думаю, что понимаю, как проверить эти типы, но я не уверен, что делать при компиляции. В настоящее время я компилирую полиморфные определения, генерируя специализации, очень похожие на шаблоны C ++, чтобы они могли работать с распакованными значениями. Например, если дано определение f<T>
, если программа вызывает только f<Int32>
и f<Char>
, то в скомпилированной программе появляются только эти специализации. (Я предполагаю компиляцию всей программы на данный момент.)
Но когда я передаю полиморфную функцию в качестве аргумента, я не вижу, как я могу генерировать правильную специализацию статически, потому что функция может быть выбрана во время выполнения. У меня нет выбора, кроме как использовать представление в штучной упаковке? Или есть способ обойти проблему?
Моей первой мыслью было как-то кодировать полиморфизм ранга n как ранг 1, но я не верю, что это вообще возможно, потому что формула в конструктивной логике не обязательно имеет пренекс-нормальную форму.
источник
Ответы:
Я немного подумал об этом. Основная проблема заключается в том, что в целом мы не знаем, насколько велико значение полиморфного типа. Если у вас нет этой информации, вы должны как-то ее получить. Мономорфизация получает эту информацию для вас, специализируясь на полиморфизме. Бокс получает эту информацию для вас, помещая все в представление известного размера.
Третий вариант - отслеживать эту информацию по видам. По сути, вы можете ввести разные типы для каждого размера данных, и тогда полиморфные функции могут быть определены для всех типов определенного размера. Я нарисую такую систему ниже.
Здесь идея высокого уровня заключается в том, что тип типа сообщает вам, сколько слов требуется для размещения объекта в памяти. Для любого данного размера легко быть полиморфным по всем типам этого определенного размера. Поскольку каждый тип - даже полиморфный - по-прежнему имеет известный размер, компиляция не сложнее, чем для C.
Правила сортировки превращают этот английский в математику и должны выглядеть примерно так:
Таким образом, полный квантификатор требует, чтобы вы дали вид, на который вы попадаете. Аналогично, спаривание - это распакованный тип пары, который просто размещает рядом с в памяти (как тип структуры C). Несвязанные объединения принимают два значения одинакового размера, а затем добавляют слово для тега дискриминатора. Функции - это замыкания, представленные, как обычно, указателем на запись среды и кода.A×B A B
Ссылки интересны - указатели - это всегда одно слово, но они могут указывать на значения любого размера. Это позволяет программистам реализовывать полиморфизм для произвольных объектов с помощью бокса, но не требует от них этого. Наконец, когда в игру вступают явные размеры, часто полезно ввести тип заполнения, который использует пробел, но ничего не делает. (Поэтому, если вы хотите взять несвязанное объединение целого и пары целых чисел, вам нужно добавить отступ первого целого, чтобы макет объекта был равномерным.)
У рекурсивных типов есть стандартное правило формирования, но обратите внимание, что рекурсивные вхождения должны быть одинакового размера, что означает, что вы обычно должны вставлять их в указатель, чтобы сортировка работала. Например, тип данных списка может быть представлен как
Таким образом, это указывает на пустое значение списка или пару int и указатель на другой связанный список.
Проверка типа для подобных систем также не очень сложна; алгоритм в моей работе ICFP с Джошуа Данфилдом, « Полная и простая двунаправленная проверка типов для более высокого ранга полиморфизма» применяется к этому случаю практически без изменений.
источник
*
против#
), но не думал об этом. Представляется разумным ограничить квантификаторы с более высоким рейтингом типами известного размера, и я думаю, что это также позволило бы мне генерировать специализации для размера статически, без необходимости знать фактический тип. Теперь время перечитать эту статью. :)Похоже, что это ближе к проблеме компиляции, чем к проблеме «теоретической информатики», так что вам, вероятно, лучше спросить в другом месте.
В общем случае, на самом деле, я думаю, что нет другого решения, кроме использования коробочного представления. Но я также ожидаю, что на практике существует много разных альтернативных вариантов, в зависимости от специфики вашей ситуации.
Например, низкоуровневое представление неупакованных аргументов обычно можно разделить на несколько вариантов, например, целочисленное или похожее, с плавающей точкой или указатель. Таким образом, для функции
f<T>
, может быть, вам действительно нужно сгенерировать только 3 разные реализации без упаковки, и вы можете представить полиморфную реализацию как кортеж из этих трех функций, поэтому создание экземпляра T для Int32 просто выбирает первый элемент кортежа, ...источник