Почему Идрису требуется, чтобы функции отображались в порядке их определений и взаимной рекурсии, объявленных с помощью mutual?Почему Идрису нужно взаимное?
Я бы ожидал, что Идрис выполнит первый проход анализа зависимости между функциями и автоматически изменит их порядок. Я всегда считал, что Хаскелл это делает. Почему это невозможно в Идрисе?
В tutorial он говорит (курсив мой):
В целом, функции и типы данных должны быть определены перед использованием, поскольку зависимые типы позволяют функции появляться как часть типов, и их сокращение поведение, влияющее на проверку типов. Однако это ограничение может быть ослаблено с помощью взаимного блока, который позволяет определять типы данных и функции , определенные одновременно.
(Agda имеет это ограничение, а также, но теперь removed the mutual keyword in favour of giving types then definitions.)
Для расширения: когда у вас есть зависимые типы, анализ автоматической зависимости а-ля Haskell будет трудно или невозможно, так как порядок зависимостей на уровне типа может очень отличаться от порядка зависимостей на уровне значений. У Haskell нет этой проблемы, потому что значения не могут отображаться в типах, поэтому он может просто анализировать зависимость, а затем typecheck в этом порядке. Это то, чему занимается учебник Идриса по поводу поведения, связанного с уменьшением, которое требуется для проверки типа.
Я не знаю, разрешена ли проблема вообще с зависимыми типами (вы теряете Hindley-Milner, с одной стороны), но я уверен, что это было бы неэффективно, даже если бы это было так.
Agda по-прежнему требует, чтобы вы были несколько явными в отношении взаимно-рекурсивных определений, поскольку вам нужно дать подпись типа каждого члена взаимно-рекурсивной группы, прежде чем давать определение любому из них. – Cactus
Да, понял, что я немного оттуда. Обновите ответ. –
Это не объясняет, почему этот выбор был сделан - почему бы не выполнить автоматический анализ зависимостей, например, в Haskell, вместо того, чтобы требовать явной рекурсии, например, в Caml? – jch