The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

Hi

I certainly agree that the current Ascii module isn't that convenient,
but it seems quite unclear to me that switching to a type with 256
constructors will help that much. Ok, there are corners of the Coq 
implementation
that we certainly could/should improve for better handling of big inductive
types, and indeed having a primitive encoding for the _ pattern could help.
The extraction is already doing something about it, and concerning the kernel
it seems to be on the roadmap, only waiting for somebody with some time
to code it. But sooner or later, we'll have to handle true binary functions
on ascii, for instance when considering ascii as bounded integers and hence
defining an addition on them. 
Another approach is currently experimented by Benjamin Grégoire: bringing
a few builtin native data-types to Coq, directly interfaced with the
underlying hardware. If I remember correctly, he mainly focuses on bounded
integers (31-bits) and arrays, but chars are also to be proposed this way.
A preliminary version of his work is in the branch "native" of Coq svn.

By the way, what about also reforming the module String someday ? I tend
to think that having an Haskell-like vision where string = list ascii
would be nicer than the current specialized pseudo-list type. This way,
many functions could be shared between String and List. Of course,
remain to be check that we could keep the specific parsing/printing
of strings even when string = list ascii...

Best regards,

Pierre L.