Remove special cases for true, false, nil, ref

[myreen]

Special cases in the syntax for true, false, nil and ref are to be removed. true --> True false --> False nil -- delete; users are to write [] (alternatively keep it as Nil) ref --> Ref Combinators K, I, C in the basis are to become const, id, flip.

This is based on a discussion between @mn200, @SOwens, @xrchz and me on CakeML slack.

[myreen]

This issue should arguably also rename Some and None to SOME and NONE, because there is no reason to have the unusual mixed-case names.

[xrchz]

This issue should arguably also rename Some and None to SOME and NONE, because there is no reason to have the unusual mixed-case names.

No, please don't do that. This issue can be summarised as "reduce SML compatibility in favour of consistency". Note that "true, false, nil, ref" are all SML versions of constructors that break the consistent rule that a constructor is a capitalised word (not all-caps). "SOME" and "NONE" also break the rule and are used in SML. So "Some" and "None" are correct according to the direction of this issue, and what we talked about on Slack.

[myreen]

OK, I won't change Some and None to SOME and NONE.

[mn200]

Do you want to change the grammar to enforce that rule? And if so, what should it do with identifiers that are all upper-case?

[xrchz]

For the grammar rule, I'd like something like isConsName c <=> c <> "" /\ isUpper (HD c) /\ EVERY isLower (TL c). We might still quibble about that, in which case I'd say this issue is just to make the changes described in the original post, and can be closed when those are done -- we can discuss changes to the syntax rules in a separate issue.

[myreen]

With such a strict rule, one can't have BranchWide, BranchNarrow etc.

[xrchz]

Yes, I was thinking about how to handle multi-word constructors. I prefer underscores, so Branch_wide, Branch_narrow, etc., which one could get by changing the last conjunct of my proposed rule EVERY (\x. isLower x \/ x = #"_") c. But perhaps we'd like to rule out This___hastoo_man__y_underscores__ by defining is_snake_case, or isCamelCase if preferred.

isConsName c <=>
  let words = FIELDS ((=) #"_") c in
    words <> [] /\
    EVERY (\w. w <> "") words /\
    isUpper (HD (HD words)) /\ EVERY isLower (TL (HD words)) /\
    EVERY (EVERY isLower) (TL words)

[SOwens]

I think that CamelCase constructors are going to be popular enough that CakeML should support them in the concrete syntax.

Scott

On 2018/12/05, at 11:07, Ramana Kumar notifications@github.com wrote:

Yes, I was thinking about how to handle multi-word constructors. I prefer underscores, so Branch_wide, Branchnarrow, etc., which one could get by changing the last conjunct of my proposed rule EVERY (\x. isLower x \/ x = #"") c. But perhaps we'd like to rule out This_hastoo_many_underscores__ by defining is_snake_case, or isCamelCase if preferred.

isConsName c <=> let words = FIELDS ((=) #"_") c in words <> [] /\ EVERY (\w. w <> "") words /\ isUpper (HD (HD words)) /\ EVERY isLower (TL (HD words)) /\ EVERY (EVERY isLower) (TL words)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[xrchz]

I still prefer snake case and the formal predicate I most recently gave above. Things that are not allowed won't become popular, so the question is whether you anticipate complaints :) However, camel case does lend itself to a simple formalisation: isConsName c <=> c <> "" /\ isUpper (HD c) /\ EVERY isAlpha (TL c).

[mn200]

That CamelCase formalisation doesn't then preclude SOME...

[xrchz]

Indeed, but only because I don't want the formalisation to be with respect to an allowed words list. The intent is that SOME would mean 4 words S, O, M, and E. If you want just 1 word, it should be Some. Again I affirm that I prefer snake case S_o_m_e over camel case SOME, because it's less confusing when there are single letter words. (Another example: InARow vs In_a_row.)

[mn200]

I am happy to change the relevant definition whenever someone figures out the final verdict. @xrchz's most recent suggestion forbids underscores, which I guess isn't the intention...

[xrchz]

I disagree with that claim. The most recent isConsName I gave above is intended to describe snake case with a single initial capital, e.g., This_is_allowed but TheseAre not_allowed. I checked it again and still think it's correct. Separately, I suspect we may want to also allow digits wherever we allow lowercase letters. EDIT: Oops! It's not the "most recent". sorry. It's the one that uses the variable words that I'm talking about.

[myreen]

This is the suggestion I made on slack that started the discussion about true, false, etc.

isConsName s =
  if s ∈ {"true"; "false"; "nil"} then T else
  if EVERY (λc. MEM c "_'" ∨ isDigit c ∨ (isAlpha c ∧ isUpper c)) s then F else
  if s ≠ "" ∧ isAlpha (HD s) ∧ isUpper (HD s) then T else F

@xrchz complained:

I'm not super keen on the new rule for two reasons. It seems complicated and ad hoc, and it encourages all caps.

I agree that my rule is a bit complicated and I too think the first line if s ∈ {"true"; "false"; "nil"} then T else shouldn't be there (as is the main purpose of this issue).

However, @xrchz 's suggestions, below, certainly seems "complicated and ad hoc" to me.

isConsName c <=>
  let words = FIELDS ((=) #"_") c in
    words <> [] /\
    EVERY (\w. w <> "") words /\
    isUpper (HD (HD words)) /\ EVERY isLower (TL (HD words)) /\
    EVERY (EVERY isLower) (TL words)

Why can't we have something really simple as follows and then just encourage good names by good examples and good defaults (Some, Greater, True, etc.)?

isConsName s <=> 
  s <> "" /\ isUpper (HD s) /\ EVERY (\c. c = #"_" \/ isAlpha c \/ isDigit c) s

[myreen]

I guess we would also like to have a isVarName function, where the isUpper is swapped for isLower for the first character:

isVarName s <=> 
  s <> "" /\ isLower (HD s) /\ EVERY (\c. c = #"_" \/ isAlpha c \/ isDigit c) s

My suggestions do not allow ' in variable or constructor names. I guess these definitions should be tweaked to allow ' characters wherever digits are allowed

[xrchz]

Is this issue done or not? What more needs to be done? As I suggested above, I think we should discuss the grammar rule separately, and focus on removing special cases for this issue.

[xrchz]

@myreen do you know the answer to the question above?

[myreen]

@xrchz I agree that the general discussion about the grammar rule should be continued separately from this issue. To answer your direct questions (I didn't realise they were for me):

Is this issue done or not? What more needs to be done?

No, this issue is not done. The only thing that has happened is that "Combinators K, I, C in the basis are to become const, id, flip." That's what 991b0b2 achieved.

I was under the impression that @mn200 would do "Special cases in the syntax for true, false, nil and ref are to be removed", which still remains to be done.

[xrchz]

I have attempted to progress this. I hope @mn200 can check my commit above and finish whatever remains.

[myreen]

The syntax [] should not map to Nil (or nil), since it just confuses everyone. The list constructor names ought to be [] and ::, in my opinion.

[mn200]

Mapping [] to the id Short "[]" is fine as far as it goes, but it would be nice to have a syntax for qualified reference. Previously I could write List.nil. Do we give up on this? (Totally can give up on it, btw)

[xrchz]

Yeah just give up on it, I think.

[myreen]

Closed by 7c269f545326201a646f694067a9d32ce3ffc837