Consistent elaboration for type attributes

[agle]

In general the policy of bincaml following Basil (and in contrast to ASLp) is to always operate on a fully typed AST with types always locally available. While Basil's type system was sufficiently simple to implement this naively (there are only primitive types and the IR is fully annotated from the start), we have attempted to add more features to our variables, namely

• Constness attributes
  • We use this to distinguish state from constant function declarations
  • I think we should maybe move this to the type system
• Sharedness attributes
  • local (to a function or procedure)
  • global (either readable (captured) or writable (modified) by any procedure
    • basically this is just implicit parameter passing
    • these are implicitly thread-local
  • global & observable
    • accesses to this variable are observable side-effects visible to all threads

We would sometimes like to operate on a lamdba-lifted form but still consider stores side-effecting; are these ideas contradictory? Do shared locals make any sense?

We have a problem in the frontend with these attributes; because we neither require explicit variable declaration, nor complete type annotation (as with function application types this becomes verbose) we there is a hacky attempt to lookup the right variable type, leading to two variables with the same name and different types.

• We can rule out complete type annotation of the IR as this is too verbose for my liking, especially for the function calls (like memory store/load following the transform, or just ADT constructors).
• We could require explicit declaration of everything and have the frontend propagate the declaration
  • This would require boogie-style variable declaration lists on procedures--- basil does not output this.
  • We currently softly require this (emit a warning on omission) on global variables
    • some tests currently ignore the warning
    • requires choice of a sensible fallback
  • Some mess in the frontend to deal with declaration lookup for each rvalue variable.
• We could load a sparesely-type annotated IR and elaborate the types fully using a type inference algorithm

The last option is my favoured, it requires more code but removes typing as a concern of the frontend, and still allows us to work on a fully typed ast at all times. Ideally make the IR independent in the type system it uses to allow experimentation with different algorithms. Procedures, blocks, and stmts, and expressions are already generic in the variable and expression type, and the expression type is generic in the type of its typ field, this is nearly there. The subtasks of this are

• Fix the type lattice so it can represent untypedness, or add some form of optional annotation expression.
• Type unification algorithm
• Type inference based on the AST
• Elaboration of types based on the AST - injecting back into the IR
• Typing repair when we construct new expressions to ensure the IR remains fully typed
• Transform passes to perform type inference and checking.