What type systems can prevent goal suspension in logical languages?
Asked Answered
U

1

23

From section 3.13.3 of the curry tutorial:


Operations that residuate are called rigid , whereas operations that narrow are called flexible. All defined operations are flexible whereas most primitive operations, like arithmetic operations, are rigid since guessing is not a reasonable option for them. For example, the prelude defines a list concatenation operation as follows:

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

Since the operation “++” is flexible, we can use it to search for a list satisfying a particular property:

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

On the other hand, predefined arithmetic operations like the addition “+” are rigid. Thus, a call to “+” with a logic variable as an argument flounders:

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

Curry does not appear to guard against writing goals that will be suspended. What type systems can detect ahead of time whether a goal is going to be suspended?

Upwind answered 12/1, 2011 at 0:29 Comment(1)
IMO, such a question could be answered sooner by experts in type systems (perhaps, at cstheory.stackexchange.com ) or Curry experts (in their mailing list).Wiese
R
3

What you've described sounds like mode checking, which generally checks what outputs will be available for a certain set of inputs. You may want to check the language Mercury which takes mode checking quite seriously.

Rosenberger answered 10/4, 2011 at 9:19 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.