Метапрограммирование в Агде и немного философии

[xeno_by]

На днях просмотрел паперу Dependent Type Providers [1] и магистерскую диссертацию Reflection in Agda [2], которые используют средства рефлекшена, предоставляемые Агдой, для метапрограммирования

Comments

[ex_juan_gan]

Хм, концептуально это логично звучит; но это как бы выходит за пределы математики, и непонятно, как это формализовать-то.

[xeno_by]

На это мне пока что ответить нечего, к сожалению. Я предполагаю, что именно из-за этого никто особо из академиков не парится на эту тему.

[ex_juan_gan]

Но проблема-то от этого не исчезает, конечно. Метапроблема.

[ext_1178598]

> и непонятно, как это формализовать-то.

А это действительно плохо?