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

Question

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

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

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

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

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

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

 f1 * (f2 * f3)

вместо

f1 * f2 * f3

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

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

curry: T1 * T2 * T3 ... -> T1 -> T2 -> ... uncurry: T1 -> T2 -> .. T1* T2 * T3

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

uncurry (fold user_op (uncurry term))

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

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

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

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 частях выше являются лишь указаниемэто повлечет за собой.)Этот вариант кажется излишним, если все, чего вы хотите добиться, - это полиадичность.

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