Opt-in static typing globally

[rockboynton]

Is your feature request related to a problem? Please describe.
My team is considering using Nickel for our config language, but we really like static typing, and want to make sure it is enforced when people outside of our immediate team try to change stuff. We would like a way to opt-in to enforce static typing globally, so for example we can have CI type-check the config and "you shall not pass" people if it doesn't check out.

Describe the solution you'd like
A simple solution is to just have a CLI flag to opt-in

Describe alternatives you've considered
Another idea that has been floated is to have a per-file pragma, but this might allow people to comment that out in a moment of frustration and still be able to merge.

Additional context
This idea was originally discussed on the Discord: https://discord.com/channels/1174731094726295632/1179430745727586407/1285771238618435605 (and following replies)

[yannham]

There's one remaining question though, if your use-case is really to prevent people from circumventing static typing. In Nickel, a contract annotation disables typechecking locally (cf relevant section of the manual).

This means that writing let my_awful_value_trust_me_its_a_number | Number = ...content... will pass the typechecker, even in a statically typed block, whatever ...content... is. On the bright side the Number contract is the security gate to enter the statically typed block; this contract will error out with a nice error message should it fail, before the variable is used in an actual numeric operation. Still, if ...content... does stupid things inside, they won't be caught statically by the typechecker.

One possibility is to have several levels of enforcement, and one where no matter what happens, any piece of code is always statically typechecked. But this might prove to be harder to use, because the language wasn't built with that idea in mind (some stdlib functions could be difficult to use, for example - see #2050). It really depends on the complexity of the configuration, though - in practice, most standard functions are entirely fine and the statically typed core should be as powerful as any basic functional language out there. And there are solutions (basically have a different, better-typed interface for some of those functions) as mentioned in #2050, and having such a strict typechecking mode could be a motivation to try to implement them.

In any case, most statically typed languages have escape hatch - Obj.magic in OCaml, unsafePerformWhatever in Haskell, unsafe in Rust, etc. - so maybe it's also fair to say that there will be an escape hatch but that such pattern in code reviews should be a red flag.

Another noteworthy point is that merging isn't statically typed currently either (this isn't necessarily impossible in theory, but it needs a non trivial evolution of the type system and some prior design work). Though if the merging happens on the CLI - you just write a bunch of .ncl files without explicit merging and then call nickel foo.ncl bar.ncl qux.ncl then you'll probably be fine.

As a side note, while static typing is really nice for functions, I think you can go very far (and actually farther than static typing for some properties) with proper contracts for your configuration data. You can run nickel eval it in the CI, and that should catch whatever errors you are trying to protect against, I believe.

[yannham]

(As another illustration of the "contract annotations disable typechecking" issue, someone could just take a whole .ncl file and put a ( <file_content>) | Dyn around it, negating the effect of the flag, which isn't very different from removing the pragma in term of friction)

[rockboynton]

for unsafe in Rust (and unsafePerformIO in Haskell), code is still typechecked though, it's not like you could do let i: u32 = unsafe { "foo" }. That may just be me being pedantic, and I understand what you are trying to say about having an "escape hatch", though.

I would be satisfied if it required removing or adding some obvious thing in order to disable typechecking so it would be hard to get through review (removing some --strict CLI argument in a CI script, a pragma line in the .ncl source, or adding the ( <file_content>) | Dyn thing you mentioned. I just don't want it to be a thing that can be done without knowing you are doing it, if that makes sense.

[yannham]

It's not useful to the conversation, but just because I wanted to write down this heresy, you can actually do very dirty things with unsafe 😈

let x : u32 = unsafe { std::mem::transmute::<[bool; 4], u32>([true, true, false, false]) };

On a more serious note, I agree. I propose to start with a --strict flag (the name is still to be bikeshed, but this doesn't block the implementation) which just starts the typechecker in static mode by default, but still disables it under contracts.

We can always revisit later and add the stricter level where everything has to be typed, even under contract annotations, if ever needed. Both shouldn't be hard to implement at all; the only question is if the second level would is usable and thus useful in practice.