Add support for local variables

[eminence]

There are some "helper variables" in physics/temperature_conversion.nbt that currently leak through the prelude, like offset_celsius and scale_fahrenheit. These variables feel like "implementation details" that should be contained only to the nbt file they are defined in.

Perhaps there could be a concept of local variables?

[sharkdp]

Thank you for reporting this.

Yes, this is unfortunate. I see several ways to address this:

1. Add a way to have module-local constants/functions, like you proposed. We would probably need a new keyword like private for this (let private offset_celsius = …) or use a decorator like we have for unit declarations (@private)?
2. Do the opposite: have everything private by default and introduce a way to export entities from a module (pub/public/@public/export)
3. Add something similar to module scopes or namespaces, where we could have mod details { let offset_celsius = …; } and then use it internally with details::offset_celsius. That namespace would not be hidden, but it would not be imported by default when doing use physics::temperature_conversion. Only if someone would do use physics::temperature_conversion::details.
4. Add function-level local variables, maybe with a Haskell-style syntax:

   fn from_celsius(t_celsius: Scalar) -> Temperature =
     (t_celsius + offset_celsius) kelvin
     where offset_celsius = 273.15

   This would not really help in this case (as we want that constant to be present in multiple functions), but would certainly be helpful in a lot of scenarios

It's currently not clear to me yet which way we should take forward.

[eminence]

I think if I had a magic wand that would give me one of these solutions for free, I probably would choose option 1 or 3. I would probably not vote for option 2 because I think the majority of nbt code will want to export most everything (like how the current prelude is today).

(Another short-term option might be to hide all variables that start with an underscore _ from tab-completion and the output of "ls". I think this would be pretty cheap to implement, but not very satisfying and not my preferred approach)

[triallax]

(Another short-term option might be to hide all variables that start with an underscore _ from tab-completion and the output of "ls". I think this would be pretty cheap to implement, but not very satisfying and not my preferred approach)

I work a lot with Dart, and this is the approach it takes; I have to say that while it's pretty nice to be able to see whether an identifier is private at its use site, I agree that I wouldn't prefer it as opposed to more traditional "attributes", and I think it just doesn't fit with the overall feel of the Numbat language.

[yerke]

Can I cast a vote for adding support for local (function scope) variables first? It probably would be cleaner and easier to implement. As for the syntax, would you be open to have support for let a = 10 (or some other keyword potentially (var?), I think let is used for constants right now) as well? I know this opens a separate discussion on whether to allow to multi statement functions, which as far as I understand is not allowed.

[simmsb]

For those interested, I had a play around with implementing let <ident>[: <type>] = <expr> of <value> expressions here

[yerke]

@simmsb thanks for sharing your progress. I think the example you have in your branch

fn foo(x: Scalar) -> Scalar =
  let y = x * 2 of
  let z: Scalar = y + x of
  x * y * z

would be easier to read in this format:

fn foo(x: Scalar) -> Scalar =
  let y = x * 2;
  let z: Scalar = y + x;
  x * y * z

How hard is it to pretend that ; is the same as of? ;)

[sharkdp]

Concerning the syntax, I would personally favor the let … in … syntax for let-expressions that seems common in other programming languages (Haskell) and the literature.

But what I would like even more is the … where … syntax that is also used in functional programming languages, because it puts the important things first and reads a bit more naturally. It also extends more nicely to a multi-definition version:

fn foo(x: Scalar) -> Scalar = x * y * z
  where
    y = x * 2
    z: Scalar = y + x

And I also want to extend that to local functions. Since let is currently only used for constants, and fn for functions, it seems more "symmetrical" to just use where for local definitions, which would allow us to skip both let and fn, which are not needed for disambiguation in this context, since we know that we are parsing a definition, and not a function-call expression (that is the reason for having introducer-keywords like let and fn in the first place).

fn maximum<D: Dim>(xs: List<D>) -> D = foldl(max, -inf, xs)
  where
    max(x, y) = if x > y then x else y

For those interested, I had a play around with implementing let <ident>[: <type>] = <expr> of <value> expressions here

Cool! Function-level local bindings are my personal top-priority request. It's really inconvenient to write Numbat code without them and also leads to inefficiencies (dual evaluation due to duplication of subexpressions). I have a lot of TODOs in the Numbat standard library that we could resolve once we have local bindings.

@simmsb Did that experiment run into a dead end or is that something we could pick up for an implementation of local bindings?

The type checker / type inference changes for local bindings are probably not completely straightforward. One thing that I read about, and that we should probably follow, is the Let Should not be Generalised paper, which argues that not generalizing let expressions is (1) easier and (2) favorable for type systems that go beyond Hindley Milner. The explicitly include "units of measure (Kennedy 1996)" as one of such extensions. The Kennedy-extension is more or less exactly what we have implemented in Numbat.

What's also not straightforward is the implementation of closures (see also #347 — my personal number two request), which would naturally come with local functions. So maybe we should implement local constants/variables first, and do functions in a second step.

[simmsb]

Did that experiment run into a dead end or is that something we could pick up for an implementation of local bindings?

It's definitely something that could be picked up, the implementation is fully functional.

[sharkdp]

For everyone in this thread: there is significant progress on this topic in #519 by @irevoire.

Here's something that took me a bit too long to realize. let … in … and … where … are not interchangeable. They are not even the same kind of construct. let … in … is an expression. But … where … can not appear alone, it is tied to the function definition. And always introduces identifiers "globally", for the full function scope.

let … in … is strictly more powerful, especially without lazy evaluation. Consider

fn filter<A>(p: Fn[(A) -> Bool], xs: List<A>) -> List<A> =
  if is_empty(xs)
    then []
    else if p(head(xs))
      then cons(head(xs), filter(p, tail(xs)))
      else filter(p, tail(xs))

We can not simply move head(xs) to a local variable definition using where:

fn filter<A>(p: Fn[(A) -> Bool], xs: List<A>) -> List<A> =
  if is_empty(xs)
    then []
    else if p(x)
      then cons(x, filter(p, tail(xs)))
      else filter(p, tail(xs))
  where
    x = head(xs)

because x = head(xs) is evaluated (eagerly) and leads to a "empty list" error in the xs = [] case.

On the other hand, it is possible to write this using let … in …, if the scope is limited accordingly:

fn filter<A>(p: Fn[(A) -> Bool], xs: List<A>) -> List<A> =
  if is_empty(xs)
    then []
    else 
      let x = head(xs) in
        if p(x)
          then cons(x, filter(p, tail(xs)))
          else filter(p, tail(xs))

This does not mean that I'm against where suddenly. I still like it.

Maybe we'll implement both of them, after all.

See also: elm/compiler#621 for a long discussion about the topic

[sharkdp]

where clauses are now supported in function definitions, see #519. For example

fn f(x: Scalar) -> Scalar = β × sin(z) / z
  where z = x³ + x
    and β = 0.123

Try here

This does not solve all problems that were discussed here. In particular, the original problem with the variables in physics/temperature_conversion.nbt is still not solved, as those variables are needed in two functions. But I think this can be discussed in a new issue when it becomes a problem.