Can we warn about curly braces in mistyped expression-level ifs?

[cpitclaudel]

Multiple Dafny users have been bit by the following paper cut:

function method OneOrTwo(b: bool): int {
  if b then {
    1
  } else {
    0
  }
}

Error: Function body type mismatch (expected int, got set<int>)

The problem we have here is that statement if takes curly braces, but expression if doesn't (and there, curly braces mean a set).

We can probably make this a bit better: if we see a mismatch between set<T> and T in the branches of an expression if, we can add a note to the error that says that expression-level if doesn't take braces.

[kjx]

Once again: what's going on here is a bit deeper - I think there's a longstanding misdesign around Dafny's if (whether or not to include an then); and probably the way "{}" are overloaded both as set syntax and block delimiters.

I do appreciate I'm probably the only person who thinks revisiting this is worthwhile:
but I encourage the team to think about doing that for a next major release.

[keyboardDrummer]

How do we feel about replacing the if expression with a ternary operator? Having two syntactically similar but different if constructs seems highly confusing. I understand the desire to reuse concepts such as if as much as possible in the language, but here that doesn't seem to work out well because of the overloading of braces.

The alternative language change would be reserving {} strictly for statement blocks, but I like that less.

[cpitclaudel]

How do we feel about replacing the if expression with a ternary operator?

Not good: chained ternary operators look really bad, and long chains of if/else if are pretty common in Dafny.

[kjx]

I guess Dafny has a ternary operator - or at least a ternary expression - it's just that the syntax is if E then T else F rather than E -> T ; F or (if E T F)

Making the expression and statement forms of "if" consistent wrt "then" seems an obvious move.
I'd keep it in both, but you don't have to.

handling sets vs whatever-else-brackets-are-used-for is trickier. I'm happy to discuss options if/when people are interested --- or I could bid to do a syntactic redesign for an amazon reasoning award, instead of what I'm planning on (library design stuff) --- but I can see a number of different design options here that may be worth exploring, all of which would reduce or eliminate overloading "{}", but in different ways.

I don't know if you've aware of the more "Pythonic" syntax in Scala-3 --- I'm not a Scala programmer by any means! --- but I think there efforts are at least interesting.

https://dotty.epfl.ch/docs/reference/other-new-features/indentation.html

https://dotty.epfl.ch/docs/reference/other-new-features/control-syntax.html

[cpitclaudel]

Making the expression and statement forms of "if" consistent wrt "then" seems an obvious move.

A counterpoint might be that the braces are unnecessary, since 1. we already have parentheses, and 2. there can be at most one expression per branch of an if?

On the other hand, expression-level matches are allowed to use braces:

function method M() : int {
  match 0 {
    case 0 => 1
    case _ => 2
  }
}

[MikaelMayer]

What about

if condition {
  then X
  else Y
}

? That way, it would work both for statements and expressions the same :-P

[cpitclaudel]

That way, it would work both for statements and expressions the same :-P

How would it work for statements?

[MikaelMayer]

if condition {
  then
    var x := 1;
    print x;
    return 1;
  else
   var y := 1;
   assert y == 2;
   return 2;
}

[keyboardDrummer]

Maybe it would be enough to have an automatic formatter that changes:

function method OneOrTwo(b: bool): int {
  if b then {
    1
  } else {
    0
  }
}

into

function method OneOrTwo(b: bool): int {
  if b then { 1 } else { 0 }
}

Note that this would require modifying newlines which the upcoming formatter doesn't do

[keyboardDrummer]

What about

if condition {
  then X
  else Y
}

? That way, it would work both for statements and expressions the same :-P

I think that's brilliant! It's similar to how match syntax currently already solves this problem.

We would have the following symmetry:

method Match(x: bool) returns (r: int)
{
  match x {
    case true => r := 0;
    case false =>
      var v1 := 3;
      r := v1;
  }
}

method If(x: bool) returns (r: int)
{
  if x {
    then r := 0;
    else
      var v1 := 3;
      r := v1;
  }
}

The downsides I see are:

• More braces in expressions than necessary
• Different type of if syntax than other languages use
• The lack of braces around if and case blocks is inconsistent with other blocks

However, I think having the exact same syntax for expression and statement ifs is a huge win. Having similar syntax between the two ifs is confusing, and having very different syntax means having to learn the same concept with two pieces of syntax.