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
