|
Notes |
|
|
(0000831)
|
|
mark
|
|
2015-07-06 17:28
|
|
How do you think this ought to be compiled? What type should MaybeBDD have, for example?
The error message can be improved: you had to figure out what TypeInfo_25 was, and both line numbers refer to the containing disjunction instead of the disjuncts. Also, it's a try goal not a disjunction. But I think the general idea is right, in that the type was bound in one branch and not in another.
This issue applies to an existential type escaping from any form of disjunct. I'll upload a simplified case. |
|
|
|
(0000832)
|
|
pbone
|
|
2015-07-06 19:28
|
|
I think that this can be compiled correctly, if unintuitive. If MaybeBDD is typed as some [E] maybe_error(bdd(V), {string, E}).
It will become unintuitive if the exception type appears in the head of the clause, that will require the predicate to be existentially typed. |
|
|
|
(0000833)
|
|
mark
|
|
2015-07-06 23:42
|
|
To put the question another way, what would be the output of calling io.write(type_desc.type_of(MaybeBDD), !IO)? What's in the type_desc for E?
For the error branch, the type_desc is obviously meant to be whatever type_desc the exception value had. But for the ok branch, the type_desc is not provided anywhere. That's more or less what the compiler error message is trying to say.
Note that a similar idiom to those documented in the Existential Types chapter also applies here, namely, wrap ExpPrime in a univ:
catch_any ExpPrime ->
MaybeBDD = error({"My message", univ(ExpPrime)}) |
|
|
|
(0000834)
|
|
pbone
|
|
2015-07-07 10:29
|
|
I tried breaking the predicate into two parts so that I can put the try goal in a predicate that explicitly returns an existential type. (My idea is that the types should be named apart and the type of the exception should be set when MaybeBDD is unified with error and deconstructed.
:- some [E] pred test_try(bexpr(V)::in, maybe_error(bdd(V), {string, E})::out)
is det.
test_try(BooleanExpression, MaybeBDD) :-
promise_equivalent_solutions [MaybeBDD] (
( try []
BDDPrime = make_bdd(BooleanExpression)
then
MaybeBDD = ok(BDDPrime)
catch_any ExpPrime ->
MaybeBDD = error({"My error message", ExpPrime})
)).
test2(BooleanExpression, !IO) :-
test_try(BooleanExpression, MaybeBDD),
( MaybeBDD = ok(BDD)
; MaybeBDD = error({ErrMessage, _}),
% This deconstructon should determine the type of the error.
write_string(ErrMessage, !IO),
sorry($pred, "Error")
),
io.write(BDD, !IO).
But this doesn't work. and using `new error` doesn't work because error is not existentially typed itself. (I'm learning more about existential types BTW.)
:- type maybe_error(T)
---> ok(T)
; some [E] error(string, E).
test2(BooleanExpression, !IO) :-
promise_equivalent_solutions [MaybeBDD] (
( try []
BDDPrime = make_bdd(BooleanExpression)
then
MaybeBDD = ok(BDDPrime)
catch_any ExpPrime ->
MaybeBDD = 'new error'("My error message", ExpPrime)
)),
( MaybeBDD = ok(BDD)
; MaybeBDD = error(ErrMessage, _),
% This deconstructon should determine the type of the error.
write_string(ErrMessage, !IO),
sorry($pred, "Error")
),
io.write(BDD, !IO).
This works, it solves the problem in the same way as your use of univ. I've learnt that if I want the type of the error to be determined when error is deconstructed, then I need error to have the existential type applied to it. (Or univ, if I want it a little later).
We can make it a type error for the type of an exception to escape the catch_any branch. Or indeed any branching structure, this will allow us to produce a better error message. Do you agree? is a type error the way to go here? (My reasoning is that the program is incorrectly typed.) |
|
|
|
(0000835)
|
|
pbone
|
|
2015-07-07 10:29
|
|
|
|
|
(0000836)
|
|
mark
|
|
2015-07-07 14:58
|
|
Breaking it into two parts better illustrates why this is a program error, not just a compiler bug. The signature says that there is "some" type, which means that this predicate is responsible for producing that type (see "Semantics of type quantifiers" in the reference manual). But the programmer only provides that type in the catch_any clause, not in the then clause, hence the "mode" mismatch.
The compiler could fill in the type as 'void', like in other circumstances, but this doesn't seem a good idea. If the programmer has provided a type in at least one branch of a branched structure, they ought to do so in all branches. In any case the compiler's use of 'void' would generate a warning.
Which brings us to a different problem: there is no way to give different types in different branches anyway, because that would be a type error. So the following won't work:
( X = 1 ; X = "foo" ), io.write(X, !IO)
Instead you must push the polymorphic calls inside the branches:
( X = 1, io.write(X, !IO) ; X = "foo", io.write(X, !IO) )
or else you can "box" the existential type:
( X = 1, UX = univ(X) ; X = "foo", UX = univ(X) ),
io.write(univ_value(UX), !IO)
So, regarding your last question, if the programmer does address the "mode" error by providing a type for every branch (or none), then with the current language they will already necessarily receive a "type" error, as the existential type in one branch is opaque and cannot be referred to in the other branches.
I don't think it matters much whether these are called mode errors or type errors. Given that the type quantifier determines where a type is produced, the two concepts amount to the same thing as far as checking the quantifiers is concerned. |
|
polymorphism_try_bug.m (1,608) 2015-07-06 12:50