Skip to content

Commit

Permalink
Merge pull request #189 from vekatze/explicit-non-affine-variables
Browse files Browse the repository at this point in the history
make copying operations explicit (`!foo`)
  • Loading branch information
vekatze authored Jun 15, 2024
2 parents 4beeb01 + ed8d7ef commit c9115c5
Show file tree
Hide file tree
Showing 85 changed files with 939 additions and 727 deletions.
4 changes: 2 additions & 2 deletions bench/action/bubble/module.ens
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
},
dependency {
core {
digest "Gqqa9FY2WS877MlG-wkGQvejwae4dipQ32MD6njVaIQ",
digest "9Rol5ZkFxSC_Rso9Sfh6zPW9yvxcg7_b_6dMCn9Dss4",
mirror [
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-1.tar.zst",
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-3.tar.zst",
],
enable-preset true,
},
Expand Down
4 changes: 2 additions & 2 deletions bench/action/dictionary/module.ens
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
},
dependency {
core {
digest "Gqqa9FY2WS877MlG-wkGQvejwae4dipQ32MD6njVaIQ",
digest "9Rol5ZkFxSC_Rso9Sfh6zPW9yvxcg7_b_6dMCn9Dss4",
mirror [
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-1.tar.zst",
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-3.tar.zst",
],
enable-preset true,
},
Expand Down
2 changes: 1 addition & 1 deletion bench/action/dictionary/source/dictionary-nt.nt
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ define make-big-dict(size: int): dictionary(int, int) {

define random-lookup-sum(count: int, d: &dictionary(int, int)): unit {
let rsum =
grow(count, 0, function (acc, _) {
grow(0, count, function (acc, _) {
let key = random(1000000) in
let val on key =
match intdict::lookup(key, d) {
Expand Down
4 changes: 2 additions & 2 deletions bench/action/intmap/module.ens
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
},
dependency {
core {
digest "Gqqa9FY2WS877MlG-wkGQvejwae4dipQ32MD6njVaIQ",
digest "9Rol5ZkFxSC_Rso9Sfh6zPW9yvxcg7_b_6dMCn9Dss4",
mirror [
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-1.tar.zst",
"https://github.com/vekatze/neut-core/raw/main/archive/0-50-3.tar.zst",
],
enable-preset true,
},
Expand Down
16 changes: 10 additions & 6 deletions book/src/basis.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,23 +54,27 @@ Note that the above example executes the type `list(int)` as a function.
Let's see how types are executed when copying values. For example, consider the following code:

```neut
define foo(xs: list(int)): unit {
some-func(xs, xs)
define foo(!xs: list(int)): unit {
some-func(!xs, !xs)
}
```

Note that the variable `xs` is used twice. Because of that, the compiler translates the above code into the below (pseudo-code; won't typecheck):
Note that the variable `!xs` is used twice. Because of that, the compiler translates the above code into the below (pseudo-code; won't typecheck):

```neut
define foo(xs: list(int)): unit {
define foo(!xs: list(int)): unit {
let f = list(int) in
let xs-clone = f(1, xs) in // passing `1` to copy `xs`
some-func(xs-clone, xs)
let xs-clone = f(1, !xs) in // passing `1` to copy `xs`
some-func(xs-clone, !xs)
}
```

Note that the above example executes the type `list(int)` as a function.

You must prefix a variable with `!` if the variable needs to be copied.

The prefix `!` is unnecessary if the variable can be copied for free.

### On Immediate Values

We don't have to discard immediates like integers or floats because their internal representations don't depend on memory-related operations like `malloc` or `free`. Because of that, "discarding" immediate values does nothing. Also, "copying" immediate values means reusing original values.
Expand Down
4 changes: 2 additions & 2 deletions book/src/manual-installation.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ Add the below to your `.bashrc`, `.zshrc`, etc.

```sh
# this sets the core module (or "prelude") that is used in `neut create`
export NEUT_CORE_MODULE_URL="https://github.com/vekatze/neut-core/raw/main/archive/0-50-1.tar.zst"
export NEUT_CORE_MODULE_DIGEST="Gqqa9FY2WS877MlG-wkGQvejwae4dipQ32MD6njVaIQ"
export NEUT_CORE_MODULE_URL="https://github.com/vekatze/neut-core/raw/main/archive/0-50-3.tar.zst"
export NEUT_CORE_MODULE_DIGEST="9Rol5ZkFxSC_Rso9Sfh6zPW9yvxcg7_b_6dMCn9Dss4"
```

Then, get the compiler:
Expand Down
6 changes: 6 additions & 0 deletions book/src/programming-in-neut.md
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,12 @@ define foo() {
}
```

<div class="info-block">

The compiler reports an error if you rewrite the example above so that it uses the variable `f` more than once. This behavior is to avoid unexpected copying of values. You can satisfy the compiler by renaming `f` into `!f`. The next section will cover this topic.

</div>

### Calling Functions

Functions `f` can be called against arguments `e1`, ..., `en` by writing `f(e1, ..., en)`:
Expand Down
58 changes: 47 additions & 11 deletions book/src/static-memory-management.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Here, we'll see how to write performant programs in Neut.
In Neut, the content of a variable is _copied_ according to its type _if the variable is used more than once_. Consider the following code:

```neut
// before compilation (pseudo code)
define foo(xs: list(int)): list(int) {
let ys = xs in // use `xs` (1)
let zs = xs in // use `xs` (2)
Expand All @@ -27,8 +28,8 @@ In the above code, the variable `xs` is used three times. Because of that, the c
```neut
// after compilation (pseudo-code)
define foo(xs: list(int)): list(int) {
let xs1 = copy-value-along-type(list(int), xs) in
let xs2 = copy-value-along-type(list(int), xs) in
let xs1 = COPY-VALUE(list(int), xs) in
let xs2 = COPY-VALUE(list(int), xs) in
let ys = xs1 in
let zs = xs2 in
some-func(ys);
Expand All @@ -40,6 +41,7 @@ define foo(xs: list(int)): list(int) {
Also, the content of a variable is _discarded_ _if the variable isn't used_. Consider the following code:

```neut
// before compilation
define bar(xs: list(int)): unit {
Unit
}
Expand All @@ -50,7 +52,7 @@ In the above code, since `xs` isn't used, the content of `xs` is discarded as fo
```neut
// after compilation (pseudo-code)
define bar(xs: list(int)): unit {
let _ = discard(list(int), xs) in
let _ = DISCARD-VALUE(list(int), xs) in
Unit
}
```
Expand All @@ -67,7 +69,7 @@ define buz(x: int): unit {
// pseudo-code
define bar(x: int): unit {
let _ = discard(int, x) in
let _ = DISCARD-VALUE(int, x) in
Unit
}
```
Expand All @@ -78,6 +80,40 @@ In the literature, a use of a variable is called _linear_ if the variable is use

If you're interested in how Neut achieves these discarding/copying operations, please see [How to Execute Types](./how-to-execute-types.md).

### To Be Conscious of Cloning Values

Suppose the content of a variable were to be copied simply by using it more than once. In that case, we might suffer from unintended cloning and encounter unexpected performance degradation.

The compiler thus requires us to prefix the name of a variable with `!` when the variable needs to be copied. Let's consider the following code:

```neut
define make-pair(xs: list(int)): pair(list(int), list(int)) {
Pair(xs, xs)
}
```

When checking this code, the compiler will report an error because the code uses the variable `xs` twice and the variable isn't prefixed with `!`.

You can satisfy the compiler by renaming `xs` into `!xs`:

```neut
define make-pair(!xs: list(int)): pair(list(int), list(int)) {
Pair(!xs, !xs)
}
```

### Cloning Values For Free

The prefix `!` is unnecessary if the variable can be copied for free. For example, the following code will typecheck:

```neut
define make-pair(x: int): pair(int, int) {
Pair(x, x)
}
```

because we can "copy" integers for free (by simply using the same `x` twice).

## The Problem: Excessive Copying

Now, suppose we defined a function `length` as follows:
Expand All @@ -93,16 +129,16 @@ define length(xs: list(int)): int {
}
```

Also, suppose that we used the function as follows:
Also, suppose that we used this `length` as follows:

```neut
define use-length(xs: list(int)): unit {
let len = length(xs) in // use `length` to calculate the length of `xs`
some-function(len, xs) // then use `len` and `xs`
define use-length(!xs: list(int)): unit {
let len = length(!xs) in // use `length` to calculate the length of `!xs`
some-function(len, !xs) // then use `len` and `!xs`
}
```

Note that the variable `xs` is used twice. Therefore, in this example, the content of `xs` is copied _just to calculate its length_. This is a disaster. The end of the world. Every wish is crushed into pieces.
Note that the variable `!xs` is used twice. Therefore, in this example, the content of `!xs` is copied _just to calculate its length_. This is a disaster. The end of the world. Every wish is crushed into pieces.

Luckily, there is a loophole for this situation.

Expand Down Expand Up @@ -186,8 +222,8 @@ The result of `let-on` (that is, `len` in this case) can't include any noetic te
Incidentally, you can also create a value of type `a` from a value of type `&a`, as follows:

```neut
define clone-value<a>(x: &a) -> a {
*x
define make-pair-from-noema<a>(x: &a): pair(a, a) {
Pair(*x, *x)
}
```

Expand Down
2 changes: 1 addition & 1 deletion book/theme/book.js
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ hljs.registerLanguage("neut", function (hljs) {
},
{
className: "builtin",
begin: "<=|->|=>|\\*|:|\\||this|,|;|\\b_\\b|&|\\b-(?=\\s)|=|magic|assert|new-channel|new-cell|static|include-text",
begin: "<=|->|=>|\\*|:|!|\\||this|,|;|\\b_\\b|&|\\b-(?=\\s)|=|magic|assert|new-channel|new-cell|static|include-text",
},
hljs.COMMENT(
"//", // begin
Expand Down
4 changes: 2 additions & 2 deletions install.sh
Original file line number Diff line number Diff line change
Expand Up @@ -142,8 +142,8 @@ printf $BLUE "note: "
echo "please restart your shell after adding the following environment variables to your shell config:"

echo ""
echo "export NEUT_CORE_MODULE_URL=\"https://github.com/vekatze/neut-core/raw/main/archive/0-50-1.tar.zst\""
echo "export NEUT_CORE_MODULE_DIGEST=\"Gqqa9FY2WS877MlG-wkGQvejwae4dipQ32MD6njVaIQ\""
echo "export NEUT_CORE_MODULE_URL=\"https://github.com/vekatze/neut-core/raw/main/archive/0-50-3.tar.zst\""
echo "export NEUT_CORE_MODULE_DIGEST=\"9Rol5ZkFxSC_Rso9Sfh6zPW9yvxcg7_b_6dMCn9Dss4\""

if command -v apt-get >/dev/null 2>&1; then
echo "export NEUT_CLANG=$CLANG"
Expand Down
5 changes: 5 additions & 0 deletions src/Context/Elaborate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module Context.Elaborate
initializeInferenceEnv,
insConstraintEnv,
insertActualityConstraint,
insertAffineConstraint,
setConstraintEnv,
getConstraintEnv,
setSuspendedEnv,
Expand Down Expand Up @@ -64,6 +65,10 @@ insertActualityConstraint :: WeakTerm -> App ()
insertActualityConstraint t = do
modifyRef' constraintEnv $ (:) (C.Actual t)

insertAffineConstraint :: WeakTerm -> App ()
insertAffineConstraint t = do
modifyRef' constraintEnv $ (:) (C.Affine t)

getConstraintEnv :: App [C.Constraint]
getConstraintEnv =
readRef' constraintEnv
Expand Down
4 changes: 4 additions & 0 deletions src/Entity/Const.hs
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,10 @@ holeVarPrefix :: T.Text
holeVarPrefix =
"{}"

expVarPrefix :: T.Text
expVarPrefix =
"!"

unsafeArgcName :: T.Text
unsafeArgcName =
"neut-unsafe-argc"
Expand Down
3 changes: 3 additions & 0 deletions src/Entity/Constraint.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import Entity.WeakTerm qualified as WT
data Constraint
= Eq WT.WeakTerm WT.WeakTerm -- (expected-type, actual-type)
| Actual WT.WeakTerm
| Affine WT.WeakTerm

type MetaVarSet =
S.Set HID.HoleID
Expand All @@ -23,3 +24,5 @@ getLoc c = do
m
Actual (m :< _) ->
m
Affine (m :< _) ->
m
4 changes: 4 additions & 0 deletions src/Entity/Ident.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,10 @@ isHole :: Ident -> Bool
isHole (I (varName, _)) =
holeVarPrefix `T.isPrefixOf` varName

isCartesian :: Ident -> Bool
isCartesian (I (varName, _)) =
expVarPrefix `T.isPrefixOf` varName

innerLength :: Ident -> Int
innerLength (I (varName, _)) =
T.length varName
5 changes: 4 additions & 1 deletion src/Scene/Elaborate/Debug.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@ printConstraints = do
cs <- getConstraintEnv
forM_ cs $ \c -> do
case c of
Actual {} -> return ()
Actual {} ->
return ()
Affine {} ->
return ()
Eq expected actual -> do
printNote' $ toText expected <> " == " <> toText actual
Loading

0 comments on commit c9115c5

Please sign in to comment.