[isabelle-dev] Additional type variable(s) in specification

Makarius makarius at sketis.net
Thu Dec 2 17:46:20 CET 2010

On Thu, 2 Dec 2010, Brian Huffman wrote:

> But if we had something like a "fixes" clause for types, it would look 
> nicer and indicate the intention unambiguously, making a warning message 
> unnecessary:
> locale count = fixes_type 'a assumes ex_inj: "EX f::'a => nat. inj f"

This would be a substantial change in the way "polymorhphism" works in the 
system.  IIRC, Moscow ML introduced such an extension to Hindley-Milner 
typing and consequently caused some serious breakdown.


More information about the isabelle-dev mailing list