[isabelle-dev] Notes on datatype_new list

[Makarius]

On Mon, 26 May 2014, Jasmin Christian Blanchette wrote:

> Am 26.05.2014 um 12:34 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
>
>> What new users see when they look at the actual definition of lists is 
>> not that important. There are many, many situations where the actual 
>> definition of something is much more complicated than the idealised 
>> version that one would use for teaching.
>
> Indeed, this is an old observation that has been repeated over and over 
> throughout the history of computing. The definitions of most library 
> functionality in various programming languages looks obfuscated. Take 
> for example "stdio.h" in C. On my "user-friendly Mac", it looks like 
> this:
>
>    __BEGIN_DECLS
>    void	 clearerr(FILE *);
>    int	 fclose(FILE *);
>    ...
>    int	 fgetpos(FILE * __restrict, fpos_t *);
>    char	*fgets(char * __restrict, int, FILE *);
>    #if defined(_DARWIN_UNLIMITED_STREAMS) || defined(_DARWIN_C_SOURCE)
>    FILE	*fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_3_2, __DARWIN_EXTSN(fopen));
>    #else /* !_DARWIN_UNLIMITED_STREAMS && !_DARWIN_C_SOURCE */
>    FILE	*fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_2_0, __DARWIN_ALIAS(fopen));
>    #endif /* (DARWIN_UNLIMITED_STREAMS || _DARWIN_C_SOURCE) */
>    int	 fprintf(FILE * __restrict, const char * __restrict, ...) __printflike(2, 3);

One could blame the C language for being obsolete and requiring all this 
extra rubbish, but even Scala can compete here.  Scala libraries are easy 
to use, but only a few elect experts know how there are implemented.
See again 
http://stackoverflow.com/questions/1722726/is-the-scala-2-8-collections-library-a-case-of-the-longest-suicide-note-in-hist

I've implemented collections myself until Scala 2.7, but starting with 
Scala 2.8 I am flying blind, and merely hope to get my own little add-ons 
over continued changes by the experts, e.g. see 86f9c6912965.


For HOL we have our own history of complexity in the bootstrap process. 
Everything below theory Main might be somehow obscure.  Often it is 
possible to do some peephole optimizations to reduce the obscurity to a 
reasonable level.

The same for Pure.  The new @{here} antiquotation at least gives the 
formal declaration point of type "fun", but without any clue how it is 
really done.


 	Makarius