[Ur] Opaque ascription

[Adam Chlipala]

Ron de Bruijn wrote:
> In Robert Harper's book 'Programming in Standard ML' in section 20.2 
> named 'Opaque ascription' he uses the :> notation.
>
> The : notation is used for transparent ascription in Standard ML (and 
> I assume also in Ur/Web).
>
> http://en.wikipedia.org/wiki/Standard_ML also explains this.
>
> It seems that you are saying that Ur's : == SML's :>, but then why has 
> SML's : been left out in Ur

Right; Ur only includes opaque ascription.  I've never liked transparent 
ascription.  I find that such a feature makes it too easy to be lazy and 
not give a self-contained interface for a module (which reduces 
documentation quality), by letting implementation choices for abstract 
types leak through automatically.