Размышляя о параметре типа

Question

Я пытаюсь создать функцию

import Language.Reflection 
foo : Type -> TT 

Я попробовал его с помощью reflect тактику:

foo = proof 
    { 
    intro t 
    reflect t 
    } 

, но это отражается на самой переменной t:

*SOQuestion> foo 
\t => P Bound (UN "t") (TType (UVar 41)) : Type -> TT 

Answer 1

Отражение в Идрисе - это чисто синтаксическая функция времени компиляции. Чтобы предсказать, как это будет работать, вам нужно знать, как Idris преобразует вашу программу на свой основной язык. Важно отметить, что во время выполнения вы не сможете получить отраженные условия и восстановить их, как если бы вы были с Lisp. Вот как скомпилирована ваша программа:

1. Внутренне, Идрис создает отверстие, которое ожидает что-то типа Type -> TT.
2. В этом состоянии работает скрипт доказательства для foo. Мы начинаем с каких-либо предположений и цели типа Type -> TT. То есть, строится термин, который выглядит как ?rhs : Type => TT . rhs. Синтаксис ?foo : ty => body показывает, что есть отверстие под названием foo, возможное значение которого будет доступно внутри body.
3. Шаг intro t создает функцию, аргумент которой равен t : Type. Это означает, что теперь у нас есть термин, такой как ?foo_body : TT . \t : Type => foo_body.
4. Шаг reflect t затем заполняет текущее отверстие, беря его с правой стороны и преобразуя его в TT. Этот термин на самом деле является лишь ссылкой на аргумент функции, поэтому вы получаете переменную t. reflect, как и все другие скрипты сценария проверки, имеет доступ только к информации, доступной непосредственно во время компиляции. Таким образом, результатом заполнения foo_body с отражением термина t является P Bound (UN "t") (TType (UVar (-1))).

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

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

Потеря производительности зависит от представления достаточной информации о типе для отражения. После компиляции кода Idris в нем нет информации о типе (в отличие от системы JVM или .NET или динамически типизированной системы, такой как Python, где типы имеют представление времени выполнения, к которому может обращаться код). В Идрисе типы могут быть очень большими, потому что они могут содержать произвольные программы - это означает, что необходимо сохранить гораздо больше информации, а вычисления, выполняемые на уровне типа, также должны быть сохранены и повторены во время выполнения.

Если вы хотите задуматься о структуре типа для дальнейшей автоматизации доказательств во время компиляции, взгляните на тактику applyTactic. Его аргумент должен быть функцией, которая принимает отраженный контекст и цель и возвращает новый отраженный тактический сценарий. Пример можно увидеть in the Data.Vect source.

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