IR: Let primitive expressions take manifest arguments

[nomeata]

Triggered by the clean-up necessary post #560 I finally fixe something
that bothered me a long time:

The IR pretends that primitive values are first-class functions, but
they are never compiled that way (and should not, and maybe even cannot,
as in the case of @serialize with a lying polymorophic type), instead
they always have manifest arguments.

So this gives PrimE an exp list.

At this point, there is no fundamental difference anymore between an
unary operation and a primitive with one argument. So unary and binary
operations and relations become just one such primtive operations.
This removes redundancy in IR-to-IR passes.

There is currently an OtherPrim constructor that still takes a string.
Eventually, this should disappear, replaced by an ADT of the actual
prims we support, e.g. a NumericConversion of (Type.prim, Type.prim)
constructor instead of the unstructured "Int->Word32" strings right
now. This would also allow for a nicer backend, as common code is
easiler shared between the many conversions.

[crusso]

Not a review yet, but it seems that doing it this way means we loose the ability to type-check primitive applications in the IR and just have to trust them. It would be nice if we could check at least some (better all) primitive applications in the IR are well-typed, even those that don't arise from source translation. I wonder if we should attach a perhaps optional type to OtherPrim or, better, an environment mapping primitives to their types. FTR, although I don't think we had any true polymorphic primitives, I believe some of the pseudo primitives (@await) are effectively polymorphic and are used at various instances of their true type within the code. Did you stumble across this?

[nomeata]

Not a review yet, but it seems that doing it this way means we loose the ability to type-check primitive applications in the IR and just have to trust them.

Quite the opposite, it makes it easier to add custom typing rule for each prim we care about! And polymorphic prims with special typing rules (Serialize, Show) are a main motivation of this.

[crusso]

Not a review yet, but it seems that doing it this way means we loose the ability to type-check primitive applications in the IR and just have to trust them.

Quite the opposite, it makes it easier to add custom typing rule for each prim we care about! And polymorphic prims with special typing rules (Serialize, Show) are a main motivation of this.

But, as it stands, have we not lost some of the typechecking we had? After translation from Syntax to IR, all the 'OtherPrims' are (currently) uncheckable and trusted, or have I missed something?

[nomeata]

But, as it stands, have we not lost some of the typechecking we had? After translation from Syntax to IR, all the 'OtherPrims' are (currently) uncheckable and trusted, or have I missed something?

They were uncheckable and trusted before as well, so this is not a regression (but a step towards fixing it).

[nomeata]

More precisely: Previously we blindly trusted the the type annotation on the prim, which had a function type, but could be anything. Now we blindly trust the type annotations of the prim’s arguments, and its result type.

[crusso]

More precisely: Previously we blindly trusted the the type annotation on the prim, which had a function type, but could be anything. Now we blindly trust the type annotations of the prim’s arguments, and its result type.

Is that entirely true? For prelude defined prims, we could rely on all uses in the IR that were derived from source carrying the same annotation we could check against. I think that aspect is still lost and it will be a little easier to construct bad IR terms... Would it not be easy to get the desugarer to insert the required type in the IR term and, perhaps later on replace that hack by a fixed OtherPrim typing function?

[nomeata]

For prelude defined prims, we could rely on all uses in the IR that were derived from source carrying the same annotation we could check against.

But we can’t rely on that! Passes may change annotations (some of them do traversals into types). Also, some prims work with more than one type (array_len for example).

it will be a little easier to construct bad IR terms...

I think it is just as easy. Why should it be harder now?

But yes, I do want to add type-checking of all prims to check_ir eventually (and maybe refactor the data type to not use strings but enumerate the prims)

[crusso]

It seems a shame to discard the type annotation here, when we could use it to check the argument/result typing in IR, but I can live with this...

[nomeata]

I think the typing should not come from an annotation (who knows where it comes from…), but a “real” typing rule for each primitive :)

[crusso]

I'll relent. LGTM.