Spelling errors in pattern matches

heatherleaf commented 5 years ago

GF doesn't make any syntactic distinction between how parameters, functions and variables are written. There is a convention that parameters should be capitalised, but functions and variables be lower-cased, but it's not enforced. This leads to problems, here is an example:

abstract TestAbs = {
cat S; B;
fun sOk, sBug : B -> B -> S;
fun bTrue, bFalse : B;
}
concrete Test of TestAbs = {
param Bool = True | False;
lincat S = {s : Str};
lincat B = {s : Str; b : Bool};
lin sOk x y = {s = x.s ++ y.s ++ case <x.b, y.b> of {
        <True, False> => "<TrueFalse>" ;
        <_,    _    > => "" 
}};
lin sBug x y = {s = x.s ++ y.s ++ case <x.b, y.b> of {
        <True, Fasle> => "<TrueFasle>" ;
        <_,    _    > => "" 
}};
lin bTrue  = {s = "True"; b = True};
lin bFalse = {s = "False"; b = False};
}

The only difference is that False is misspelled in sBug. Here's the result:

> i -src Test.gf
- compiling TestAbs.gf...   write file TestAbs.gfo
- compiling Test.gf...   write file Test.gfo
linking ... OK

TestAbs> gt sOk ? ? | l
False False
False True
True False <TrueFalse>
True True

TestAbs> gt sBug ? ? | l
False False
False True
True False <TrueFasle>
True True <TrueFasle>

The misspelling of Fasle makes it a parameter variable which then captures <True,True> too, which was not intended. This bug is very difficult to catch, because GF didn't print any warning at all.

How can we capture these errors better?

heatherleaf commented 5 years ago

I have a solution too! 🥇

I don't suggest the Haskell way: to require parameters to be capitalised and variables lower-cased. But I suggest that we make it explicitly recommended:

Print a warning whenever a parameter is defined non-capitalised, and whenever a variable is capitalised. (Let functions be either, because the RGL is sprinkled with capitalised functions)
(Optional) Add a per-module compiler flag for suppressing these warnings (can be useful for old modules that do not follow the recommendation)

johnjcamilleri commented 5 years ago

I like the idea of warnings to encourage conventions. Are you saying this should be implemented in the compiler for all GF grammars, or somehow targeted only at the RGL?

Rather than build this into the compiler, we could also imagine a separate gflint tool. This is very common with other languages, eg. HLint for Haskell. Implementing this shouldn't be too hard using GF-as-a-library and having it separate from the compiler is probably good from a separation of concerns point of view. Not least because it's recently been discussed that the GF error messages need a bit of an overhaul.

heatherleaf commented 5 years ago

I like the idea of warnings to encourage conventions. Are you saying this should be implemented in the compiler for all GF grammars, or somehow targeted only at the RGL?

This is dangerous and hard-to-catch for all GF grammars, not just the RGL

Rather than build this into the compiler, we could also imagine a separate gflint tool.

That's also a possibility of course. But I think this is more severe than many of the current warnings that the compiler generates (e.g., about missing lock fields), so either move all warnings to the gflint tool, or have them in the compiler. Whatever has the highest chance of getting implemented :)

johnjcamilleri commented 5 years ago

You're saying this is "severe" as if it's a bug in GF, but in truth it is a feature of the language. That it can lead to hard to find errors is just an unfortunate side-effect. I don't agree that a warning about this is "more serious" than other GF warnings.

heatherleaf commented 5 years ago

You're saying this is "severe" as if it's a bug in GF, but in truth it is a feature of the language. That it can lead to hard to find errors is just an unfortunate side-effect.

Let's say it's a very unfortunate feature of the language...

I don't agree that a warning about this is "more serious" than other GF warnings.

This is of course debatable and I guess that discussion won't lead to anything useful. Let me rephrase to:

The warning I suggest is as important as the current warnings that the compiler generates, because it can catch serious grammar bugs just as the current warnings can. (E.g., "patterns never reached", "no linearization of X", "function X is not in abstract", "missing lock field")

aarneranta commented 5 years ago

The general form of a warning could be: later patterns overshadowed. This is how it is in GHC, since just separating upper and lower case does not capture all overshadowing.

I also think that such a warning be better than forcing some conventions that are not language features: lint would be a more proper place for such conventions.

A historical note:

The feature of not separating between constructor and other id's has a long history: GF was designed on the basis of ALF, which in turn was inspired by ML. Some of the early GF code was directly translated from such old code. Agda also still has this freedom.

When I saw Haskell's identifier classes I found it to be a severe restriction on the freedom of speech, i.e. on using whatever identifiers come out naturally and/or are traditionally used. Later I have come to appreciate some of the advantages of the added control from upper vs. lower-case identifiers, in particular the avoidance of (some of) the risk of overshadowing.

Aarne.

From: John J. Camilleri notifications@github.com Sent: Thursday, May 16, 2019 9:58:20 AM To: GrammaticalFramework/gf-rgl Cc: Subscribed Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

You're saying this is "severe" as if it's a bug in GF, but in truth it is a feature of the language. That it can lead to hard to find errors is just an unfortunate side-effect. I don't agree that a warning about this is "more serious" than other GF warnings.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/GrammaticalFramework/gf-rgl/issues/240?email_source=notifications&email_token=AAWBQXLCDUWREG254AVEZO3PVUHZZA5CNFSM4HNDB5T2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVQ73YA#issuecomment-492961248, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AAWBQXIMQHLS7WJY3TRMS3LPVUHZZANCNFSM4HNDB5TQ.

aarneranta commented 5 years ago

Now I see that the overshadowing warning is already there ;-)

Maybe we should just promote this to an important warning and tune down some less important ones (e.g. lock fields). This could be done by using verbosity levels.

Aarne.

From: Aarne Ranta Sent: Thursday, May 16, 2019 10:11:54 AM To: GrammaticalFramework/gf-rgl; GrammaticalFramework/gf-rgl Cc: Subscribed Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

The general form of a warning could be: later patterns overshadowed. This is how it is in GHC, since just separating upper and lower case does not capture all overshadowing.

I also think that such a warning be better than forcing some conventions that are not language features: lint would be a more proper place for such conventions.

A historical note:

The feature of not separating between constructor and other id's has a long history: GF was designed on the basis of ALF, which in turn was inspired by ML. Some of the early GF code was directly translated from such old code. Agda also still has this freedom.

When I saw Haskell's identifier classes I found it to be a severe restriction on the freedom of speech, i.e. on using whatever identifiers come out naturally and/or are traditionally used. Later I have come to appreciate some of the advantages of the added control from upper vs. lower-case identifiers, in particular the avoidance of (some of) the risk of overshadowing.

Aarne.

From: John J. Camilleri notifications@github.com Sent: Thursday, May 16, 2019 9:58:20 AM To: GrammaticalFramework/gf-rgl Cc: Subscribed Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

You're saying this is "severe" as if it's a bug in GF, but in truth it is a feature of the language. That it can lead to hard to find errors is just an unfortunate side-effect. I don't agree that a warning about this is "more serious" than other GF warnings.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/GrammaticalFramework/gf-rgl/issues/240?email_source=notifications&email_token=AAWBQXLCDUWREG254AVEZO3PVUHZZA5CNFSM4HNDB5T2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVQ73YA#issuecomment-492961248, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AAWBQXIMQHLS7WJY3TRMS3LPVUHZZANCNFSM4HNDB5TQ.

heatherleaf commented 5 years ago

Now I see that the overshadowing warning is already there ;-) Maybe we should just promote this to an important warning and tune down some less important ones (e.g. lock fields). This could be done by using verbosity levels.

The problem with my example is that it doesn't trigger the overshadowing warning! (That's why I had to match over a pair of bools)

The misspelled Fasle just "steals" one of the three possible alternatives that would otherwise go to the catch-all. So currently, my example grammar doesn't generate any warning at all.

heatherleaf commented 5 years ago

I'm perfectly ok with a more complicated heuristics for generating warnings. Here is another alternative:

(my original suggestion) warn if a parameter is defined lowercased, and if a variable is upper-cased
(alternative) warn if a variable which doesn't start with _ is not used

One reason I suggested the first one is that it's probably extremely easy to implement. Just do a simple string check whenever a parameter is defined, and whenever a variable is created (in a lambda or a pattern match).

aarneranta commented 5 years ago

This seems to be simply a bug in the warning generator.

The conventions you suggest might make sense on a very high verbosity level. But issuing them by default would give lots of warnings on legacy code.

Aarne.

From: Peter Ljunglöf notifications@github.com Sent: Thursday, May 16, 2019 10:23:25 AM To: GrammaticalFramework/gf-rgl Cc: Aarne Ranta; Comment Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

Now I see that the overshadowing warning is already there ;-) Maybe we should just promote this to an important warning and tune down some less important ones (e.g. lock fields). This could be done by using verbosity levels.

The problem with my example is that it doesn't trigger the overshadowing warning! (That's why I had to match over a pair of bools)

The misspelled Fasle just "steals" one of the three possible alternatives that would otherwise go to the catch-all. So currently, my example grammar doesn't generate any warning at all.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/GrammaticalFramework/gf-rgl/issues/240?email_source=notifications&email_token=AAWBQXJ6AEQU2BB6IV4DAP3PVUKX3A5CNFSM4HNDB5T2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVRB4MI#issuecomment-492969521, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AAWBQXOMF764SOXOGREYYDLPVUKX3ANCNFSM4HNDB5TQ.

aarneranta commented 5 years ago

Sorry for a mistake in my previous comment: this is not a bug, because the pattern <,> is reached by <False,True> for instance. Hence the overshadowing analysis is not sufficient to capture errors like this.

Aarne.

From: Aarne Ranta Sent: Thursday, May 16, 2019 10:31:41 AM To: GrammaticalFramework/gf-rgl; GrammaticalFramework/gf-rgl Cc: Comment Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

This seems to be simply a bug in the warning generator.

The conventions you suggest might make sense on a very high verbosity level. But issuing them by default would give lots of warnings on legacy code.

Aarne.

From: Peter Ljunglöf notifications@github.com Sent: Thursday, May 16, 2019 10:23:25 AM To: GrammaticalFramework/gf-rgl Cc: Aarne Ranta; Comment Subject: Re: [GrammaticalFramework/gf-rgl] Spelling errors in pattern matches (#240)

Now I see that the overshadowing warning is already there ;-) Maybe we should just promote this to an important warning and tune down some less important ones (e.g. lock fields). This could be done by using verbosity levels.

The problem with my example is that it doesn't trigger the overshadowing warning! (That's why I had to match over a pair of bools)

The misspelled Fasle just "steals" one of the three possible alternatives that would otherwise go to the catch-all. So currently, my example grammar doesn't generate any warning at all.

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/GrammaticalFramework/gf-rgl/issues/240?email_source=notifications&email_token=AAWBQXJ6AEQU2BB6IV4DAP3PVUKX3A5CNFSM4HNDB5T2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVRB4MI#issuecomment-492969521, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AAWBQXOMF764SOXOGREYYDLPVUKX3ANCNFSM4HNDB5TQ.

heatherleaf commented 5 years ago

Sorry for a mistake in my previous comment: this is not a bug, because the pattern <,> is reached by <False,True> for instance. Hence the overshadowing analysis is not sufficient to capture errors like this.

Exactly!

Perhaps my second suggestion is better? To issue a warning if a (named) variable is not used. That would capture most misspellings (unless you misspell the same thing twice)

GrammaticalFramework / gf-rgl

Spelling errors in pattern matches #240