Lower bound viewtype errors

I think I’ve come across this error before, but I’m not sure or don’t
recall what it means (error line in yellow):

/media/RAID5/share/ATS_learning/minDisj.dats: 23248(line=817, offs=24) –
23255(line=817, offs=31): error(3): sort mismatch: the sort of [s2V(3163)]
is [t@ype], but the sort of its lower bound is [viewtype].
/media/RAID5/share/ATS_learning/minDisj.dats: 23248(line=817, offs=24) –
23255(line=817, offs=31): error(3): mismatch of static terms (tyleq):

implement
minConj(gr, emap): GREXP = let
macdef d2g(gr) = let
val rgr = case+ ,(gr) of
| GRgenes(gs) => GRgenes(gs)
| GRconj(gs) => GRgenes(gs)
| GRdisj(gs) => let
val dsz = int_of_size(genes_size(gs))
val rgr1 = if 1 = dsz then GRgenes(gs)
else ($raise InvalidCase; GRdisj(gs))
in rgr1 end
| X => X
in rgr end
in (case+ gr of
| ~GRconj(ex1,ex2) => let
val (ex1,ex2) = (d2g(ex1),d2g(ex2))
in (case+ (ex1,ex2) of
| (~GRgenes(s1), ~GRgenes(s2)) => minConj(GRconj (s1+s2),emap)
| (~GRconj(ex11, ex12), ex2) =>
minConj(GRconj(minConj(GRconj(ex11, ex12),emap),ex2),emap)
| (ex1, ~GRconj(ex21, ex22)) =>
minConj(GRconj(ex1, minConj(GRconj(ex21, ex22),emap)),emap)
| (LL,RR) => GRconj(LL,RR)
):GREXP end
| ~GRconj(gs) => let
val glist = genes_listize(gs)
val mingene = list_min(glist, emap)
val _ = genes_free(gs)
in GRconj(genes_make_sing(mingene)) end
| X => X
): GREXP
end // end of [minConj]

First, I do see what you are saying about this getting a little out of
hand. Sorry for being obtuse … I know you mentioned a reference-counted
absviewtype previously; are there any relevant examples (assuming I can do
this without a drastic rewrite of the code)?

I know I said I was basically done with this, it is just that minor changes
and bugs keep popping up (as they always seem to).

OK, that issue is solved, I’ll try and be more careful with case/ifs.

I am wondering the best way to tackle this problem from the same code:
extern
fun print_pretty_grexp (grexp: !GREXP): void

implement
minConj(gr, emap): GREXP = let
fun d2g(gr:GREXP): GREXP = let
val rgr = (case+ gr of
| ~GRgenes(gs) => GRgenes(gs)
| ~GRconj(gs) => GRgenes(gs)
| ~GRdisj(gs) => let
val dsz = int_of_size(genes_size(gs))
val rgr1 = (if 1 = dsz then GRgenes(gs)
else (print_pretty_grexp(GRdisj(gs));
$raise InvalidCase; GRdisj(gs))): GREXP
in rgr1 end
| X => X): GREXP
in rgr end

Is it to just create a val binding for GRdisj(gs)?

I have to say that I don’t see an easy way to fix your code.

Maybe turning GREXP into a datatype is the best way to go.

A very typical scenario in practice can be described as follows.
A programmer often picks a data representation at the beginning when he
knows very little about what he really needs. He uses the representation
and starts to find problems with it. However, he has no easy way to change
the data representation as doing so would require a lot of code to be
re-written.
So he bites the bullet and spends more and more of his time on debugging.

Properly using abstract types in ATS is a highly effective way to fight the
above issue.

Using datatype for GREXP makes a lot sense. But why did you use
dataviewtype for GREXP? Because you did not want to have GC running?

For the sake of completeness, the code was easy to fix using a binding as I
guessed, but it does make things look far more complex:

  | ~GRdisj(gs) => let
      val dsz = int_of_size(genes_size(gs))
      val rgr1 = (if 1 = dsz then GRgenes(gs)
        else let
          val gr = GRdisj(gs)
        in (print_pretty_grexp(gr);
          $raise InvalidCase; gr)
        end): GREXP
    in rgr1 end
  | X => X): GREXP

In general, a case-expression or if-expression should be annotated with a
type.

Unfortunately, a macdef in ATS cannot involve types (but it can in ATS2).
So I suggest that you turn d2g into a function.

I suggest that you use macros only in cases where using functions would be
inconvenient. As gcc (with -O2) does inlining
pretty aggressively, using macros so as to gain efficiency is rarely needed
if at all.

Honestly, I did it because I found out about linset and linmap but did not
know about funset and funmap, so I thought I had to have a dataviewtype.

As for exceptions, I’m just using them to track bugs right now as unhandled
exceptions - probably not the best style (thanks for pointing out that
memory leak complication though).

I see. Then switching GREXP to a datatype should be the right way to go.
I first thought that you just wanted to learn how to use dataviewtype.
Anyway,
you learned your lesson :slight_smile:

I suppose one thing I could do is to change my sets/maps to be
funsets/funmaps, but I’d still be working with a datatype (I guess this
particular problem would go away in that case).

I really think that this is an example that should persuade you not to make
GREXP a dataviewtype.
Pattern matching is supposed to help you write clean code. If you have to
fight the typechecker all the time,
then I think it may be time to change GREXP into an abstract viewtype.

By the way, linear types and exceptions usually don’t mix. Unless you have
strong justification, I would
suggest avoiding such a programming style.

–Hongwei

Yes, that is the right fix.

You have many lines like

case+ x of
| ~GRgenes (genes) => GRgenes (genes)

This means that you free a node and then create another node that is just
the same as the one freed.

A more efficient way to do this would be

case+ x of
| GRgenes _ => (fold@ (…); x) // fold@ is compiled into a no-op.