[isabelle-dev] typrep?

[Florian Haftmann]

Hi Amine,

> wrt to d) and e) (Users/Developers, HOL is difficult).
> This theory is for now a "using" HOL, but of course I want to develop it
> in a manner that it could become part of HOL.
> The situation you mention in d) and e) has not to be this way and we
> should not take it for granted that HOL is complex to develop etc. The
> social and psychological consequences are not very nice if it becomes a
> rule (my opinion).

I share your concerns, though I would see the subtleties of HOL rather
technical consequences than a "rule".

> Isabelle/HOL is remarkably more user friendly than many other system.
> 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.
Whether the situation became worse in the past years -- in my view it
got even better, but this may be subjective due to my experience.
Perhaps the focus of problems shifted.

> If typerep is mainly used in connection with code-generation (as I
> understand) isn't it an option to generate all these instances when you
> call any code-generation facility? Or even in prior step e.g. called
> setup-every-thing-that-has-to-do-with-code-generation?

This is even worse:  in the first case, you won't be able to join any
(!) two theories which invoke code generation since you have a lot of
unredeemable duplication.  The problem with the latter case is: there is
*never* such a point.

> Besides, I don't object to the idea of typerep at all, I am just
> confused why the names clash? (Wasn't this the problem). In other words
> is this problem unavoidable, so that one needs a hard
> discussion/decision like typerep or no typerep?

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

Cheers
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090121/1d441aa9/attachment.sig>