[mercury-users] 're-creating' higher order insts?

[Ondrej Bojar]

Mark Brown wrote:
> This is on the right track.  You want something like
> 
> :- pred assert_function_is_inst_foo(..., func_type::in, func_type::out(foo))
> 	is {semi,}det.

Exactly. It's just my limited English (or possibly any natural language skills) 
that I needed that many words. I should have written Mercury instead. :-)

> 1) You can replace the static checking with dynamic checking.  Your
> application will have a fixed set of insts that it is interested in, so
> you can create a type to describe every possible inst.  Then construct a
> value of this type each time you put a function in the ADT, and make sure
> you keep track of which value goes with with function (e.g., by packaging
> them up in the same term).  You can pass this information in the ... part
> of the assert_function_is_inst_foo predicate, above, which can throw an
> exception or fail if it is anything other than "foo".

I understand this technique, but I don't see how to do the final assert. Or is
this definition of the assert_function_is_inst_foo above valid?

assert_function_is_inst_foo(..., Func, Func).

I'd expect to need some magical promise_I_know_the_inst_better_than_you call.


Indeed, the compiler given:

:- type foo == (pred(int)).
:- inst foo == (pred(out) is det).

:- pred assert(foo::in, foo::out(foo)) is det.
assert(Foo, Foo).


complains:

clip.m:008: In clause for `assert(in, out((clip.foo)))':
clip.m:008:   mode error: argument 2 did not get sufficiently instantiated.
clip.m:008:   Final instantiatedness of `Foo' was `ground',
clip.m:008:   expected final instantiatedness was `(pred((free >> ground)) is
clip.m:008:   det)'.

> 2) If you are feeling courageous, you can replace static checking with no
> checking.  For some purposes this may be safe enough (e.g. if the whole
> module only uses one higher-order inst, you aren't so likely to get it
> wrong).  It would seg fault if you got it wrong, though.

Yes, but I still have the problem above.

Thanks, Ondrej.

-- 
Ondrej Bojar (mailto:obo at cuni.cz / bojar at ufal.mff.cuni.cz)
http://www.cuni.cz/~obo
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------