Types

[thevirtuoso1973]

Two main things to decide on: the types available in our language and our type checking approach.

For types, maybe:

• String
• VecString or just Vec if we do not anticipate Vec\<T> being needed. (I just realized that fixed size array types might not be not very useful.)

Possible dynamic type checking approach: during SLD resolution, whenever we resolve and see a type mismatch with the expected signature we throw a ResolutionError (I may rename this error type in this case) that's labelled as an exception. The caller(s) should be able to see it's an exception and just pass it up without further exploring the SLD tree. This assumes that we should never encounter type errors during SLD resolution. Specifically, given some selected goal goal_pred/n if we find a rule with a matching head goal_pred/n then it must match the associated types.

Type definitions could be something like:

goal_pred(X: String, Y: VecString) :- [body].

If the body contains variables not present in the head literal, their types would still be defined since there is some associated head literal (or builtin) that would define that variable type. (Notably DDlog uses some other way to define types that seems unnecessary for our purposes.)

---

Related literature:

• https://link.springer.com/chapter/10.1007/978-3-540-92995-6_12
• https://dl.acm.org/doi/abs/10.1145/1376916.1376957
• http://budiu.info/work/ddlog.pdf
• https://www.cis.upenn.edu/~bcpierce/tapl/

[mechtaev]

@thevirtuoso1973 , thanks for initiating discussion about data structures and types.

Perhaps, we can also add TAPL to related literature.

Apart from what you menioned, it would be nice to identify exact use cases that we would like data structures and types to cover. So far, we only have one concrete use case: passing arrays to several operators and builtin predicates: run, ::set_cmd and ::set_entrypoint. If this was the only use case, adding types and data structures would be an overkill: it is easier to just implement an ad hoc varargs for these predicates.

The second use case for data structures I can think of is parsing configuration files. Configuration files like JSON are recursive data structures, so it would require more complicated types.

The third use case is to parameterise images with e.g. list of packages that are installed on these images. This would be interesting, but this goes beyond the typical Docker usage scenarious.

---

goal_pred(X: String, Y: VecString) :- [body].

If there are multiple rules with goal_pred, I guess it means only the first one needs to be annotated?

Possible dynamic type checking approach

If I understand the approach correctly, it means that we have the disadvantage of static typing, that is the inconvenience of adding type annotation, while not having its advantage, design-time error detection.