HOAS + data type a la carte
Я попытался собрать a la carte тип для значений интерпретатора лямбда-исчисления. Так как в лямбда-исчислении бывают функции-значения, мне понадобилось определить
data VFun e = VFun (e -> e)
и как только я написал отрицательное вхождение параметра, я понял, что никакого функтора у меня уже не получится. После непродолжительного поиска я нашёл у Кметта предложение воспользоваться профункторами и сдобрить всё это типами второго порядка, на что я пойти не могу. Есть альтернативные решения Дея и Хаттона, например, завести тип "замыкание" или перейти просто к представлению с индексами де Брейна, но это уже болезненно. В любом случае, я пишу транслятор, интерпретатор писал для интереса, и в этой теме сильно глубоко разбираться не хочется, но.
Это ведь синтаксическая причина. А мне интересно, в чём причина семантическая: какого именно дьявола призывают HOAS, что я не могу собрать катаморфизм для такого типа? Я не вижу никаких реальных семантических проблем в том, чтобы пройтись по AST в HOAS-форме и что-то от такого AST посчитать. Товарищи, посоветуйте, пожалуйста.
data VFun e = VFun (e -> e)
и как только я написал отрицательное вхождение параметра, я понял, что никакого функтора у меня уже не получится. После непродолжительного поиска я нашёл у Кметта предложение воспользоваться профункторами и сдобрить всё это типами второго порядка, на что я пойти не могу. Есть альтернативные решения Дея и Хаттона, например, завести тип "замыкание" или перейти просто к представлению с индексами де Брейна, но это уже болезненно. В любом случае, я пишу транслятор, интерпретатор писал для интереса, и в этой теме сильно глубоко разбираться не хочется, но.
Это ведь синтаксическая причина. А мне интересно, в чём причина семантическая: какого именно дьявола призывают HOAS, что я не могу собрать катаморфизм для такого типа? Я не вижу никаких реальных семантических проблем в том, чтобы пройтись по AST в HOAS-форме и что-то от такого AST посчитать. Товарищи, посоветуйте, пожалуйста.