Page 1 of 1
Bounded polymorphism problem
Posted: 17 May 2019 15:54
by Martin Meyer
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'
Re: Bounded polymorphism problem
Posted: 18 May 2019 22:07
by Thomas Linder Puls
Thank you, we will look at it.
Re: Bounded polymorphism problem
Posted: 28 May 2019 13:03
by Thomas Linder Puls
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.
Re: Bounded polymorphism problem
Posted: 29 May 2019 0:17
by Martin Meyer
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.
Re: Bounded polymorphism problem
Posted: 29 May 2019 9:35
by Thomas Linder Puls
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.
Re: Bounded polymorphism problem
Posted: 29 May 2019 18:58
by Martin Meyer
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.
Re: Bounded polymorphism problem
Posted: 30 May 2019 13:52
by Martin Meyer
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!