Специализни шаблонца! (udpn) wrote,
Специализни шаблонца!
udpn

HOAS + data type a la carte

Я попытался собрать a la carte тип для значений интерпретатора лямбда-исчисления. Так как в лямбда-исчислении бывают функции-значения, мне понадобилось определить

data VFun e = VFun (e -> e)

и как только я написал отрицательное вхождение параметра, я понял, что никакого функтора у меня уже не получится. После непродолжительного поиска я нашёл у Кметта предложение воспользоваться профункторами и сдобрить всё это типами второго порядка, на что я пойти не могу. Есть альтернативные решения Дея и Хаттона, например, завести тип "замыкание" или перейти просто к представлению с индексами де Брейна, но это уже болезненно. В любом случае, я пишу транслятор, интерпретатор писал для интереса, и в этой теме сильно глубоко разбираться не хочется, но.

Это ведь синтаксическая причина. А мне интересно, в чём причина семантическая: какого именно дьявола призывают HOAS, что я не могу собрать катаморфизм для такого типа? Я не вижу никаких реальных семантических проблем в том, чтобы пройтись по AST в HOAS-форме и что-то от такого AST посчитать. Товарищи, посоветуйте, пожалуйста.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 2 comments