Estimating cost of evaluating spend script

[Shimuuar]

Главную проблему для оценки времени выполнения представляют струткуры данных переменного размера: байтостроки, текст, списки и функции принимающие параметры такого типа.

Рассмотрим, например, функцию sum :: [Int] -> Int для её выпонения надо выполнить число сложений равное длине списка и не можем задать разумную верхнюю границу, т.к. список может быть длиннее. То есть время выполнения функции надо моделировать как функцию от "размера" типа. Это однако немендленно приводит к той же самой проблеме экспоненциального времени вычисления

let f0 = \xs → xs ++ xs
let f1 = \xs → f0 xs ++ f0 xs
...
in fN [0]

Точно также при оценке времени исполнения данной программы надо будет вызвать функии оценки времени выполнения 2^N раз. Т.е. мы получаем эффективно бесконечное время выполнения. Нужно использовать какую-то другую схему выполнения

[Shimuuar]

Думаю, что главную проблему для нас составляют лямбда функции. Т.к. именно при подстановке парамтра в лябду мы можем получить взрывной рост размера AST. Один возможный подход борьбы с этим состоит в требовании того чтобы скрипты были в β-нормальной форме, т.е. не содержали редексов (λx. ...) y. Это даст нам AST, которе редукции могут только уменьшать: входит такой битковый форт. Проблемы у этого подхода -- две:

1. Что делать с let? let x = e1 in e2 можно переписать как лямбда выражение: (λx. e2) e1. Т.е. их надо инлайнить, вместе с тем их хотелось бы сохранить

2. Примитивы map/filter/etc принимают функции как параметры, что вероятно позволяет протащить функции и возможно сконструировать экспоненциальное поведение

[Shimuuar]

Проблему с размером строк/списков можно отчасти решить просто введением ограничения на размер списка/строки. Это не решает проблему до конца, но для для любого типа, не содержащего функций можно поставить ограничение на размер нормальной формы