[isabelle-dev] Notes on datatype_new list

[Tobias Nipkow]

On 26/05/2014 16:13, 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:

I disagree. You should not obfuscate definitions that have an equivalent simple
version. Makarius spoke from experience when he said that people will look at
List.thy and they will get confused. That confusion should be minimized rather
than saying that other types (eg nat) are also defined in a terrible way. We
would not define them like that if datatype was already there at that point.

Tobias

>     __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);
> 
> In Lisp, I'd like to see how they "define" nil, cons, car, cdr, and cadadaar.
> 
> Even staying with Isabelle, all types defined before "'a list" and "'a option" are good examples -- products, sums, nats, unit, bools are all defined in a terrible way.
> 
> Now, with jEdit allowing to jump to the definition (as opposed to the documentation), I can see that this becomes a more acute issue Yet again I would argue that the "terrific" and "truly baroque" specification of "list" is better than products, sums, nats, unit, bools.
> 
>> I have almost never found destructors or discriminators to be useful.
> 
> I'd be curious to understand why. Perhaps you could elaborate in a separate thread. With multiple constructor datatypes, it is true that one often ends up needing a "case" expression anyway, but there are still many situations where you need the discriminator (or a '=' or '~=' that amounts to one) in an assumption, and then it's convenient to use the selectors directly, e.g.:
> 
>     lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
> 
> Jasmin
>