search

quangis / transforge

Describe processes as type transformations, with inference that supports subtypes and parametric polymorphism. Create and query corresponding transformation graphs.
GNU General Public License v3.0
2 stars 0 forks source link

Type inference between tools is overly general #72

Closed nsbgn closed 2 years ago

nsbgn commented 2 years ago

The NoisePortionAmsterdam and Deforestation scenarios from https://github.com/quangis/cct seem to have some operation nodes that have a type that is hard to explain.

NoisePortionAmsterdam: an instance of getamounts is R2(Reg, Ratio), but should be R2(Reg, Count). Why?

Deforestation: an instance of subset is R2(Loc, Nom), but should be R2(Loc, Bool). Why?

nsbgn commented 2 years ago

While type inference works inside tools, between tools, the types are fixed to their most general. This is because each tool expression is evaluated before being concatenated.

That is, say that we have a function f : x ** x | x << Ratio and a tool T that implements that function. We then write the algebra expression for T as f(~Ratio). But this means that T has a function signature of Ratio ** Ratio, NOT of x ** x | x << Ratio. This works perfectly fine when attaching the output of tools to input of other tools, because this is indeed the most general instance of T --- but we lose the specificity on the output end.

This can be considered a bug.

nsbgn commented 2 years ago

Labelled sources should not be represented as Python data structures. Instead, labels are directly substituted with expressions during the parsing stage. If it is desirable to have substitutable structures in an evaluated expression, then variables in abstractions are a better way to achieve that.

Labels that refer to source nodes would simply be replaced with the corresponding source expression (eg ~A).

nsbgn commented 2 years ago

We have been working with objects of type dict[Expr, list[Node | Expr]] to represent workflows. However, when issue #72 is resolved, we can no longer simply map Expr objects to their inputs, as Expr can only be parsed once the inputs are parsed. Therefore, we should make a dedicated Workflow data structure for use in TransformationGraph.add_workflow. This will require a lot of changes in the tests.

nsbgn commented 2 years ago

~If this is to work, sources should probably know their most specific type. Otherwise, an expression like f (1: A) would need the actual type of 1 to remain variable, since it might also be 1.~ Actually, we can just keep it variable, and at the point that we are generating a graph, assume that type inference has run its course and set the type to be the most general possible (i.e. A).