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 
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
foo[e]
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 I also think we already have a precedent for this since a run foo already infers the proper type.
I wouldn’t translate the decl constraint that way. Suppose the predicate is
sig S {}
sig S2 extends S {}
pred foo [x: one S2] {...}
Then
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))
}