Marc Weber wrote:
Excerpts from Adam Chlipala's message of Fri Dec 17 02:00:30 +0100 2010:
Marc Weber wrote:
== main.urs ==
val main : unit -> transaction page
val recIdTopLevel: a ::: Type -> a -> a
The important difference between the two definitions is that [recId] has
explicit type annotations for arguments and return type, while
[recIdTopLevel] doesn't. Type inference for Ur is undecidable, so
sometimes you need to annotate to satisfy the type checker.
So the type annotations in main.urs are for humans only?
No, signatures hide details of implementations, just like in ML. But
the following is true, too:
So the types of declarations in .ur and .urs file are compared after
type checking has taken place ..
That is, in checking a module, principal types are synthesized for all
its components, then these types are checked for compatibility with the
signature. The error message you gave was generated before the first
stage finished.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
