Delay type #223

byorgey · 2021-10-12T20:58:07Z

Make explicit in the type system when evaluation of a computation should be delayed. This gives the user fine-grained control over selective laziness (for example, once we have sum types and recursive types, one could use this to define lazy infinite data structures). It also allows us to guarantee that certain commands such as build and reprogram delay evaluation of their arguments, and lets the user e.g. define their own modified versions of build without compromising those guarantees.

Delay is indicated by curly braces both at the value and type levels, that is, if t : ty then {t} : {ty}.
force : {ty} -> ty is now exposed in the surface language.
Change from a CEK machine to a CESK machine. Recursive let and def delay via allocating a cell in the store. For now, there is no other way to allocate anything in the store, but see discussion at Error when wrapping build #150 for some possible future directions.
change the types of build and reprogram to require a delayed program, e.g. build : string -> {cmd a} -> cmd string
if and try also require delayed arguments.
don't elaborate Build and Reprogram with extra Delay wrappers since one is now required by the type
Division by zero, negative exponents, and bad comparisons now throw exceptions.

Closes #150. Closes #226.

- Add a new type constructor `delay` - `TDelay` is now written with special double brackets `{{...}}`; `{{t}} : delay ty` whenever `t : ty` - Add a special case to the parser: `{{}}` parses as `delay noop` - `force : delay ty -> ty` is now written as a prefix `!` e.g. `{{5}} : delay int` and `!{{5}} : int` - Change the types of `build` and `reprogram` to require a delayed program, e.g. `build : string -> delay (cmd a) -> cmd string` - Don't elaborate `Build` and `Reprogram` with extra `Delay` wrappers since one is now required by the type

byorgey · 2021-10-13T03:50:23Z

Once we're all on the same page re syntax etc, I will update the tutorial and example programs.

polux · 2021-10-13T06:55:27Z

This made me realize a few things and I'm wondering if we should do this at all. Adding my thoughts/questions to #150 so the conversation doesn't get fragmented.

Now that the arguments to `if` must be delayed: - Remove the elaboration for applications of `if` - Assume the arguments will be VDelay at runtime

It is now a CESK machine, though we don't yet use the store for anything.

polux

Nice! I only have a few nits.

I reviewed the PR because if I understand the github UI correctly you did request a review. But the step function is not modified yet. Is it because you'd like to stage the review? (Which is very much welcome if that is the case: it's always easier to review small chunks.) Or is it because you're planning on modifying the step function in a different PR?

src/Swarm/Language/Syntax.hs

src/Swarm/Language/Typecheck.hs

src/Swarm/Game/CESK.hs

byorgey · 2021-10-15T11:04:24Z

@polux I think I requested a review when I initially opened the PR. I didn't specifically request one just now, but I appreciate the feedback, and you're right, reviewing in small chunks is helpful! I do plan to update the step function in this PR. Right now a store exists but is never used for anything.

Some bugs to fix noted by comments, and we still don't yet use memoized delay for recursion.

Note, `Build` and `Reprogram` still need to be updated.

byorgey · 2021-10-23T02:50:36Z

I think this is ready for another round of review. Note that at the moment, all delays are non-memoizing except for recursive let bindings and all def bindings; there is no way for users to explicitly get memoization. Of course this is probably something we want to explore further, but based on the conversation in #150 it seems like there is a large design space to explore, so I just wanted to get something simple working here first.

xsebek · 2021-10-23T12:29:19Z

Great work @byorgey! 👍

I will play with this some more, but the first thing I thought about was that it would be helpful to add the braces to F1 help:

┌─────────────────────────┬──────────────
│build <name> {<commands>}│Create a robot

Could you please add a table of types, now that we have {a} and a+b?

byorgey · 2021-10-23T12:32:27Z

Good ideas @xsebek , will do!

byorgey · 2021-10-23T20:49:34Z

How do you think the table of types should fit with the rest of the help? If I just add another table horizontally they all get too narrow in a reasonably-sized terminal window.

xsebek · 2021-10-24T10:35:39Z

Also it seems this fixes the wait cancellation 🥳 #194

xsebek · 2021-10-24T11:07:44Z

I updated my list.sw and measured this with delay-type and on main:

branch	`testLIST` with `8ticks/s`	`testLIST` with `1024ticks/s`	`testLIST_BIG` with `8ticks/s`	`testLIST_BIG` with `1024ticks/s`
delay-type	58s	>1s	<1h	47s
main	1min 7s	>1s	<1h	49s

The improvement is small*, but it is there and all that matters is that it is not slower. 👍
_{*) Likely because I used the lazy values for more efficient headTail from which head is forced without computing tail.}

There is a small bug with cancelling and then repeating a long computation, for example:

> let lbiggest = cons (2^2^21) $ cons (2^2^7) nil in len lbiggest // Ctrl-C
> let lbiggest = cons (2^2^21) $ cons (2^2^7) nil in len lbiggest
fatal error: Reference to unknown memory
  cell 16

~~But I don't think it is important enough to block this~~ There is a more common but just as fatal example below. 🙁

xsebek · 2021-10-24T11:21:21Z

@byorgey ad F1 help - I was thinking the table would be above commands, but it may need scrolling to fit in smaller terminals. Which is probably OK as it is focused and can use ⬇️ and ⬆️ .

We can leave that for another PR - with scrolling we could even list all available commands.

xsebek

Incredible work @byorgey! I think this is good to merge except for the problem with cancelling computation, which is unchecked and hopefully easy to fix. 🙂

src/Swarm/Game/Step.hs

test/Unit.hs

src/Swarm/Game/Step.hs

byorgey · 2021-10-24T19:42:38Z

You're right, it does fix #194, though I didn't realize I was fixing it. =) The bug previously was that we did Ctrl+C just by setting the robot's machine to idleMachine, but we did not actually put it back into the activeRobot set. Previously, the idleMachine actually had to execute a no-op instruction, but since it was not in the activeRobot set it never made progress executing this no-op instruction, and the REPL still thought it was doing something. But having idleMachine execute a no-op is silly; I changed it to be simply a CEK machine in a done state. Now it is correct to not add the robot to the activeRobot set, and the REPL immediately recognizes that the base is no longer doing anything.

byorgey · 2021-10-24T20:23:16Z

Hmm, good catch re: Ctrl+C causing problems with memory cells. This is a bit tricky. When we hit Ctrl+C we set the base's machine to idleMachine, which is definitely no longer correct, because idleMachine has an empty store, so this just throws away any memory cells that were allocated. However, it would also not be correct to just leave the store the same and reset the other machine components, because we might be in the middle of evaluating a cell, which would therefore be set to a Blackhole. If we ever try to use it, the system will encounter the Blackhole and incorrectly complain about an infinite loop.

Perhaps the solution is that a Blackhole should save the original expression which is being evaluated; when we Ctrl+C, any Blackholes in the store should be reset.

Hmm, I discovered by accident that we can end up with stray Blackholes if an exception is thrown as well. So we'll need some more general mechanism for resetting them...

- Add functions `cancel` and `resetBlackholes` to reset the store properly - Use those functions (1) when cancelling the base computation via Ctrl+C, or (2) when there is an uncaught exception

byorgey · 2021-10-24T21:25:58Z

This ought to fix the issues with Ctrl+C and the store.

Based on suggestion in #223 (comment) . Not quite sure how to effectively use it yet.

polux

Nice! I gave it a good look but couldn't find anything really meaningful to say.

src/Swarm/Game/CESK.hs

polux · 2021-10-25T07:13:02Z

src/Swarm/Game/Step.hs

+    -- body, binding the variable to a reference to the memory cell we
+    -- just allocated for the body expression itself.  As a fun aside,
+    -- notice how Haskell's recursion and laziness play a starring
+    -- role: @loc@ is both an output from @allocate@ and used as part


Reminds me of "Assembly: Circular Programming with Recursive do" in https://wiki.haskell.org/wikiupload/1/14/TMR-Issue6.pdf :)

xsebek

This ought to fix the issues with Ctrl+C and the store.

I checked it out and it works perfectly! 🥳

byorgey added 3 commits October 12, 2021 12:59

basic syntax highlighting for emacs mode

86ae889

Merge branch 'main' into delay-type

c94f5cc

byorgey requested a review from polux October 12, 2021 21:02

polux mentioned this pull request Oct 13, 2021

Error when wrapping build #150

Closed

xsebek mentioned this pull request Oct 13, 2021

Logical operators #189

Closed

byorgey mentioned this pull request Oct 13, 2021

Allow exceptions in pure code #226

Closed

byorgey added 13 commits October 14, 2021 14:57

switch back to function name syntax for force

6a99255

switch to {ty} syntax for delay type

0fa0099

use single braces for delayed terms

7364f35

Merge branch 'main' into delay-type

3d8a266

delay if and try arguments

9ed1673

fix runtime behavior of if

f4babe4

Now that the arguments to `if` must be delayed: - Remove the elaboration for applications of `if` - Assume the arguments will be VDelay at runtime

fix runtime behavior of try

d7522cf

division by zero and negative exponent now raise an exception

55885bf

fix syntax of benchmark programs

c4e259e

comparison now raises an exception on bad values

199fb25

add a store to the CEK machine

e81abef

It is now a CESK machine, though we don't yet use the store for anything.

rename Swarm.Game.CEK -> Swarm.Game.CESK

45b37bc

fix benchmark import

c154072

polux requested changes Oct 15, 2021

View reviewed changes

src/Swarm/Language/Syntax.hs Outdated Show resolved Hide resolved

src/Swarm/Language/Typecheck.hs Outdated Show resolved Hide resolved

src/Swarm/Game/CESK.hs Outdated Show resolved Hide resolved

src/Swarm/Game/CESK.hs Show resolved Hide resolved

byorgey added 6 commits October 15, 2021 06:12

update some comments

4dacbc5

memoized vs non-memoized delay. Add VRef and related CESK rules.

5584c19

Some bugs to fix noted by comments, and we still don't yet use memoized delay for recursion.

annotate Let and Def at parse time with whether they are recursive

6b43820

Interpret recursive let expressions via memoized delay

e993955

Put definitions in the store as well

d4b8533

fix If and Try to work with any kind of delayed value

9a6a3f1

Note, `Build` and `Reprogram` still need to be updated.

byorgey added 2 commits October 22, 2021 21:23

add more tests related to delay type

f680055

update tutorial to reflect changes re: { ... } syntax and delay

8b996cd

byorgey marked this pull request as ready for review October 23, 2021 02:45

byorgey requested a review from polux October 23, 2021 02:50

add curly braces to build help

f9cf73e

xsebek requested changes Oct 24, 2021

View reviewed changes

src/Swarm/Game/Step.hs Show resolved Hide resolved

test/Unit.hs Outdated Show resolved Hide resolved

src/Swarm/Game/Step.hs Show resolved Hide resolved

xsebek mentioned this pull request Oct 24, 2021

Add list example #261

Merged

byorgey linked an issue Oct 24, 2021 that may be closed by this pull request

Ctrl+C does not work in the middle of a wait command #194

Closed

fix problems with store + Ctrl+C/exceptions

1522514

- Add functions `cancel` and `resetBlackholes` to reset the store properly - Use those functions (1) when cancelling the base computation via Ctrl+C, or (2) when there is an uncaught exception

byorgey added 2 commits October 24, 2021 16:36

tests: add evalutesToInAtMost to count evaluation steps

2d3451f

Based on suggestion in #223 (comment) . Not quite sure how to effectively use it yet.

add a test showing that a definition is evaluated at most once

b6bd65c

byorgey requested a review from xsebek October 25, 2021 03:37

polux approved these changes Oct 25, 2021

View reviewed changes

xsebek approved these changes Oct 25, 2021

View reviewed changes

byorgey added the merge me Trigger the merge process of the Pull request. label Oct 25, 2021

mergify bot merged commit c982e81 into main Oct 25, 2021

mergify bot deleted the delay-type branch October 25, 2021 13:28

byorgey mentioned this pull request Oct 28, 2021

Seed robots are broken? #264

Closed

xsebek mentioned this pull request Jan 30, 2022

fatal error: Reference to unknown memory cell #299

Closed

byorgey mentioned this pull request Jun 20, 2022

Retire raise command #407

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Delay type #223

Delay type #223

byorgey commented Oct 12, 2021 •

edited

Loading

byorgey commented Oct 13, 2021

polux commented Oct 13, 2021

polux left a comment

byorgey commented Oct 15, 2021

byorgey commented Oct 23, 2021

xsebek commented Oct 23, 2021

byorgey commented Oct 23, 2021

byorgey commented Oct 23, 2021

xsebek commented Oct 24, 2021 •

edited

Loading

xsebek commented Oct 24, 2021 •

edited

Loading

xsebek commented Oct 24, 2021

xsebek left a comment •

edited

Loading

byorgey commented Oct 24, 2021 •

edited

Loading

byorgey commented Oct 24, 2021 •

edited

Loading

byorgey commented Oct 24, 2021

polux left a comment

polux Oct 25, 2021

xsebek left a comment •

edited

Loading

Delay type #223

Delay type #223

Conversation

byorgey commented Oct 12, 2021 • edited Loading

byorgey commented Oct 13, 2021

polux commented Oct 13, 2021

polux left a comment

Choose a reason for hiding this comment

byorgey commented Oct 15, 2021

byorgey commented Oct 23, 2021

xsebek commented Oct 23, 2021

byorgey commented Oct 23, 2021

byorgey commented Oct 23, 2021

xsebek commented Oct 24, 2021 • edited Loading

xsebek commented Oct 24, 2021 • edited Loading

xsebek commented Oct 24, 2021

xsebek left a comment • edited Loading

Choose a reason for hiding this comment

byorgey commented Oct 24, 2021 • edited Loading

byorgey commented Oct 24, 2021 • edited Loading

byorgey commented Oct 24, 2021

polux left a comment

Choose a reason for hiding this comment

polux Oct 25, 2021

Choose a reason for hiding this comment

xsebek left a comment • edited Loading

Choose a reason for hiding this comment

byorgey commented Oct 12, 2021 •

edited

Loading

xsebek commented Oct 24, 2021 •

edited

Loading

xsebek commented Oct 24, 2021 •

edited

Loading

xsebek left a comment •

edited

Loading

byorgey commented Oct 24, 2021 •

edited

Loading

byorgey commented Oct 24, 2021 •

edited

Loading

xsebek left a comment •

edited

Loading