Saying "latently-typed language" is making a category mistake

[Gabriel Dos Reis]

"Marshall" <marshall.spight at gmail.com> writes:

| David Hopwood wrote:
| >
| > A type system that required an annotation on all subprograms that do not
| > provably terminate, OTOH, would not impact expressiveness at all, and would
| > be very useful.
| 
| Interesting. I have always imagined doing this by allowing an
| annotation on all subprograms that *do* provably terminate. If
| you go the other way, you have to annotate every function that
| uses general recursion (or iteration if you swing that way) and that
| seems like it might be burdensome. Further, it imposes the
| annotation requirement even where the programer might not
| care about it, which the reverse does not do.

simple things should stay simple.  Recursions that provably terminate
are among the simplest ones.  Annotations in those cases could be
allowed, but not required.  Otherwise the system might become very
irritating to program with.

-- Gaby