art-w

Two interesting projects in that space:

- https://arcan-fe.com/ which introduces a new protocol for TUI applications, which leads to better interactions across the different layers (hard to describe! but the website has nice videos and explanations of what is made possible)

- Shelter, a shell with reproducible operations and git-like branches of the filesystem https://patrick.sirref.org/shelter/index.xml

As much as I love APL for its notation, Erlang does provides equivalent highlevel operators for processing sequences of elements. It's not fair to compare your highlevel implementation in APL to your lowlevel optimized (and quite unreadable) solution in Erlang. Here's the equivalent algorithm:

    is_descendant(A, B) ->
        lists:all(fun ({Actor, Event}) ->
                        Event =< proplists:get_value(Actor, B, -1)
                  end, A).
    
    compare(A, B) ->
        A_in_B = is_descendant(A, B),
        B_in_A = is_descendant(B, A),
        {A_in_B,
         B_in_A,
         A_in_B and B_in_A,
         not (A_in_B or B_in_A}}.

APL-enthousiasts often forget that APL forces you to use its builtin operators, while modern languages provide means to implement them (and aren't restricted to arrays). lists:all isn't a builtin in Erlang, but does it really matters that you can write it as `^/` in APL?

Note for functional programmers: `^` is the boolean AND operator, `/` is `fold`, and somehow there's an APL builtin hack so that `fold` knows that 1 (true) is the monoid identity of `AND`... but really `^/` is a compact notation for `fold (&&) True`

For completness:

    all(_, []) -> true.
    all(Pred, [X | Xs]) -> Pred(X) andalso all(Pred, Xs).

    get_value(_, [], Default) -> Default;
    get_value(K, [{K, V} | _], _) -> V;
    get_value(K, [_ | Rest], Default) -> get_value(K, Rest, Default).

While I agree I was expecting a more visual story from the synopsis, I strongly recommend the movie "The Hunt" with Mads Mikkelsen to get a feeling of what he may have gone through. It's a really good movie.

Have you looked at the table of contents?

http://people.ucalgary.ca/~rzach/static/open-logic/open-logi...

Summary: They are going for the foundations of maths, computer science, and logic with completeness, decidability and computability on the menu. I don't know the authors, and I understand your reticence, but the contents looks really good. It's not the kind of logic a practitioner would care about, probably, but it is the big mathy results that logicians do need to learn: they actually mention that this isn't a new course for them, but rather a reference book for lessons that are already given to philosophers.

It's also clearly not written for people who are afraid of maths -- I'm more concerned about their targeted audience. Can you go through that text without an already solid interest in maths?

Ha, you got me for a second. The bits aren't "stored" inside the vertex, but in the segments: It would be like saying that the space between bits "{0,1} {0,1}" contains 2 bits of information, and that we could encode more compactly by disposing bits around a circle, hence maximizing the number of bits in the center space. So given a triangular/square grid, the number of traceable segments is what matters (and that's where the ink goes too.)

I agree that triangles look a lot better than squares (to the point that the "swastika effect" is indeed a problem, even though the drawings are generated by a human, and not randomly.) However, they are also very hard to draw properly.

To recover the QR code decentralization, have you tried to encode data inside your triangular grid? You would loose the "drawable" property (due to the size), but the result would still look more interesting than the pixel junk of QR codes (and you could enforce "connectivity" for aesthetic and error correction.)

I hope you are joking. This isn't a spreadsheet, it's a stupid bruteforce algorithm that misses the point of the dataflow paradigm:

- Everything gets recomputed on any minor change.

- If a cell is referenced by N other cells, it will be recomputed N+1 times on every update. Worse, this can be exponential for A2=A1+A1, A3=A2+A2, which leads to A1 being recomputed 5 times. There's no sharing or memoization.

- Circular references are detected because they trigger a "too much recursion" exception.

- An impure cell "=Math.random()" will be observed with different values by its dependencies.

Not exactly: you don't get the O(1) access to the two previous computations with loeb. It abstracts the collection used for memoization, but it doesn't provides "locality".

Here's a presentation that dives into loeb and expands it to a comonadic fixpoint that lets you do the fibs example correctly: https://www.youtube.com/watch?v=F7F-BzOB670

Even if you manage to remove the explicit "reads" field, the "code" thunk is still going to point to the parent cells, so that wouldn't help the GC much.

That's a bad example, since GHC will perform common expressions elimination, which effectively give the same name to the two `add 1 z` (unless you specifically ask it not to, with `-O0`.)

Furthermore, Incremental isn't memoizing every function calls. It just keeps the intermediate results of the latest computation in memory, so that when the inputs change, it can determine exactly which subresults need a recomputation, and which can be reused. It's like Excel, but with dynamic dependencies.

(But yes, Haskell definitively does not do this. You could say that Haskell is about doing the least amount of work to compute something fresh, while Incremental is about working the least to recompute something we (almost) already computed just before.)

I agree that some language features have a binary nature, like static/overridable or lazy/strict, but maybe we shouldn't classify all of them like that?

The "new" keyword in Java is very much like the proposed "return from": if you know that something is an object, and that object allocation is always done on the heap, then Foo() is as clear as new Foo(). The "new" keyword is a residual from C++, where you actually had a choice. Is it possible that people don't dismiss Python for Java because of the lack of "new", but because its GC isn't as good?

If we had an hypothetical IDE that used colors to transmit static analysis to the user, then we could categorise the keywords between "this is something the IDE can infer" and "this is something the user should specify". Object allocation falls into the inferable (so rather than writing "new", the IDE would highlight the expression in red); virtual is not inferable; delay is not inferable; tail calls are inferable, and can be shown in pink or whatever.

Anyway, TCE is an optimization: we can run more programs faster when we have it. When we don't use tailrec, we still benefit from it as our program consumes less memory overall. The cost of tailcall elimination is purely cognitive, for people who learned the old C-like stack behaviour (but even C compilers handle TCE now.) If TCE/no-TCE matched the static/virtual and lazy/strict binary choice, then there would be situations were TCE has a negative impact on the code runtime.

If your argument isn't "well, you don't need new syntax and help from the compiler if you just pay attention and remember not to use with/try if you ever need guaranteed tail calls", then please state it more clearly because I haven't understood it.

To clarify: Yes, I believe that whichever stack release semantic is chosen (tailcall optimization or the current behaviour) triggers an understanding of its limitation. Languages that support tailcalls natively yield programmers that "see" tailcalls (so they don't think about it more than necessary), and non-tailcall support yield programmers that "see" stack allocation on recursion (but they don't think about the stack more than tailcall programmers do.)

Now, we both like the "default" behaviour that we have practised the most, because we really understand its limitation. When confronted with the other semantic, we can make it work, but it's slower to trigger our reflexes, and causes frustration:

A tailcall programmer forced to use a non tail-call language will have to "compile" his tail recursion into a loop. A non-tailcall programmer forced to use a tailcall language will gain free stack, but won't have to rewrite his algorithm.

Sure, finally breaks the tailcall syntax, just like it breaks the syntax rule "the function ends on a return".

You are right that I haven't stated my motivation for arguing about tailcalls:

- I really believe that tailcalls should be supported by Python. Recursion is too useful, and it's hard enough to teach without suffering the second class behaviour that Python currently offers.

- A new syntax is harder to sell to programmers and the python team, because it says "tailcalls are not the norm". I claim that "return f()" is used way too much to justify the cost of writing explicitly "return from f()" for a free optimization.

- A beginner doesn't need to know about tailcall to benefit from it, just like we don't teach them about the stack until they hit a stackoverflow. If you have two semantics with respect to stack release, it becomes harder to teach than if you choose only one (it triggers the question "why would you ever NOT write "return from" when you can?")

You seem to disagree that tailcalls should be optimized everywhere possible, but I'm not sure if it's because you don't care about writing "return from" in general (and just want to enforce it when it's actually observable), or think that "return from" isn't always an optimization (but I'm really missing a counter-example?), or really believe that tailcalls makes the semantic of the stack harder because of things like "finally" (in which case I think we both suffer from a bias towards the stack-release semantic that we are used to.)

If Python had tailcalls by default, would we have an argument for a "return after" syntax?

I like static analysis. I just don't think tailcalls require a more explicit annotation than any other language feature: writing "return from collect()" in your example doesn't clarify your intent, it just triggers a warning when someone breaks the tailcall (but he can still break the stack complexity through other means.) You do have to state your global property somewhere: the local tailcall annotation allow you to prove it today, not guarantee its survival upon software evolution. And as a user of your library, my static analyser could benefit from a function annotation on your side, but it won't care about your usage of "return from".

What's so invisible about your examples? I agree that an optimizing interpreter makes the situation harder to analyse, because we can't remember every simplification it handles. Without it, the tailcalls are very explicit.

Previously, you argued that Python semantics makes it very clear that all costs are visible. This seems to be against any rewrite rule, as the visible cost ("or False", "+ 0", "finally: pass") suddenly disappear. You are using your own rebuttal as an argument to make tailcalls look harder to analyse! They are not.

And I definitely thing it is a property of the specific call site, NOT the entire function, whether it should be checked for tailness. Decorators are the wrong solution here.

As a caller of a function, the property you care about is "does it consumes a fixed amount of stack?". As the writer of this function, that's the thing that matters in the end: Sure, that means checking each tail calls, but you really want the global guarantee that you didn't forgot one. The local explicit annotation becomes redundant.

But tailcalls already have a syntax:

    return f(a, b, c) # tailcall on f
    return f(g(b)) # tailcall on f
    return f(a, b, c) + 0  # tail call on +

Now, regarding your concern for the static analysis of stack allocation: This is not a feature you have for any other aspect of the language... you have no way of specifying your expected memory consumption. But you do have your experience, you know the traps, you have learned the patterns to look for. Sure, the annotation could be used by a static linter, but builtin static analysis is not a feature in Python. Why should tailcalls be a syntaxic exception?

(Note: tail recursion is a special case of tail calls! The annotation you are thinking about would be more interesting as a function annotation, as you really don't want to track each of your recursive returns to state your global expectation.)

What you are asking for is common for new language features: You want a red flag, something that highlight the semantic prominently, so that you don't forget and are forced to think about something you aren't used to. Please have a look at your python code: how many returns end with a call to a function? Are you going to decorate each of them with "tailreturn"? It's really a free optimization, your program will run faster and consume less memory once it is there.

(Is Python even specifying that its implementation should use a stack?)

I disagree, HTML is a datastructure like any other, and it should be easy to build one without going through an untyped string or an auxiliary file. It's painful to make one html file per renderable item -- and debugging takes more time (once you've found who's responsible for rendering it, you need to check the corresponding template, so there's an additional step in your way.) There's no semantic in using the filesystem to organize your templates: it's the code that specify the meaning, and your programming language provides more organization units than your FS (or should we do "one function per file and one directory per class/module"?). (Also, the obvious filename typo vs static checking of function names; and the fact that your template is going to contain some rudimentary form of code or force you to obfuscate your intent even more.)

Which is why I don't like the proposal: it's not unifying HTML and Erlang, it's compiling string macros into Erlang. Is there any reasons not to embed the interpolation in Erlang directly?

    hello(N) ->
      Name = <em><? N ?></em>,
      <#>
        <p>Hello <? Name ?></p>
        <p>The <#></#> lets you group
           multiple elements, that don't
           have a parent, as a single value.</p>
      </#>.

You probably don't care what a "Tiger" search would return, but I find the DDG results vastly more informative:

https://duckduckgo.com/?q=tiger

Recommendations: animals, military, people, movies, bands, organizations, technology, ... with a pretty picture, a subtitle, and a short description.

Top results: Wikipedia, Tiger Direct (a shop), WWF, Defenders of Wildlife, Tiger Woods, Detroit Tigers (baseball), ... (infinite list.)

https://encrypted.google.com/search?hl=en&q=tiger

Single recommendation: Tiger (Animal), with a pretty picture, the life expectancy and the scientific name.

Top results: Tiger Airways, Wikipedia, Tiger Stores (a shop), WWF, Tiger Direct (another shop), Defender of Wildlife, ...

Special results "in the News": Tiger Airways, Tiger Woods.

I've been happily using DDG for almost a year now, but I still use `!g` regularly because it does get confused sometimes (point is: no search engine is perfect, but DDG makes it easy to redirect your search elsewhere.) I switched because google was pushing g+ too hard, experimenting with the presentation, customizing the result list based on my profile, and it was breaking my flow (like the popup "make google your default search engine", I get why they do it, but it required unwanted attention.) Somehow DDG convinced me that they would be less invasive.

I'm sorry, I don't think I understand your message and my answer might be off as a result. Could you link to the current research on more general solutions than Checker, so I can get a clearer picture?

a type system limitation that every type describing side effects [...] can only be used in the context of a compiler/interpreter.

A type system is just a logic description of a property that a program might have. It specifies how the language constructs interact with this property []. The fact that compilers use a type system is independent of your ability to write your custom type system, or to use it in a different context (IDE, toolchain, ..).

[] Are you saying that a type system shouldn't be concerned by the AST of the language?

An external type checker for Haskell: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... And the various type checkers for the not statically typed languages (python, ..)

Also, I don't understand why you distinguish "typing side effects" as something different from the rest?

you need to write a different type system for each property

But you do have to define your type system at some point? Are you thinking of something like Mezzo, where some userland properties can be defined without going down the type-system-definition road? https://protz.github.io/mezzo/

But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.

That's why type systems are defined with respect to the language construct, by rules on the AST (? I'm confused because of the earlier [*] here).

To go back to Agda significance for a custom type system, it's not enough to define a type system. You generally want to prove that your definition is valid: If your "checked exceptions" says that a program `P` can't fail due to an exception, you want to check that you didn't forget anything by verifying the type checker with respect to the actual semantic of the language.

You can also embed your custom property into Agda type system (isn't that what you want?).

People working on program synthesis consider the Occam razor "the shortest/simplest code" to be a good heuristic of the intended function (given a good test case.) Their main problem is the exponential space search.

This example is bizarre, because a fast implementation is probably going to rely on a SAT solver, at which point the "queens code" (in any language) becomes a declarative specification of the solution!

Also, I don't think that Haskell, OCaml, (or Prolog) are that much declarative: They have a very clear evaluation model, which you need to know in order to write any code. They also have debuggers as a result.

It's not reasonable to embed every possible language constructs, semantic and logic into a theorem prover. So the trick is to make the host generic enough to be able to embed your needs as a domain specific language: your critic becomes a library problem. Which implies that you only need to trust the host logic/implementation; and many people can work, collaborate and profit from the same core. Also, we kind of know how a generic logic can be done, but the domain specific logic are more controversial (because everyone needs are different.)

The fact that your DSL is represented as an immutable datastructure by the host is really not important. Any code you write is going to be turned into a datastructure at some point. The immutability should be read as "the context in which this result is valid has been made fully explicit", where "context" includes "things that mutate over time". You don't loose in expressivity, you just can't forget to handle special cases.