Suggestions for the Shen

[Antti Ylikoski]

I have some development suggestions for the Shen system.

1.  There was an event when my editor had added one unprintable,
"invisible" character into the Shen source file.

This made the Shen type system infinite loop.  It was difficult to
discover the error.

2.  It eventuated that my editor had added one extraneous period "."
into the source file.

This also made the Shen type system infinite loop.

3.  As I have discussed, the bpropmll.shen file had a mystic case of
the Shen type system infinite looping.

A simple Unix lint type program / addition to the Shen reader could
have fixed the cases 1) and 2).  See

https://en.wikipedia.org/wiki/Lint_(software)

As to the case 3), I do realize that the problem of "finding out
whether there is an error there" is undecidable.  But it would be very
nice if the Shen type system could give some other error message, than
going into an infinite loop.

yours, AJY

[Mark Tarver]

TBoS 356-361 has a proof of the termination of the type checker w.o. user types.  However there is no method for detecting infinite loops in arbitrary theories; a corollary of the Turing equivalence of the type notation.

Mark