Change data types, adding some fixed width

[Bastacyclop]

This will be useful for image processing applications in particular.

[Bastacyclop]

In particular float becomes f32 and float4 becomes vec(4, f32) to avoid confusing vector width and bit width.

[michel-steuwer]

👍 I would still like to see a reply to the comment 💬 I made.

[michel-steuwer]

Do we want to enforce here that size is a Cst and that it is one of: 2, 3, 4, 8, 16?

[Bastacyclop]

Maybe we want to write some vector-width generic code with types such as nFunT(w => f32 ->: vec(w, f32)? Although you could still use VectorType(w, f32) if you wanted.

[Bastacyclop]

I feel like such checks would be better suited when you try to generate code with a specific backend/target?

[michel-steuwer]

This form of polymorphism is dangerous anyway because the type suggests that we can build a VectorType(w, f32) for all w: Nat. But that isn't true.

We will have to be looking a bit more carefully how to define the VectorType on the formal side, I guess.

[Bastacyclop]

Maybe we can open an issue about that? There is also the issue that elemType should be a ScalarType ideally but we have no way of creating ScalarTypeIdentifiers for example.

[Bastacyclop]

Maybe we want subtyping constraints (#11) but also nat constraints?