Какие системы типов могут предотвратить приостановку цели в логических языках?

Question

Из раздела 3.13.3 учебника по карри:

---

Остаточные операции называются жесткими, а узкие - гибкими. Все определенные операции являются гибкими, в то время как большинство примитивных операций, таких как арифметические операции, являются жесткими, так как гадание не является разумным вариантом для них. Например, прелюдия определяет операцию конкатенации списка следующим образом:

infixr 5 ++
...
(++)             :: [a] -> [a] -> [a]
[]       ++ ys   = ys
(x:xs) ++ ys     = x : xs ++ ys

Поскольку операция "++" является гибкой, мы можем использовать ее для поиска списка, удовлетворяющего определенному свойству:

Prelude> x ++ [3,4] =:= [1,2,3,4]       where x free
Free variables in goal: x
Result: success
Bindings:
x=[1,2] ?

С другой стороны, предопределенные арифметические операции, такие как сложение "+", являются жесткими. Таким образом, вызов "+" с логической переменной в качестве аргумента приводит к ошибкам:

Prelude> x + 2 =:= 4 where x free
Free variables in goal: x
*** Goal suspended!

---

Карри, кажется, не защищает от написания целей, которые будут приостановлены. Какие системы типов могут заранее определить, будет ли цель приостановлена?

Answer 1

То, что вы описали, звучит как проверка режима, которая обычно проверяет, какие выходы будут доступны для определенного набора входов. Вы можете проверить язык Mercury, который относится к проверке режима довольно серьезно.