Predicate parameters are not constrained

One of the most surprising things in Alloy for me was that predicates are not constrained by their parameter type

pred foo[ n :one Int ] {}

run withset { foo[ Int ] } 
run withnone { foo[ none ] } 

Clearly the first run makes n a set and the second uses none. Both times the constraint defined for the n parameter does not satisfy the given constraint one Int.

It would make my life a lot easier (and I expect newcomers as well) if the predicate began with checking its parameters. That s pred foo[ n : Int ] { one n .... }

I vaguely recall that Daniel ones explained me why this was a case of a rock and a hard place. However, I think it is a good time to have this discussion. And if Daniel can explain it, at least we’ve got it on record :slight_smile:

It is indeed a really annoying feature of Alloy that declaration constraints are only enforced when you run a function or predicate directly. My recollection is that the reason we didn’t enforce them everywhere is that we couldn’t come up with a simple semantics. The obvious strategy would be to add explicit constraints in calls, so that if you call a predicate

pred foo[ n :one Int ] {}

like this


the call would be taken as short for

foo[e] and one e

The problem, as far as I recall, is that it’s not clear what to do with functions. Suppose I declare

fun bar [x: one X]: Y {...}

and now I have something like

all a, b: X | bar[a+b] in bar[a] + bar[b]

what constraints do I add and where?

It just seemed more trouble than it was worth. Now that I think about it again, though, I wonder if the inconsistency we already have is any better than just doing this for predicates but not functions, which should be pretty easy.

1 Like

Could we also constrain it to be in the proper set? I.e. one (e & Int). I guess the parser will not allow any mismatched types but it will make my life a bit easier :slight_smile: I also think we already have a precedent for this since a run foo already infers the proper type.

BTW, there is already a discussion on github No type checking on directly run predicates · Issue #14 · AlloyTools/org.alloytools.alloy · GitHub

I wouldn’t translate the decl constraint that way. Suppose the predicate is

sig S {}
sig S2 extends S {}
pred foo [x: one S2] {...}


one (x & S2)

allows x to violate the constraint x in S2. What’s wrong with this?

one x and x in S2

Not following … assuming s was meant to be x?

sig S {}
sig S2 extends S {}
check {
	all x : univ | (x in S2 and one x) iff (one (x & S2))

Has no counter example?

Yes, sorry – meant x. I edited the original post.

Try this:

sig S {}
sig S2 extends S {}
check {
	all x : set univ | (x in S2 and one x) iff (one (x & S2))

Ah! Thanks :slight_smile:

Good lesson!