Am 26.05.2014 um 12:34 schrieb Lawrence Paulson <l...@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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to