Могут ли количественные типы, , которые появляются в Idris 2 , использоваться, чтобы гарантировать сложность алгоритма? Например, подпись map определена для Vect как
map : (a -> b) -> Vect n a -> Vect n b
, но если мы изменим ее как
map : (n f: (a -> b)) -> Vect n a -> Vect n b
(если это правильный синтаксис), то мы узнаем f будет использоваться только n раз. Это дает нам дополнительную уверенность в том, что map линейно по отношению к n. Однако это не доказывает этого, поскольку мы могли бы выполнять другие операции, которые> O (n), не игнорируя типы. Это правильно? И можно ли его расширить, чтобы доказать, что map действительно O (n)? И возможно ли это, если нет некоторого аргумента, такого как f, для обозначения сложности, как в инверсии матрицы O (m ^ 3)
invert : Vect m (Vect m elem) -> Vect m (Vect m elem)