[isabelle-dev] Notes on datatype_new list

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Mon May 26 16:13:26 CEST 2014


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);

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




More information about the isabelle-dev mailing list