thanks again for the provocation in your SIGPLAN blog piece, and the follow-up here focusing in on cast notation.

In his 2015 SNAPL paper “A Complement to blame”, Phil Wadler attributes the introduction of the ‘e : S => T’ notation (NB single colon!) to the 2011 POPL paper “Blame for All” (with Amal Ahmed, Robby Findler and Jeremy Siek), in the course of an interesting discussion of (the evolution of) notation for contracts, casts and blame over a 15–20 year period.

The discussion makes clear that it indeed can take a long time for the judicious choice of symbolism to emerge, measured in terms of cognitive load as you have it in your SIGPLAN article; in Phil’s case, he makes clear the appeal to two factors, left-to-right reading (for Western authors! a reminder to check our privilege, if ever there was one) order, together with the ‘free ride’ of being able to concatenate two casts, but *not* eliding the middle term (as Jeremy or others might unwittingly surmise as a further potential ‘free ride’).

Interestingly, Phil makes a separate point there, namely that using a C-like cast notation (he mentions Siek/Taha postfix ‘@’, but… mutatis mutandis) appears to require cast reduction to depend on type inference, in order to be able to push through casts at higher type in the ‘usual’ (Wrap) rule. So his justification for source/target casting (and the subsequent notational choice) has a semantic component to it, as well as the visual.

But it seems that if you take our 2019 WGT paper which uses an ‘unwrapped’ rule for higher-type casts, then such a rule would work perfectly fine, if more opaquely, written ‘@’-style (I’d write it, if I could figure out how to do so cleanly in markdown [fixed –MMG]). A pity we didn’t notice that at the time, though!

2019 WGT:

lam (x:A). M[x] : (x:A) -> B[x] => (y:C) -> D[y] -->
lam (y:C). let x = (y:C => A) in (M[x]:B[x] => D[y])

versus

lam (x:A). M[x] @ (y:C) -> D[y] -->
lam (y:C). let x = (y @ A) in (M[x] @ D[y])

And then the choice between notation ‘M @ A’ versus your preference for Carnapian functor/argument style ‘cast(M, A)’ (say), starts to seem a more modest cognitive gap to have to bridge… and with no ‘accidental’ free rides, either: ‘M @ A @ B’ can’t (seemingly) elide ‘A’ without doing some (object-level) reduction. But even then, how much of this is itself a ‘happy’ accident of our particular (syntactic and semantic) choices?