lower bound viewtype errors

[Brandon Barker]

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]

[gmhwxi]

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.

[Brandon Barker]

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)?

[gmhwxi]

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

[Brandon Barker]

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).

[Brandon Barker]

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).

[gmhwxi]

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?

[Brandon Barker]

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).

[gmhwxi]

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.

[gmhwxi]

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 :)

[Brandon Barker]

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

[gmhwxi]

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.