It's interesting just how much of the debate in modern logic boils down to aesthetic preferences. On the other hand, I guess that if there were overwhelming practical advantages, there wouldn't be much to debate...
BTW, here's a "discussion paper" by Paulson and Leslie Lamport about typing in specification laguages from 1999: https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulso.... Paulson represents the "pro-type" view, but note that since that paper was written, there have been developments in mechanised theorem proving of untyped formalisms, including in Lamport's own (TLA+).
BTW, here's a "discussion paper" by Paulson and Leslie Lamport about typing in specification laguages from 1999: https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulso.... Paulson represents the "pro-type" view, but note that since that paper was written, there have been developments in mechanised theorem proving of untyped formalisms, including in Lamport's own (TLA+).