Re: [isabelle] A course based on Isabelle/HOL and some feedback...



On Thu, 26 Apr 2012, Thomas Genet wrote:

-- It is a bad idea to use a variable name like id in a function
 equation, e.g.:

fun f:: "nat => nat"
where
"f(id)=id"

 OK, the error message says:
*** Type error in application: incompatible operand type
***
*** Operator:  f :: nat => nat
*** Operand:   id :: ??'a => ??'a

 and a (careful) student may understand that 'id' is already defined as a
 function etc... however this is far more difficult to find when the
 function has 10 complex equations.

This is one of these scoping errors that then lead to a conflict with the type constraints imposed by already defined entities, and are thus discovered indirectly. The type checking phase could be a bit more ambitious to maintain precise position information and report that (which is technically not so easy and might require one or two more release cycles to materialize).

But the actual scoping is already represented quite nicely in current Isabelle2011-1 right now, if you use Isabelle/jEdit and rely in its "Haribo effect". This means the sources are painted in funny colors according to the role of identifiers. The Prover IDE also has the magic CONTROL (or COMMAND) key, which asks the system to explain the formal status of some piece of source.

So the above "id" would have come out black (constant) instead of the expected blue (free variable), and its tooltip would have said "constant Fun.id", with a hyperlink to jump to its definition in main HOL. So students would have to spend less energy divinating the meaning of the text themselves.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.