хочу сделать из него компилятор. сложность в том, что eval для выражений вызывается на стадии проверки типов (зависимая типизация), и если я сделаю "втупую" ещё и компилятор выражений в какой-то другой язык, то получается, что при добавлении нового выражения мне нужно изменить свою кодовую базу в двух местах: eval и compile. это муторно, к тому же эти реализации могут расходиться из-за багов, т.е. во время компиляции одна семантика, а во время исполнения совсем другая.
есть какие-то общепринятые подходы для решения этой проблемы?
Идея в том, что разные семантики - это просто разные параметры у eval. eval пишется один раз, а потом в него подставляются разные методы "вычисления". Гуглить надо "стандартную семантику".
Это вы хотите сказать, что модные эффекты придумали в лиспе?
а чем вас не устраивает разные семантики? Они вам и понадобятся разные скорее всего. Как минимум на тайп-левеле нужно вычислять в том числе и открытые термы, а на терм-левеле только закрытые (ну если у вас там не что-то странное). Агда к примеру заглядывает под лямбды во время нормализации, а в рантайме это нетипично делать. В рантайме у вас с высокой вероятностью типов уже не будет (хаскель выкидывает типы, к примеру, но часть инфы оставляет), так что не получится сделать type-driven partial evaluation, а на тайп-левеле это удобно, потому что позволяет делать такие вещи: https://raw.githack.com/effectfully/inference-in-agda/master/InferenceInAgda.html#eta-rules Ну и так далее. Можете попытаться сделать универсальный вычислитель, но скорее всего будет и неудобно и тормозно. Но если у кого-то есть статьи на эту тему, то я бы тоже почитал
> Как минимум на тайп-левеле нужно вычислять в том числе и открытые термы, а на терм-левеле только закрытые у меня eval просто принимает список значений для вычисления терма. если значение "отсутствует", то это будет просто нейтральная переменная в списке > гда к примеру заглядывает под лямбды во время нормализации, а в рантайме это нетипично делать. меня устраивает энергичная стратегия и во время компиляции, и в рантайме > В рантайме у вас с высокой вероятностью типов уже не будет (хаскель выкидывает типы, к примеру, но часть инфы оставляет) это зависит от системы типов. емнип, идрис не "выкидывает" все типы в рантайме, а вычисляет. у хаскелля может быть с этим попроще, т.к. у него нет зав. типов из коробки
Обсуждают сегодня