Typechecking of subtraction with natural numbers

[jameseb7]

Currently, the type system for RoboChart defines the type of a subtraction applied to two natural numbers to be of the integer type. While this makes sense due to the fact the result could be negative, it prevents using the result as part of a counting down pattern such as count = count - 1, where count has type nat. Here count may never actually go negative, and showing that it does not go negative is a separate proof obligation, but the pattern in general is not erroneous. It may be better to allow the result of subtracting naturals to be a natural, and let FDR reject cases where the number goes outside the bounds of the natural number type.

[alvarohm]

I think this issue will be dealt with when I separate the type checker into the Z type checker and an extra type checker. In the Z type checker, the type of both count and count - 1 would be Arithmos and there would be no error. In the extra type checker, we can keep this rule but give a warning instead of an error. This extra type checker would allow validations that are either helpful to the user or necessary for the csp generator.

…

On Wed, 19 May 2021 at 13:48, James Baxter ***@***.***> wrote: Currently, the type system for RoboChart defines the type of a subtraction applied to two natural numbers to be of the integer type. While this makes sense due to the fact the result could be negative, it prevents using the result as part of a counting down pattern such as count = count - 1, where count has type nat. Here count may never actually go negative, and showing that it does not go negative is a separate proof obligation, but the pattern in general is not erroneous. It may be better to allow the result of subtracting naturals to be a natural, and let FDR reject cases where the number goes outside the bounds of the natural number type. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#32>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABEHMYPNVJC6OZLEXQNQJR3TOOXRPANCNFSM45ETGUWA> .