Effekt by example #536
Effekt by example #536
Conversation
dvdvgt
added
documentation
| // Fold a list using `f`, starting from the left given a starting value. | ||
| // | ||
| // O(N) | ||
| def foldLeft[A, B](l: List[A], init: B) { f: (B, A) => B }: B = { | ||
| var acc = init; | ||
| l.foreach { x => acc = f(acc, x) }; | ||
| acc | ||
| } |
There was a problem hiding this comment.
Does this work on the MLton backend (mutable variable used in a foreach)?
Anyways — it would be nice to put a few tests for these new functions into the stdlib tests :)
There was a problem hiding this comment.
This how other functions like sum are also defined, so I just assumed this works
| val packet = do receive[Job]() | ||
| packet match { | ||
| case Some(p) => println("processing request") | ||
| case None => do break() |
There was a problem hiding this comment.
Note that from #528 onward, you'll need to bind the label:
each(0, 100) { (i) {label} =>
total = total + i;
if (total > 15) label.break()
println(i)
}|
|
||
| ```effekt:repl | ||
| var x: Int | ||
| ``` |
There was a problem hiding this comment.
In the future, it might be nice to have a forward reference to regions right here.
|
I just noticed that all tests in |
|
|
||
| ``` | ||
| interface Exception { | ||
| def throw(msg: String): Nothing |
There was a problem hiding this comment.
We have a very flat subtyping lattice in Effekt. Nothing is bottom in this lattice and thus is a subtype of everything. However, there is no inhabitant of this type. Yet, it is still useful. It is commonly used as the return type for functions that do not return. This is exactly what happens in other languages with exceptions. throw will never return anything.
There was a problem hiding this comment.
Thanks for the question! We could also explain that somewhere ("it's the type for unreachable things") -- it might even be worthy to say that it's Rust's & TypeScript's never, C++'s noreturn.
| def containsFile(fs: FileSystem, name: String): Bool = | ||
| fs match { | ||
| case File(name1, _) and name1 == name => true | ||
| case Directory(_, children) => |
There was a problem hiding this comment.
It would be helpful to note that brackets {} do not currently work in case expressions, unless that is going to change soon...
There was a problem hiding this comment.
I am not exactly sure what you mean. The body of each arm may be a single expression or a statement delimited by curly braces. So what you are describing should work unless I misunderstood your remark. Feel free to elaborate in this case
There was a problem hiding this comment.
That is, you also could have written { true } as the first match arm's body.
There was a problem hiding this comment.
see #422, I don't think the new parser resolved this
There was a problem hiding this comment.
Ha, thanks. I would have expected this to work. This should be easy to support if we want to.
| try { | ||
| div(a, b) | ||
| } with Exception { | ||
| def throw(msg) = { |
There was a problem hiding this comment.
Question: there is a fair amount of code out there with handlers as anonymous functions, i.e.
try div(a, b)
with Exception {
(msg) => panic(msg)
}Is this deprecated, or is it limited syntax sugar? It is decently widespread enough in other documentation that it may be nice to mention.
There was a problem hiding this comment.
Good question!
If we had defined the Exception effect as follows
effect Exception(msg: String): Nothing
we could have used the syntax you described. However, this is IMO in a bit of a weird place right now because of the different keyword (effect vs interface). I am therefore reluctant to mention it. I'll give it some thought.
There was a problem hiding this comment.
Oh interesting, okay! That clears up a lot of confusion I had. I thought effect Exception(msg: String): Nothing was a direct alias to interface Exception { def Exception(msg: String): Nothing } and couldn't figure out why it wasn't working...
| } | ||
| ``` | ||
|
|
||
| The operations `break` and `continue` have their usual semantics, except that they are handled by `loop` as operations of the algebraic effect `Control`. |
There was a problem hiding this comment.
As a newcomer to effects, the semantics of break/continue don't actually line up very well with my mental model of how effects systems work...
- Do
whileandloopboth use the sameControleffect, or dobreakandcontinueonly function withinloop? - Does the
whileconstruct desugar into some sort of handler, and if so, is it installed at the top level or wrapped around thewhilecomputation? - Can you call
continuewithin a function called within a loop and have it continue the external loop?
There was a problem hiding this comment.
Thanks for taking your time to ask these insightful questions! It is very valuable for us to get feedback for newcomers to algebraic effects.
whileis a natively built-in constructor and does not use theControleffect by default. However, no one is stopping you from wrapping a while loop using this effect in a handler and defining your own behaviour :)- See previous answer. Interestingly,
loopis a handler. I invite you to look at the (relatively concise) implementation to perhaps reconcile it with your mental model:
https://github.com/effekt-lang/effekt/blob/master/libraries%2Fcommon%2Feffekt.effekt#L651-L677 - Yes, indeed. You can do that. Note that the semantics of
Controldepend on the lexically nearest handler. If there is one "deeper nested" than loop, that one will handleControlinstead. This is true for all effects, of course.
Feel free to ask further questions, should anything be unclear to you.
There was a problem hiding this comment.
Cool! Is there any reason you all decided to separate out while into a built-in primitive in the first place?
There was a problem hiding this comment.
I am not aware of any particular reason. I would guess that while loops map nicely to some of the backends and can leverage the respective backend's optimisations.
| Perhaps unusual, you can also call `fib` using Effekt's implementation of [Uniform Function Call Syntax | ||
| ](https://en.wikipedia.org/wiki/Uniform_Function_Call_Syntax#cite_note-4): | ||
|
|
||
| ```effekt:repl | ||
| 5.fib | ||
| ``` |
There was a problem hiding this comment.
I feel like this is subtly combining two different things:
- UFCS
- the ability to omit parens for functions without parameters
Could we split it into two? Show 5.fib() first and then show the parenthesis-omitting part some time later?
examples/features/blocks.effekt.md
Outdated
| } | ||
| ``` | ||
|
|
||
| As we have established in a previous section, functions in Effekt are second-class. While you cannot pass them as first-class values to other functions as argument, you can pass them as second-class blocks. |
There was a problem hiding this comment.
I might suggest moving this whole section into the functions.effekt.md section... it's not entirely clear at the moment how UFCS and blocks interact (i.e. I was surprised that you can't do { 5.div(0) }.default(0))
There was a problem hiding this comment.
Good point, I will add some explanation for blocks and UFCS
|
Thanks to @jiribenes for workshopping the captures and regions sections with me! |
| @@ -0,0 +1,119 @@ | |||
| # FFI | |||
There was a problem hiding this comment.
| # FFI | |
| # FFI (Foreign Function Interface) |
| Effekt allows defining extern functions via FFI. | ||
| Let's start with the JavaScript backend by defining a function that adds two numbers: |
There was a problem hiding this comment.
| Effekt allows defining extern functions via FFI. | |
| Let's start with the JavaScript backend by defining a function that adds two numbers: | |
| Effekt allows communicating with the host platform (for instance JavaScript) by defining extern functions via FFI. | |
| Let's start with the JavaScript backend by defining a function that adds two numbers: |
|
|
||
| ## `extern include` | ||
|
|
||
| Sometimes, you want to include a whole JavaScript files containing your favourite JavaScript library |
There was a problem hiding this comment.
| Sometimes, you want to include a whole JavaScript files containing your favourite JavaScript library | |
| Sometimes, you want to include a whole JavaScript file containing your favourite JavaScript library |
| extern include js "./mycoollibrary.js" | ||
| ``` | ||
|
|
||
| > NOTE: Do not run this code on the website ^ |
There was a problem hiding this comment.
Can you explain why? Something like: "since these paths are relative, includes can only be used in local projects, but not on the Effekt website."
| extern js """ | ||
| function set$impl(ref, value) { | ||
| ref.value = value; | ||
| return $effekt.unit; | ||
| } |
There was a problem hiding this comment.
| extern js """ | |
| function set$impl(ref, value) { | |
| ref.value = value; | |
| return $effekt.unit; | |
| } | |
| extern js """ | |
| function set$impl(ref, value) { | |
| ref.value = value; | |
| return $effekt.unit; | |
| } |
Please do not use tabs.
| You can and should annotate the capture of your extern function as `extern <capture> def ...` | ||
|
|
||
| - no capture, usually denoted as `pure`, also writable as `{}` | ||
| - if you want to allocate into a global scope, use `global` |
There was a problem hiding this comment.
| - if you want to allocate into a global scope, use `global` | |
| - if you want to allocate into a global scope (e.g. the JavaScript heap), use `global` |
| - if your operation does I/O (like for example `println`), use `io` (this is the default capture) | ||
| - if your operation does other control effects, use `control` |
There was a problem hiding this comment.
| - if your operation does I/O (like for example `println`), use `io` (this is the default capture) | |
| - if your operation does other control effects, use `control` | |
| - if your operation performs I/O (like for example `println`), use `io` (this is the default capture) | |
| - if your operation captures the continuation use `control` (in the JS backend, control definitions should return a monadic value of type `Control`) |
This PR aims to add literate Effekt files showcasing the various interesting aspects of Effekt. The main target audience are researchers (including, most notably, compiler engineers). I mostly tried to limit explanations to purely syntactical aspects. Considering our target audience, the semantics should mostly be straightforward to understand.
Table of contents
Here are the planned and partially already drafted topics:
Topics marked with a
*are considered difficult and yet the most crucial topics of this collection.TODO
Changelog
foldLeftandfoldRightfunction in the standard library for listsRequest for feedback
Please do leave feedback. It is surprisingly difficult to gauge what to explain and mention and what to leave out.
While writing these examples, I may extend the standard library with new functions. It would be nice to keep an eye on those and discuss their inclusion.
Disclaimer: I am aware that there may be grammatically errors and typos. The formatting (e.g. limiting line width to ~120 characters) partly is subpar as well. Since much is still in flux, I have not bothered yet to go through the prose in more detail. When the rest is finalised, I will take care of these issues.
Future Work
Upon closer inspection, you may notice that the fenced code blocks not only have the types like
effekt:replbut alsoeffekt:hide: This content is not visible on the websiteeffekt:clear: The following content is not compiled together with previous.effekt:def: This is the default when there is no type after three ``` and contains definitions.These are preprocessing directives mainly targeting the website and still need to be implemented.