search

zydeco-lang / zydeco

a proof-of-concept programming language based on Call-by-push-value
Other
49 stars 3 forks source link

Virtualize & Remove Anns in Evaluator #25

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

(Implements #24)

This does two main things:

  1. Remove all of the completely unused Anns everywhere in the evaluator. I just found these completely pointless and difficult to keep track of.
  2. Virtualize the I/O operations in the evaluator. This is done by adding objects input: &mut dyn BufRead and output: &mut dyn Write to the runtime state and changing the evaluator to return Result<ZValue, Exit> where Exit is either an error or an early exit with an exit code. This also required minor changes to the implementations of the builtin functions.

I then also updated zydeco.rs to instantiate this abstract effect interface twice: once with the original OS primitives and once with basically empty input/output streams, and updated the builtin functions to use the new types. This also makes it possible to mock I/O and observe exit codes so we can implement #8 easily.

maxsnew commented 1 year ago

Oh I can only ask for one reviewer at a time. But I want to alert everyone who works close to this part to the change @LighghtEeloo @SchwarzXia @ricky136973

LighghtEeloo commented 1 year ago

Just checked, LGTM. Looking forward to completing #8 inside zydeco as much as possible.

Pre-considering more general use cases:

  1. Would it be convenient for the virtualized IO interface to support backends without IO accessibility? How would we express the fact that we don't support IO on some platforms? If we choose to panic! at runtime it is fine, but can we do better and lift this error to compile time?
  2. It might not be a bad idea to mark some PrimComps pure; actually, it's a problem of expressing effects and the ability and inability to use them on a specific instance of some platform, which is essentially the same problem as that in question 1. So should we classify the PrimComps by the effects they require? Algebraic effects should do the trick, but I'm not sure how hard it is to support (as a library or builtin) or how much we desire such feature.

On my side, if the questions above are responded, I think we are good to go. What do you guys think?

maxsnew commented 1 year ago

Let's take the discussion of "more general use cases" somewhere else (like slack).