Evaluation order and nontermination in query languages | Hacker News Reader

Evaluation order and nontermination in query languages

rntz.net

44 pointsluu6 comments

I expected to see mention of the Church-Rosser theorem, which may have just turned 90 years old. Pretty good vintage for a comp sci theorem.

Anyway the way I learned it is:

* for a given lambda expression, all evaluation orders which reduce to a normal form will reduce to the same normal form.

* if a lambda expression has a normal form, the 'lazy' way (normal order, leftmost-outermost-reduction, call-by-name, call-by-need) will find it.

Actually on re-reading, the article did mention confluence of the untyped lambda calculus, but only went as far as saying that the different evaluation order leads to different termination results, which is not quite as strong as saying the lazy way will find the terminating path if it exists.

https://codeberg.org/veqq/declarative-dsls is built around a query language working on tables/dataframes, hashmaps, arrays, strings etc. in the same way. I ended up allowing things like :where :group-by etc. in `select` go in any order and then allowing you to use ->> macros to micromanage the execution order.

    :set {:job "Engineer"}
    :where |(= ($ :job) "Developer")

What is going on there in that where syntax?

|(...) is the same as (fn ...) making an anonymous function. $ is an argument (in a 1 arity anonymous function.) $ is getting the whole row which is a hashmap and e.g. ({:key "value"} :key) is a way of retrieving from a hashmap. So it's "where value in column job is "Developer".

A quick skim of the article suggests it's a study of the implications of allowing query planning in programs which are notionally finite but may have unbounded computation. Interesting.