see syntax-playgroundf.df
What about casing on multiple arguments?
> fn | Cons(x,xs) => x > | Nil => 0
for (k:v in some-dict) blah for (some-dict[k] = v) blah
becomes
for (k in keys some-dict) let v = some-dict[k] in blah
The only problem is: a monotone or a discrete let?
NEED TO TRY MOAR EXAMPLES
- reachability / transitive closure
- shortest path
- parsing
- stratification
See also Dyna; See also chrisamaphone’s gist https://twitter.com/chrisamaphone/status/803309414916689920 https://gist.github.com/chrisamaphone/d399abf6d9ebb6c511d9cf414dd1b983
Some ideas:
> rel path(x,y) :- edge(x,y) > | path(x,z) :- path(x,y), path(y,z)
> rel (x,y) ∈ path <- (x,y) ∈ edge. > | (x,z) ∈ path <- (x,y) ∈ path, (y,z) ∈ path.
– TODO look at Dyna’s syntax > dist(x,y) is 1 <- edge(x,y). > dist(x,y) is d+1 <- edge(x,y), dist(y,z) is d.
Or, backwards:
> (x,y) in path <- (x,y) in edge. > (x,z) ∈ path <- (x,y) ∈ edge, (x,z) ∈ edge.
Or, more general but probably confusing to most:
> {(x,y)} <= path <- (x,y) ∈ path, (y,z) ∈ path.
DECL ::= ID(EXPR,*) :- ATOM,* . ID(EXPR,*) is EXPR :- ATOM,* .
– not sure about {not ID(PAT,*)} & co – maybe {not ID(EXPR,*)} instead? – Datalog can do it, I think! but what does it mean? ATOM ::= if EXPR ID(PAT,*) | ID(PAT,*) is PAT not ID(PAT,*) | not ID(PAT,*) is PAT
– PAT is just Datafun patterns. PAT ::= VAR | (PAT,*) | CTOR-ID(PAT,*) | [PAT,*] | LIT | !EXPR EXPR = datafun expressions
Not having to worry about where your variables are coming from! In functional syntax, it’s always unambiguous whether a variable is being bound or is an expression. In {Pro,Data}log, it isn’t; no (syntactic) distinction.[1] So, the syntax has to treat variables specially somehow.
[1]: In Prolog, there’s no semantic distinction either; but Datalog adds restrictions to make sure you can see every variable as coming from somewhere. (Every variable in the head must be mentioned in at least one positive position, i.e. “generated”, in the body.)
Suppose I want to define
fun dom s = {x | (x,_) in s} ∪ {x | (_,x) in s}
We have or-patterns, so why can’t I do:
fun dom s = {x | (x,_)|(_,x) in s}
The syntax is kind of awkward (the “|” character is overloaded), but the meaning is obvious. Problem is, it doesn’t work. Only the first pattern to match counts (in this case, (x,_), since it’s an irrefutable pattern). Possible solution: interpret patterns differently between “case” and looping constructs; “case” chooses the first pattern match (prioritized choice), while looping does all matches (parallel choice).
Alternatively, we could add a “parallel choice” construct over iteration loops, written “or”:
fun dom s = {x | (x,_) in s or (_,x) in s}
Again, there’d be funny syntax issues if you wanted to mix parallel (union) “or” loops and nested (cross product) “,” loops. But the idea is sound.
Maybe use semicolon “;” for disjunction-loop operator, a la Prolog?
What about casing on multiple arguments?
> fn | Cons(x,xs) => x > | Nil => 0
for (k:v in some-dict) blah for (some-dict[k] = v) blah
becomes
for (k in keys some-dict) let v = some-dict[k] in blah
The only problem is: a monotone or a discrete let?
NEED TO TRY MOAR EXAMPLES
- reachability / transitive closure
- shortest path
- parsing
- stratification
See also Dyna; See also chrisamaphone’s gist https://twitter.com/chrisamaphone/status/803309414916689920 https://gist.github.com/chrisamaphone/d399abf6d9ebb6c511d9cf414dd1b983
Some ideas:
> rel path(x,y) :- edge(x,y) > | path(x,z) :- path(x,y), path(y,z)
> rel (x,y) ∈ path <- (x,y) ∈ edge. > | (x,z) ∈ path <- (x,y) ∈ path, (y,z) ∈ path.
– TODO look at Dyna’s syntax > dist(x,y) is 1 <- edge(x,y). > dist(x,y) is d+1 <- edge(x,y), dist(y,z) is d.
Or, backwards:
> (x,y) in path <- (x,y) in edge. > (x,z) ∈ path <- (x,y) ∈ edge, (x,z) ∈ edge.
Or, more general but probably confusing to most:
> {(x,y)} <= path <- (x,y) ∈ path, (y,z) ∈ path.
DECL ::= ID(EXPR,*) :- ATOM,* . ID(EXPR,*) is EXPR :- ATOM,* .
– not sure about {not ID(PAT,*)} & co – maybe {not ID(EXPR,*)} instead? – Datalog can do it, I think! but what does it mean? ATOM ::= if EXPR ID(PAT,*) | ID(PAT,*) is PAT not ID(PAT,*) | not ID(PAT,*) is PAT
– PAT is just Datafun patterns. PAT ::= VAR | (PAT,*) | CTOR-ID(PAT,*) | [PAT,*] | LIT | !EXPR EXPR = datafun expressions
Not having to worry about where your variables are coming from! In functional syntax, it’s always unambiguous whether a variable is being bound or is an expression. In {Pro,Data}log, it isn’t; no (syntactic) distinction.[1] So, the syntax has to treat variables specially somehow.
[1]: In Prolog, there’s no semantic distinction either; but Datalog adds restrictions to make sure you can see every variable as coming from somewhere. (Every variable in the head must be mentioned in at least one positive position, i.e. “generated”, in the body.)
tagless-final style: http://okmij.org/ftp/meta-programming/#QUEL http://okmij.org/ftp/meta-programming/quel.pdf
quoted DSLs?
There is a natural interpretation of fixed point as creating a dataflow graph and then running it until quiescence (until fixed point is reached). This might also account for various forms of “chaotic iteration” optimization! And also for “iterative join” algorithms. (see also: “on-line monotone computation”, further down)
eg. (fix x is (e1, e2)) creates two dataflow nodes, one for e1, one for e2, which get to refer to one another!
Or, (fix x = tabulate keys func) creates one dataflow node per key in `keys’.
where tabulate : {K} -> (K -> V) -> {K: V}
many logical algorithms use deletion for efficiency. as long as a deleted fact can never get re-added, this is still monotone in a sense! and this sense of monotonicity is captured by added-removed sets!
currently the implementation has subtyping, but the only non-trivial subtypings are (a ~> b) <: (a -> b) and width subtyping of sum types.
however, we have two forms of type quantification:
- quantification over all types
- qunatification over lattice types
using Hindley-Milner unmodified probably won’t work, because how can we determine whether a function is intended to be ordinary or monotone?
also, have to incorporate typeclass-like constraint for quantification over lattice types.
counting things, for example, is naturally a commutative-monoid-style computation.
Matthew Maurer is working on a datalog-like logic language for binary analysis (https://github.com/maurer/holmes/blob/master/formal/holmes.tex) which has the property that external predicates (representing individual analyses) can have new facts added at any time! This requires monotonicity in aggregation operators.
We already have monotonicity! Can we efficiently implement on-line computation? That is to say, for a function (f : A ~> B) in our language, is there an efficient way to evaluate it over monotonically increasing inputs?
Could use SAC (self-adjusting computation), but that’s more general (works for arbitrarily-changing inputs). (A monotonic function can of course involve computing things in the non-monotonic fragment, but I think we’re guaranteed those won’t change when we change the monotone input?)