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

[Marshall]

Gabriel Dos Reis wrote:
> "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.

Yes, exactly my point.


Marshall