3 ms·

Shouldn't the 8th line of the example code read "requires release (op == CalcOp::add || op == CalcOp::sub) ==> arg 2 != none;" ? I'm assuming it's some kind of

• LudwigNagasena 3y ago
  Yeah, the second `CalcOp::add` should be replaced with `CalcOp::sub`, but `arg2 != none` is not redundant. The condition narrows `arg2` from `Int?` to `Int` when `CalcOp` requires two arguments. EDIT: Oops, I misread the comment. The following the following "check arg2 != none;" indeed seems redundant.
  • blixt 3y ago
    Since the example leads with: > Many features that make the Bosque IR amenable for automated reasoning involve simplifying and removing sources of irregularity in the semantics. I do find it strange that it both shows a bug in the logic which causes an irregularity, but also that this irregularity is allowed because of the need of a second check, rather than failing to compile because the type would be narrowed by the initial constraint (if the op argument is add/sub then arg2 MUST be non-none).
    • LudwigNagasena 3y ago
      Oh, I missed the line with the `check` keyword and misinterpreted the comment I replied to. Yes, it is indeed very strange.
      • mark_marron 3y ago
        Hmm, that is an unfortunate typo and I don't have access to the page any longer to fix it :( This example is from an earlier version of the language that was experimenting with aggressive flow sensitive typing. Interestingly, I came to the conclusion that, while sometimes magically nice, it was also often confusing. So, in the version that is (slowly) getting built as the first _release_ version has a simpler and more explicit algorithm.