Hi Laszlo
Laszlo Nemeth wrote:
Hi,
Could somebody please explain what to do about yellow question marks?
How can they arise in the first place? If I convinced the typechecker
that my program is total, what can go wrong? I'm trying to debug my
dead simple program(s): everything is green and yet all I get is '?'.
This usually means that the recursion-checker doesn't see why your
recursive call is ok. (Bug #1, the recursion checker should leave
suspicious calls with a yellow background, but it doesn't at the moment;
your program goes green after typechecking a dummy function for the
recursive call, then the machine tries to replace the dummy with an
appeal to an inductive hypothesis.)
------------------------------------------------------------------------------
( eq : all a : A => all b : A => Bool ; as, bs : List A !
let !--------------------------------------------------------!
! eqList eq as bs : Bool )
eqList eq as bs <= rec as
{ eqList eq as bs <= case as
{ eqList eq nil bs <= case bs
{ eqList eq nil nil => true
eqList eq nil (cons b bs) => false
}
eqList eq (cons a as) bs <= rec bs
{ eqList eq (cons a as) bs <= case bs
{ eqList eq (cons a as) nil => false
eqList eq (cons a as) (cons b bs)
=> eqListaux (eq a b) (eqList eq as bs) false
}
}
}
}
Am I making some stupid mistake? Why don't I get a value?
You're not making a stupid mistake, but you are unnecessarily triggering
the bug which is doing the real damage. Bug #2, if the recursion checker
is faced with a choice of inductive hypothesis, it can sometimes commit
too early to one possibility (I forget the circumstances where this
happens; it was a pretty hairy and hasty hack.). Your <= rec bs is
introducing such a choice, and it's disappearing down this hole. I agree
that it shouldn't, but that's what happens just now.
The workaround is just to delete the <= rec bs node from your program.
In any case, it isn't needed: recursion on the first argument is already
enough. I just tried and it sorts out the problem.
Epigram 1's recursion checker was fairly rapidly thrown together from
not quite the right pieces. It was what I had lying around at the time.
Not too hard to send the thing the wrong way. Given how little time I
have available for hacking, I'm afraid I can't promise to fix this bug.
I can promise not to make the same bug in Epigram 2.
Many apologies
Conor
