The Azimuth Project
Personal- David Tweed- Type systems for scientific computation (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Personal incomprehensible notes about type inference.

Basic types

  • u b,cu_{b,c} word with cc copies of bb-bit unsigned quantities. Often the actually implemented values are restricted to b=8,16,32,64b=8,16,32,64.

  • s b,cs_{b,c} word with cc copies of bb-bit signed quantities. Often the actually implemented values are restricted to b=8,16,32,64b=8,16,32,64.

  • e b,ce_{b,c} word with cc copies of bb-bit embedded quantities. An embedded quantity is an artificial interpretation as an unsigned value where b=7,15,31,63b=7,15,31,63.

The aim is the standard “type inferred” language system where a subset of the variables and expressions have explicit type annotations and all other variables/expressions have a consistent type inferred.

Big problem is that fixed-bit size integers are not closed under many useful operations. Get a slightly different interpretation of what the types mean.

Operations

A concrete atomic operation \oplus is a set of functions with various types (corresponding to the operations actually implemented on a particular CPU), eg, silly example {:u 8,16×u 8,16u 8,16,:u 16,8×u 16,8u 16,8}\{\oplus:u_{8,16}\times u_{8,16}\rightarrow u_{8,16},\oplus:u_{16,8}\times u_{16,8}\rightarrow u_{16,8}\}.

The most basic type inference is just standard Hindley-Milner type inference: e.g.,

  • given a:u 16,8a:u_{16,8} and cabc \leftarrow a \oplus b we can infer b:u 16,8b:u_{16,8} and c:u 16,8c:u_{16,8}.

  • equally given a:u 16,8a:u_{16,8}, c:u 8,16c:u_{8,16} and cabc \leftarrow a \oplus b we get an error that there is no operation with compatible type whatever type we try for bb.

“Intuitively” any “program” (i.e. sequence of assignments of expression trees to variables) has been successfully typed when

  1. Every “variable” has exactly one type.

  2. For any operation ff, given the types of all inputs and outputs there is a concrete atomic operation ff with that type.

  3. No arbitrary type choices have been made. (This basically says that for any inferred type, at enough points in the web of type inferences there was enough explicit annotation, combined with restricted instruction types, to fully determine what the inferred types must be.) This criterion is actually a bit more subtle dealing with embedded types due to lack of principal types.

Unfortunately this system is not able to do some pretty simple things for an actual instruction set.

Extension involves adding some additional embedded type values along with a set of “promotion”/“reinterpretation” rules. One tricky bit is that we no longer have a simple notion of a single principal type.

[note from Robert Smart: Hi David. Can’t quite work out how to send you a private message, so just delete this. I think my Closure Oriented Programming Language design addresses your issues. (Slightly inaccurate) doc here, and slides. Happy to give the talk anywhere. Will be in the Old Dart late Sept, early Oct for daughters wedding in Wales.]

category: personal