Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp> mentions ``%''
as possible alternative to ``:'' in the labelling syntax and writes:
 > 
 > In this case, I suppose we should read `%' as `is'.

I have difficulties with this --- after all
it is a ``percent'' glyph,
and more comfortable in a division context.

It would even be easier for me to read ``&'' as ``is'',
after all, ``&'' is ``et'',
so there is only one ``s'' missing to ``est''.    ;-)


For me, an additional argument for keeping ``:''
is that ``:'' is punctuation,
which I find appropriate for this use,
while ``%'' and ``#'' look more like infix operators.

I definitely prefer ``:''.


Concerning the use of ``:'' in type signatures,
I would write the blanks even if I didn't have to.
(I do so in Haskell.)


Regards,

Wolfram