[m-users.] Some fun with insts

[Julian Fondren]

Hello,

I don't have a question this time. I just thought this was
interesting:

   :- module oop.
   :- interface.
   :- import_module io.
   :- pred main(io::di, io::uo) is det.
   :- implementation.
   :- import_module string, list.

   :- type class
       --->    mage
       ;       fighter
       ;       thief
       ;       cleric
       ;       wizard
       ;       warrior
       ;       ninja
       ;       priest.
   :- inst underclass for class/0
       --->    mage
       ;       fighter
       ;       thief
       ;       cleric.
   :- inst upperclass for class/0
       --->    wizard
       ;       warrior
       ;       ninja
       ;       priest.

   :- pred promote(class, class).
   :- mode promote(in(underclass), out(upperclass)) is det.
   :- mode promote(in, out) is semidet.
   promote(mage, wizard).
   promote(fighter, warrior).
   promote(thief, ninja).
   promote(cleric, priest).

   :- mode promote == ground >> underclass.
   :- pred promotable(class::promote) is semidet.
   promotable(mage).
   promotable(fighter).
   promotable(thief).
   promotable(cleric).

   main(!IO) :-
       M = mage,
       promote(M, W),
       io.format("%s promotes to %s.\n",
           [s(string(M)), s(string(W))], !IO),

       io.command_line_arguments(Args, !IO),
       ( if
           Args = [ClassStr],
           Term = ClassStr ++ ".",
           io.read_from_string("args", Term, length(Term),
               ok(Class), io.posn(0, 0, 0), _)
       then
           ( if promote(Class, Upper) then
               io.format("%s promotes to %s.\n",
                   [s(string(Class)), s(string(Upper))], !IO)
           else
               io.format("%s is already a promoted class!\n",
                   [s(string(Class))], !IO)
           ),

           ( if promotable(Class) then
               promote(Class, _),
               io.write_string("deterministic promote\n", !IO)
           else true )
       else
           io.progname_base("oop", Program, !IO),
           io.format(io.stderr_stream, "usage: %s <class>\n",
               [s(Program)], !IO),
           io.set_exit_status(1, !IO)
       ).

In particular, what's interesting is how this can fail.

1. what if you claim that a wizard is promotable?

   oop.m:041: In clause for `promotable((oop.promote))':
   oop.m:041:   mode error: argument 1 had the wrong instantiatedness.
   oop.m:041:   Final instantiatedness of `HeadVar__1' was
   oop.m:041:     bound(
   oop.m:041:       cleric
   oop.m:041:     ;
   oop.m:041:       fighter
   oop.m:041:     ;
   oop.m:041:       thief
   oop.m:041:     ;
   oop.m:041:       wizard
   oop.m:041:     ),
   oop.m:041:   expected final instantiatedness was
   oop.m:041:     named inst underclass,
   oop.m:041:     which expands to
   oop.m:041:       bound(
   oop.m:041:         cleric
   oop.m:041:       ;
   oop.m:041:         fighter
   oop.m:041:       ;
   oop.m:041:         mage
   oop.m:041:       ;
   oop.m:041:         thief
   oop.m:041:       ).

2. what if M (first line of main/2) is a wizard instead of a mage?

   oop.m:004: In `main'(di, uo):
   oop.m:004:   error: determinism declaration not satisfied.
   oop.m:004:   Declared `det', inferred `semidet'.
   oop.m:045:   Call to `oop.promote'(in, out) can fail.

3. what if promote(Class, _), which happens in the
    promotable(Class) test, is itself a test?

   oop.m:065: Warning: the condition of this if-then-else cannot fail.

4. what if the promotable(Class) test is negated?

   oop.m:004:   error: determinism declaration not satisfied.
   oop.m:004:   Declared `det', inferred `semidet'.
   oop.m:065:   Call to `oop.promote'(in, out) can fail.

5. what if instead of promoting mages into wizards, you have
    promote(mage, fighter) ?

   oop.m:034: In clause for `promote(in((oop.underclass)),
   oop.m:034:   out((oop.upperclass)))':
   oop.m:034:   mode error: argument 2 had the wrong instantiatedness.
   oop.m:034:   Final instantiatedness of `HeadVar__2' was
   oop.m:034:     unique(
   oop.m:034:       fighter
   oop.m:034:     ;
   oop.m:034:       ninja
   oop.m:034:     ;
   oop.m:034:       priest
   oop.m:034:     ;
   oop.m:034:       warrior
   oop.m:034:     ),
   oop.m:034:   expected final instantiatedness was
   oop.m:034:     named inst upperclass,
   oop.m:034:     which expands to
   oop.m:034:       bound(
   oop.m:034:         ninja
   oop.m:034:       ;
   oop.m:034:         priest
   oop.m:034:       ;
   oop.m:034:         warrior
   oop.m:034:       ;
   oop.m:034:         wizard
   oop.m:034:       ).

6. what if you promote a mage into a ninja?

   (no error)

but if you add another mode,

   :- mode promote(out(underclass), in(upperclass)) is det.

then the mage->ninja promotion starts to fail:

   oop.m:030: In `promote'(out($typed_inst(oop.class, (oop.underclass))),
   oop.m:030:   in($typed_inst(oop.class, (oop.upperclass)))):
   oop.m:030:   error: determinism declaration not satisfied.
   oop.m:030:   Declared `det', inferred `nondet'.
   oop.m:032:   Inside the case ninja/0 of the switch on HeadVar__2:
   oop.m:032:   disjunction has multiple clauses with solutions.
   oop.m:032:   The switch on HeadVar__2 does not cover
   oop.m:032:     `wizard'/0.

6. what if you have exhaustive but completely wrong promotions?

no error again:

   promote(mage, ninja).
   promote(fighter, priest).
   promote(thief, wizard).
   promote(cleric, warrior).

oh well. These predicate facts are readable enough that a domain
expert could look at the table and point out any errors without
having to know any programming at all. In practice that might be a
better win for correctness than something like

   // ATS, with correct promotions enforced by math
   datatype class(int) =
           | mage(0)   | fighter(1) | thief(2) | cleric(3)
           | wizard(4) | warrior(5) | ninja(6) | priest(7)

   fn promoteclass{n:int | n < 4}(job: class(n)): [m:int | m == n + 4] 
class(m) =
           case+ job of
           | mage() => wizard()
           | fighter() => warrior()
           | thief() => ninja()
           | cleric() => priest()

A more practical example of this kind of inst stuff might be a
state machine, where you can use insts to ward against invalid
state transitions.