type-systems - 哪种类型的系统可以防止逻辑语言暂停目标？

Question

从curry tutorial的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] ?

另一方面，预定义的算术运算(如加号“+”)是严格的。因此，
使用逻辑变量作为参数的“+”调用比目 fish :

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

Curry似乎并不能防止写作目标被暂停。哪种类型的系统可以提前检测到是否将暂停目标？

Answer 1

您所描述的听起来像是模式检查，它通常检查哪些输出可用于特定的一组输入。您可能需要检查Mercury语言，它非常重视模式检查。