Currently, the following query typechecks:
?- lambda([X], X = 1) = lambda([X], X = 1).
The above query attempts to unify two lambdas together. Strictly speaking, this is asking if two relations are equivalent, which is undecidable, and entails higher-order unification. Currently, this is accepted as long as the relations bear the same type (both above have the type relation(int), and so this is ok).
The semantics of this are somewhat bizarre currently. Generally, unification will fail, as it will above (even though syntactic identity holds). Unification can succeed if the same syntactic lambda is used to create multiple closures, and then the closures are compared, like so:
clausedef(makeClosure, [], [int, relation(int, int, int)]).
makeClosure(X, lambda([Y, Z], Z is X + Y)).
?- makeClosure(1, L1), makeClosure(X, L2), L1 = L2.
What happens in this situation is that the closure environments will be unified with each other, so if we were to later attempt to call L2, like so:
% same query as before for `...`
?- ..., call(L2, 2, Result).
Result = 3.
...we get that Result = 3, as X ultimately is unified with 1 indirectly with L1 = L2. While this makes sense with respect to the explanation, it's woefully unintuitive, and almost assuredly this isn't what the user intends. We should instead statically disallow this sort of comparison.
Disallowing this is harder than it seems, as ultimately we want to ensure that we only ever unify higher-order relations with variables which are guaranteed to be uninstantiated. This suggests that we need mode analysis in the type system, at least in order to keep things intraprocedural.
Currently, the following query typechecks:
The above query attempts to unify two lambdas together. Strictly speaking, this is asking if two relations are equivalent, which is undecidable, and entails higher-order unification. Currently, this is accepted as long as the relations bear the same type (both above have the type
relation(int), and so this is ok).The semantics of this are somewhat bizarre currently. Generally, unification will fail, as it will above (even though syntactic identity holds). Unification can succeed if the same syntactic lambda is used to create multiple closures, and then the closures are compared, like so:
What happens in this situation is that the closure environments will be unified with each other, so if we were to later attempt to call
L2, like so:...we get that
Result = 3, asXultimately is unified with1indirectly withL1 = L2. While this makes sense with respect to the explanation, it's woefully unintuitive, and almost assuredly this isn't what the user intends. We should instead statically disallow this sort of comparison.Disallowing this is harder than it seems, as ultimately we want to ensure that we only ever unify higher-order relations with variables which are guaranteed to be uninstantiated. This suggests that we need mode analysis in the type system, at least in order to keep things intraprocedural.