Реализовать и представлять полиадические операции

Question

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

В макропроцессоре пользователь может написать эту функцию, потому что кортежи - это списки.

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

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

f1: D1 -> C1, f2: D2-> C2 --> f1 * f2: D1 * D2 -> C1 * C2 

легко написано, но не может быть продлен до 3-х условиях: здесь складка бы вычислить

f1 * (f2 * f3) 

вместо

f1 * f2 * f3 

[изоморфно, но не равно]

Обобщение этого вопроса: «Как мне внедрить полиадический язык программирования ", который слишком много, чтобы спросить здесь. То, что я пытался сделать, это обеспечить встроенный трансформатор:

карри: T1 * T2 * T3 ... -> T1 -> T2 -> ... uncurry: T1 -> T2 -> .. T1 * T2 * T3

так, то пользователь просто может сделать сгибы с бинарным оператором:

uncurry (fold user_op (uncurry term)) 

, но это не является ни достаточно универсален и не работает так хорошо .. :)

Я думаю, эквивалентный вопрос для Haskell было бы: поскольку Haskell не имеет n-арных продуктов, конструкторы n-ary tuple моделируются в th e библиотека с n функциями, каждая из которых должна быть выписана вручную. Это явно отстой. Как это будет исправлено?

[Я имею в виду, это тривиально, чтобы написать сценарий Python для создания этих п функций вплоть до некоторого предела п, так почему это так трудно сделать это в хорошо напечатанные образом внутри язык?]

Answer 1

есть два компонента, которые сотрудничают, чтобы вызвать эту проблему:

• кортежей автоматически не сплющенный - скобки в выражениях типа сделать больше, чем группы, они создают различные типы, которые соединены дополнительными кортежи. Это приводит к вашему наблюдению, что a * (b * c) изоморфен, но не эквивалентен a * b * c.
• Система типов не предоставляет средства для выражения алгебры по типам кортежей. Под этим я подразумеваю, что система типов не имеет оператора cons или любого эквивалента для кортежей; нет никакого способа выразить, что тип имеет больше или меньше элементов с чередованием, чем другой тип.

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

Итак, краткое изложение состоит в том, что система типа OCaml не имеет механизмов для выражения типа функции, которую вы пытаетесь написать, и, следовательно, вы не можете написать функцию (отбросив неприятные игры с помощью Obj; вы можете написать функцию , но вы не можете выразить свой тип, чтобы использовать его безопасным образом).

Answer 2

Существует в основном два варианта.

Вы можете сделать свой язык не типичным или слабо типизированным. Например, в C кортежи (целые числа, скажем) могут быть представлены как int*. Что-то нужно будет отслеживать длины кортежей, но система типа не будет. Я полагаю, вы не хотите идти именно так.

Для типа безопасного языка вам нужна очень выразительная система типов. А именно, вам нужны типы, зависящие от значений. Участниками которых являются функции, возвращающие типы. Например, конструктор типа кортежа (не путать с конструктором кортежа) может иметь тип tuple : int -> Type -> Type. Операция, которая расширяет кортеж, может иметь тип forall n:int. forall T:Type. tuple n T -> T -> tuple (n+1) T. Такие системы типов стоят дорого: обычно вывод типа не рекурсивный, и проверка типов разрешима только в том случае, если вы готовы аннотировать все виды подвыражений с их типом (аннотации в вышеприведенных частях forall являются лишь намеком на то, что влекут за собой.). Эти варианты кажутся излишними, если все, что вы хотите достичь, это полиадность.

Отказ от ответственности: Мое знание теории типов немного устарело.