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

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, который серьезно относится к проверке режима.