instance belonging to two different sorts

[anuradha252]

    module entity_event_and_action
            sort declarations
            thing :: universe
            entity :: thing
            spatial_entity :: entity
                  ...
             event :: actions
              attributes
                                   ....
             actions_new :: event 
                  ...

    module accessibility
      depends on entity_event_and_action
          sort declarations
            make_accessible :: actions_new
                            make_inaccessible :: actions_new
                              ...
            state constraints   
                false if instance(X, make_accessible),
                         -defined_object(X).

                false if instance(X, make_inaccessible),
                         -defined_object(X).
                                ...

    module unobstructing_and_obstructing
      depends on accessibility

      sort declarations
        unobstruct :: make_accessible
        obstruct :: make_inaccessible
                 ...
              axioms
        state constraints
                           false if instance(X, obstruct),
                     object(X, O),
                     -instance(X, spatial_entity). 

error that I'm receving ErrorID: TYP002 Message: The sorts inferred for variable [X at (175:22)] are not compatible. Explanation: Every variable must have a single sort from which it obtains its possible values.

Module compiles if I remove -instance(X, spatial_entity) from the state constraints.

Could this be because X here is used as an instance of event as well as entity?

Should this be allowed?

[Topology]

This is a bug,

I will need to modify type-checking to be sensitive to the sign of the instance(X, Y) literal. Right now I assumed all instance(X,Y) would appear positively. When occurring positively, they add type restrictions. My mistake here is to treat spatial_entity as a new positive restriction. The positive restriction would be to assert that X must be in {SuperSort - spatial_entity}.

What I will do to fix this as a near term solution is to not add any restriction to X in type checking for -instance(X,Y). I'll let SPARC handle the negation of the literal.

The long term fix may be to expand set calculus in my type system and render the type restrictions more formally based on the complex expressions.

[zhangyuanlin]

I double checked the paper, here is the signature of instance:

instance : universe × nodes → booleans

So, the type checking to enforce X to be of the corresponding sort is not correct. The expected sort of X in Anu's statement is universe. So, type checking should be ok.

[Topology]

The instance(X,Y) is effectively a cast, like java. The purpose of type checking is to help the programmer catch mistakes they made before sending the program to sparc.

consider

 instance(X, cats),   instance(X, dogs)

where the intersection of cats and dogs is empty.

I can let that go through and let SPARC deal with it. But SPARC is never going to tell you why the rule containing this never fires. Or if it is part of some logic that should disable a constraint, why you don't have an answer set.

Or I can catch the fact that the intersection of cats and dogs is empty and complain to the programmer.

Consider the following function signatures and rule.

johns_cat : cats
johns_dog: dogs
:- johns_cat =X, johns_dog = Y, X !=Y.

The above will generate a type error if there is no common subsort to cats and dogs exists.

Should there be a type error in the following?

cats, dogs :: pets
johns_pet : pets
johns_pet = X  : - instance(X, cats), instance(X, dogs). 
:- -dom_johns_pet 

If I don't catch it, it becomes a bomb that kills a very large sparc program.

[Topology]

I changed the program that I said would cause problems.

[zhangyuanlin]

1. In your last question, there is no type error (in terms of type signaure of functions) unless the type signature of instance() is changed. As shown in Anu's state constraint, I think instance() is very different from type cast.
2. In fact, there is similar issue in SPARC. If the instantiation of a rule doesn't exist, SPARC takes it as a warning, but not a type error.
3. in

   johns_cat : cats
   johns_dog: dogs
   :-  johns_cat = X, johns_dog = X

   We have to do some inference on the type of X. As long as the inference is "general enough", I still take the resulting check as a type checking.

4. I think underlying your reasoning, you might have embed the "meaning" (not just signature) of instance() into type checking, which I think is too strong.

[zhangyuanlin]

Edward, is this issue resolved?

[Topology]

I just re-uploaded the latest distribution, which should disable adding type constraints when instance atoms occur with a negative sign on them. Please check that the latest calm.jar does not have the same problem as originally reported in this issue.

Apart from that we discovered a difference in understanding of how type checking with respect to instance atoms should work. The resolution of that difference in understanding should probably be done through a live conversation.

instance(X,  sortY)

It is true that the signature of the instance function only requires X to be an element in the universe. I am looking at the programmer's intent and trying to catch errors early that would be very hard to detect in the SPARC program. I add the tighter type constraint because I find it helpful and (apart from the treatment of negative instance atoms) do not find it to be incorrect. (I could be wrong, but I would need help seeing how this is wrong.)