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

[Marshall]

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.


Marshall