Substitution notes

[tpetricek]

Let's say we define predicate to test (in the type system) if two data frames are joinable using some columns:

joinable(X, Y, C1, C2) := 
  is_data_frame(X), is_data_frame(Y),
  fresh t, has_col(X, C1, T), has_col(Y, C2, T).

joinable(p"d1", p"d2", "name", "jmeno")

Not evaluated

If we have not evaluated d1 and d2, we start with a

• substitution:

  { X -> p"d1"; Y -> p"d2"; C1 -> "name"; C2 -> "jmeno" }
  

• goals

  is_data_frame(p"d1"), is_data_frame(p"d2"),
  fresh t, has_col("d1", "name", T), has_col("d2", "jmeno", T).
  

• we cannot resolve is_data_frame(p"d1") so we bail

Evaluated

If both data frames are evaluated we start with a

• substitution:

  { X -> p"d1"; Y -> p"d2"; C1 -> "name"; C2 -> "jmeno" }
  

• goals:

  is_data_frame(p"d1"), is_data_frame(p"d2"),
  fresh t, has_col("d1", "name", T), has_col("d2", "jmeno", T).
  

• after a few more steps
• substitution:

  { X -> p"d1"; Y -> p"d2"; C1 -> "name"; C2 -> "jmeno"; T -> "string" }
  

• goals: []

What we get back

If it is not evaluated, joinable(p"d1", p"d2", "name", T) results in nil (no substitution)
If it is evaluated, joinable(p"d1", p"d2", "name", T) results in { T->"string" }

If one is evaluated

Assume d1 evaluated, d1["name"] : string, but d2 unevaluated
What we get from joinable(p"d1", p"d2", "name", "jmeno")? We get nil

This is unfortunate! We would want to know how far the solver got and what it figure out. Better would be:

• substitution:

  { X -> p"d1"; Y -> p"d2"; C1 -> "name"; C2 -> "jmeno" }
  

• goals (I switched order in the definition here, so we can solve the first few):

  is_data_frame(p"d1"), fresh t, has_col("d1", "name", T), 
  is_data_frame(p"d2"), has_col("d2", "jmeno", T).
  

• substitution:

  { X -> p"d1"; Y -> p"d2"; C1 -> "name"; C2 -> "jmeno"; T -> "string" }
  

• goals

  is_data_frame(p"d2"), has_col("d2", "jmeno", "string").
  

• Now we cannot solve the next goal, but we could return this as "unsolved goals" with a substitution { T -> string } and now we can report this as constraints on the data that the user needs to supply (i.e., we do not know what d2 is, but it will need to be a data frame with a string column jmeno)