Re-introduce let-declarations #42

New issue

Closed

opened 2023-06-02 20:01:51 +02:00 by samvv · 0 comments

samvv commented

2023-06-02 20:01:51 +02:00

(Migrated from github.com)

Problem

Currently, let-declarations have been split up into function declarations (using the keyword fn) and variable declarations (using the keyword let). This solves a few issues, but is far from ideal. Ideally, we'd like to keep the syntax as simple as possible and as close as possible to what Haskell does.

The original issue resulted from the fact that as a strict language, we would like to make the distinction between an ordinary variable declaration (such as let foo = 42) and functions with no argument (with type () -> Int for example). Imagine for a moment that foo did an expensive calculation and the user didn't want to run this calculation right away. Without the split, there was no way of saying that the computation should be delayed.

Solution

In this new proposal, we address some of the confusion regarding strict/lazy evaluation, typing, and the difference between function declarations and variable declarations.

A first observation is that the way the program is typed should have no effect on the way it is evaluated, be it with the exception of type classes. Therefore, whether foo is typed as () -> Int or Int should make no difference. As a consequence, the special parameterless TArrow type that came with the initial design has no real use.

A second insight is that users always can defer the computation of a variable, even in the context of strict evaluation and currying. They just have to declare a variable let foo = \() -> 42 and call it with the unit tuple. We can abstract away this solution to something like let foo = thunk 42 and force execution with e.g. foo!. Alternatively, we could introduce the lazy keyword and require the variable to be only computed if it has been referenced.

Implementation Strategy

Make declarations with a type assert and no body (such as let x : Foo) be a variable declaration. If there are any parameters such as let x a b : Foo, then that is an error that should be reported.
Make declarations with a body (such as let x = 1) be treated like a function, even if there are no parameters. In that case, it just so happens to not have a TArrow.
All patterns other than a simple bind pattern force the let-declaration to be a variable. Parameters are invalid.
mut makes the declaration automatically be a variable declaration. Parameters are invalid.
Deferred assignment works in theory on both variable declarations and function declarations. The only reason it does not work on function declarations with parameters is that the parameters cannot be referenced.

# Variable
let foo : Int
foo # invalid
if toss.
  foo = 1
else.
  foo = 2
foo # valid

# Variable
let mut foo = 42

foo := 3

# Function
let add x y = x + y

Remarks

If we ever need to introduce algebraic effects, we can still do so without running into issues involving parameterless functions not being able to hold an effect in their (missing) TArrow type. The solution using thunk as described in the previous section will always generate a TArrow, while variable declarations don't need to hold an effect and simply contribute to the effect of their parent declaration.

## Problem Currently, `let`-declarations have been split up into function declarations (using the keyword `fn`) and variable declarations (using the keyword `let`). This solves a few issues, but is far from ideal. Ideally, we'd like to keep the syntax as simple as possible and as close as possible to what Haskell does. The original issue resulted from the fact that as a strict language, we would like to make the distinction between an ordinary variable declaration (such as `let foo = 42`) and functions with no argument (with type `() -> Int` for example). Imagine for a moment that `foo` did an expensive calculation and the user didn't want to run this calculation right away. Without the split, there was no way of saying that the computation should be delayed. ## Solution In this new proposal, we address some of the confusion regarding strict/lazy evaluation, typing, and the difference between function declarations and variable declarations. A first observation is that the way the program is typed should have no effect on the way it is evaluated, be it with the exception of type classes. Therefore, whether `foo` is typed as `() -> Int` or `Int` should make no difference. As a consequence, the special parameterless `TArrow` type that came with the initial design has no real use. A second insight is that users always can defer the computation of a variable, even in the context of strict evaluation and currying. They just have to declare a variable `let foo = \() -> 42` and call it with the unit tuple. We can abstract away this solution to something like `let foo = thunk 42` and force execution with e.g. `foo!`. Alternatively, we could introduce the `lazy` keyword and require the variable to be only computed if it has been referenced. ## Implementation Strategy 1. Make declarations with a type assert and no body (such as `let x : Foo`) be a variable declaration. If there are any parameters such as `let x a b : Foo`, then that is an error that should be reported. 2. Make declarations with a body (such as `let x = 1`) be treated like a function, even if there are no parameters. In that case, it just so happens to not have a `TArrow`. 3. All patterns other than a simple bind pattern force the `let`-declaration to be a variable. Parameters are invalid. 4. `mut` makes the declaration automatically be a variable declaration. Parameters are invalid. 5. Deferred assignment works in theory on both variable declarations and function declarations. The only reason it does not work on function declarations with parameters is that the parameters cannot be referenced. ``` # Variable let foo : Int foo # invalid if toss. foo = 1 else. foo = 2 foo # valid ``` ``` # Variable let mut foo = 42 foo := 3 ``` ``` # Function let add x y = x + y ``` ## Remarks - If we ever need to introduce algebraic effects, we can still do so without running into issues involving parameterless functions not being able to hold an effect in their (missing) `TArrow` type. The solution using `thunk` as described in the previous section will always generate a `TArrow`, while variable declarations don't need to hold an effect and simply contribute to the effect of their parent declaration.

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: samvv/bolt#42

No description provided.