История изменений

Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Как бы, когда пишешь на хаскеле и ракете, вряд ли ты пользуешься алгоритмами из c++. Тут уж ничего по моему не сделаешь.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)? ...

Остальные аргументы должны быть гетерогенными списками.

На сколько я понимаю, всё таки гомогенными, иначе я не уловил, как функция будет принимать n-ный аргумент разных типов?

Так или иначе, есть сложность: нужно заранее знать типы аргументов (или типы гомогенных массивов, что одно и то же). Это нужно чтобы вычислить тип mapcar. Иначе неоткуда взять информацию о том какой тип у mapcar должен быть. А тип терма должен быть известен на этапе компиляции. Поэтому собственно там у меня гетерогенный список вместо списка аргументов переменной длины - я на этапе компиляции из него беру информацию об аргументах функции и строю для неё тип. Из списка аргументов эту информацию в коке брать нельзя (по крайней мере без штук вроде https://github.com/LPCIC/coq-elpi, но я её глядел только краем глаза и в возможностях не уверен).

Если передать первым параметром массив типов [bool, nat, option nat] как пример, то можно сделать переменное число массивов в качестве аргументов (число аргументов будет вычисляться из данного массива типов, т.е. у нас сейчас три аргумента у ф-ции и три массива аргументов).

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

Разная длина передаваемых массивов не должна по идее вызвать проблему.

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

Но я бы что то не знаю, не взялся бы наверное. Задача интересная если в смысле разобраться с elpi, но больно работы будет много, не уверен что найду время. А без epli, т.е. с передачей массива типов - задача не очень интересная: получиться должно в принципе, но работы многовато и всё таки есть шанс споткнуться на чём то нудном типа конверсия типов при определении в модулях не сработает.. и.п.. мне кажется получается деталей многовато для такого типа задачки.

Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Как бы, когда пишешь на хаскеле и ракете, вряд ли ты пользуешься алгоритмами из c++. Тут уж ничего по моему не сделаешь.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)? ...

Остальные аргументы должны быть гетерогенными списками.

На сколько я понимаю, всё таки гомогенными, иначе я не уловил, как функция будет принимать n-ный аргумент разных типов?

Так или иначе, есть сложность: нужно заранее знать типы аргументов (или типы гомогенных массивов, что одно и то же). Это нужно чтобы вычислить тип mapcar. Иначе неоткуда взять информацию о том какой тип у mapcar должен быть. А тип терма должен быть известен на этапе компиляции. Поэтому собственно там у меня гетерогенный список вместо списка аргументов переменной длины - я на этапе компиляции из него беру информацию об аргументах функции и строю для неё тип. Из списка аргументов эту информацию в коке брать нельзя (по крайней мере без штук вроде https://github.com/LPCIC/coq-elpi, но я её глядел только краем глаза и в возможностях не уверен).

Если передать первым параметром массив типов [bool, nat, option nat] как пример, то можно сделать переменное число массивов в качестве аргументов (число аргументов будет вычисляться из данного массива типов, т.е. у нас сейчас три аргумента у ф-ции и три массива аргументов).

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

Разная длина передаваемых массивов не должна по идее вызвать проблему.

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

Но я бы что то не знаю, не взялся бы наверное. Задача интересная если в смысле разобраться с elpi, но больно работы будет много, не уверен что найду время. А без epli, т.е. с передачей массива типов - задача не очень интересная: получиться должно в принципе, но работы многовато и всё таки есть шанс споткнуться на чём то нудном типа конверсия типов при определении в модулях не сработает.. и.п.. деталей многовато как по мне для задачки типа proof-of-concept.