Bounded polymorphism problem

Discussions related to Visual Prolog
Martin Meyer
VIP Member
Posts: 276
Joined: 14 Nov 2002 0:01

Bounded polymorphism problem

Unread post by Martin Meyer » 17 May 2019 15:54

Hello Thomas,

this works (in build 902):

Code: Select all

class predicates     p : () -> Dom         where Dom supports integer. clauses     p() = 1 + 0.
But with these variants there is some problem:

Code: Select all

class predicates     p1 : () -> Dom         where Dom supports integer. clauses     p1() = 1.  % raises: 1 is not in the domain 'Dom'   class predicates     p2 : (integer) -> Dom         where Dom supports integer. clauses     p2(X) = X.  % raises: The expression has type '::integer', which is incompatible with the type 'Dom'
Regards Martin

User avatar
Thomas Linder Puls
VIP Member
Posts: 2422
Joined: 28 Feb 2000 0:01

Re: Bounded polymorphism problem

Unread post by Thomas Linder Puls » 18 May 2019 22:07

Thank you, we will look at it.
Regards Thomas Linder Puls
PDC

User avatar
Thomas Linder Puls
VIP Member
Posts: 2422
Joined: 28 Feb 2000 0:01

Re: Bounded polymorphism problem

Unread post by Thomas Linder Puls » 28 May 2019 13:03

p1 is clearly a bug.

But p2 is correct, which you can see from this example:

Code: Select all

class main   domains     dom = integer [-10..10].   predicates     p : (integer) -> dom.   end class main   %==   implement main   clauses     p(X) = X.   end implement main
Here dom is an actual type 'supports' integer. And that gives the error, because the conversion would go in the wrong direction.
Regards Thomas Linder Puls
PDC

Martin Meyer
VIP Member
Posts: 276
Joined: 14 Nov 2002 0:01

Re: Bounded polymorphism problem

Unread post by Martin Meyer » 29 May 2019 0:17

Analogous p1 could be proofed correct by:

Code: Select all

class main   domains     dom = integer [2..10].   predicates     p : () -> dom.   end class main   %==   implement main   clauses     p() = 1.   end implement main
I think when type checking is done that way, for any use of bounded polymorphism on an output parameter, a type checking error could be proofed correct. Thus I expect that the type checking for output parameters is done "the other way around".

I suppose these declarations are equivalent (because there is only a single parameter of type Dom):

Code: Select all

class predicates     pA : (Dom)         where Dom supports integer.   class predicates     pB : (integer).
Likewise I would expect that in the case of an output parameter these are equivalent:

Code: Select all

class predicates     qA : (Dom [out])         where Dom supports integer.   class predicates     qB : (integer [out]).
And, when type checking is done this way, the declaration of p2 should be equivalent to (and should thus compile):

Code: Select all

class predicates     p2B : (integer) -> integer.
Regards Martin

User avatar
Thomas Linder Puls
VIP Member
Posts: 2422
Joined: 28 Feb 2000 0:01

Re: Bounded polymorphism problem

Unread post by Thomas Linder Puls » 29 May 2019 9:35

I fully agree regarding pA.

But qA is a completely different story.

With your bound you have declared a predicate which given any subtype Dom of integer returns a value in that type.

Such a predicate is very hard to implement (without having access to the actual type of Dom).

The statement about qA would be correct if the bound was in the other direction:

Code: Select all

...         where integer supports Dom.           % illegal: Visual Prolog does not support bounds in that direction
I am not sure if a mathematic reference helps or interest you, but... The type of a predicate is contravariant in the types of input arguments, and covariant in type of output arguments and the return type. This means that all sub/super type considerations are the completely opposite (dual) for these kinds of arguments.
Regards Thomas Linder Puls
PDC

Martin Meyer
VIP Member
Posts: 276
Joined: 14 Nov 2002 0:01

Re: Bounded polymorphism problem

Unread post by Martin Meyer » 29 May 2019 18:58

Yes, covariant/contravariant is a very good hint. I had not known these terms. You are always a great source of information.

Like you said, a predicate type is covariant in the type of its output arguments. It seems however that by the semantics "a predicate which given any subtype Dom of integer returns a value in that type" of where Dom supports integer, predicate qA is treated contravariant in the Dom output argument.

The result of contravariance in an output argument is that bounded polymorphism is not applicable to output parameters at all. I have tried all (below three) cases to apply it to object output arguments, but the compiler refuses them all:

Code: Select all

interface superType end interface superType   class superType : superType end class superType   implement superType end implement superType   %===   interface subType supports superType end interface subType   class subType : subType end class subType   implement subType end implement subType   %===   implement main   class predicates     oA : (Type O [out])         where Type supports superType. clauses     oA(O) :-         O = subType::new().  % super/sub   %---   class predicates     oB : (Type O [out])         where Type supports subType. clauses     oB(O) :-         O = superType::new().  % sub/super   %---   class predicates     oC : (Type O [out])         where Type supports superType. clauses     oC(O) :-         O = superType::new().  % super/super
Hence my conclusion is: With the current semantics (the one you stated) p from my initial examples is the bug, while the errors in p1 and p2 are correct. But the semantics should be changed, so that bounded polymorphism can also be used on output parameters.
Regards Martin

Martin Meyer
VIP Member
Posts: 276
Joined: 14 Nov 2002 0:01

Re: Bounded polymorphism problem

Unread post by Martin Meyer » 30 May 2019 13:52

I said "The result of contravariance in an output argument is that bounded polymorphism is not applicable to output parameters at all." But now I realized, that is wrong because it works this way:

Code: Select all

class predicates     pInOut : (Dom, Dom [out])         where Dom supports integer. clauses     pInOut(X, X).
Thus my above conclusion is not correct either. Indeed the current semantics is sensible also for output parameters.

Even in the p example the compiler is not doing very wrong. Because the type mismatch will be detected at runtime:

Code: Select all

class predicates     p : () -> Dom         where Dom supports integer. clauses     p() = 1 + 0.   domains     dom = integer [2..10].   clauses     run() :-         hasDomain(dom, X),         X = p(), % raises runtime error: The value '1' is not in range [2 .. 10] of the domain 'main::dom'         stdIO::write(X).
So, my new conclusion is: Bounded polymorphism is working fine, thank you for patience and support!
Regards Martin

Post Reply