[Ur] Opaque ascription

Adam Chlipala adamc at impredicative.com
Wed Mar 28 09:20:57 EDT 2012

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.

More information about the Ur mailing list