[isabelle-dev] typrep?

[Chris Capel]

On Wed, Jan 21, 2009 at 02:44, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Amine Chaieb wrote:
>> Isabelle/HOL is remarkably more user friendly than many other system.

If this is indeed the case, I'm glad I picked it, rather than some
other system. I found the learning curb quite steep, though I believe
I am near the leveling-out part. But my opinions on how to improve
that have to do with building a new user interface catering to
novices, which I am working on myself, and perhaps a couple new
tutorials aimed a little lower as well. :)

>> All this effort of the past decades seems to have negative back effects
>> in the past years: Many Developers stand before complex situations
>> nobody or sometimes only one understands. Don't you think it is time to
>> invest in a more developer-friendly Isabelle/HOL ?
>
> Not sure whether user-friendliness means less developer-friendliness.

This is not generally true in my experience, though of course Isabelle
could be different.

My uninformed opinion in this particular instance is that the problem
could be mostly solved with better error reporting first, and perhaps
with a rearrangement (as you suggest) second. Adding more error
reporting doesn't increase the developer's burden in the long term,
although rearranging things can sometimes. It seems to me that helpful
error messages are key to user-friendliness. The error in Amine's case
should say first which statement in which theory instantiated each of
the conflicting typerep instances, and what the derived theories are
that are immediately being merged, and second give a hint as to the
need to rearrange things.

If the interface is helpful enough when you do something wrong, you no
longer have to be an expert to avoid getting stuck at errors.

> The problem is: you can instantiate every type class only once to a
> particular type.  There is no way to get around.

Here, I am completely ignorant as to Isabelle's workings. But could
you not somehow cache the first instantiation at the heap level and
then check before the second to see if it's cached already? This may
seem ugly, but for classes that are instantiated implicitly, maybe
it's the best way.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)