[isabelle-dev] typrep?

[Florian Haftmann]

Concerning typerep, an ease could be achieved:  as Alex pointed out,
"size" (and also "eq" and "itself") are bootstrapped rather early,
whereas "typerep" appears after List.thy.  One solution is to move
"typerep" up in the hierarchy:

a) Move Nibbles and Characters to a distinct theory Char.thy just right
after datatype.

b) Therein, provide an explicit type isomorphic to char list;  this is a
duplication which does not harm since it is only used as a technical
facility for code generation, not much logical properties are needed.

c) Typerep.thy then could immediately follow Char.thy and is
incorporated via Code_Eval.thy (stupid name btw.) in Plain.thy.

d) In List.thy, the conventional strings are established as types string
= char list

This would yield a complete setup of "typerep" since Plain.thy, which
leaves only a minimal risk of producing "bad" thygraphs.

	Florian

Florian Haftmann schrieb:
> 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
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

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/1474aae7/attachment.sig>