[Agda] dimly recalled strings?

[Conor McBride]

Hi Dan

On 28 Feb 2009, at 14:06, Dan Licata wrote:

> Hi Conor,
>
> On Feb28, Conor McBride wrote:
>> Hi folks
>>
>> Is there a handy String type I can get hold of by importing
>> something or invoking some pragma. I have some dim memory
>> of seeing such a thing, but perhaps it was another place,
>> another system...
>
> The string module in the library shows how to do this:
>
> http://www.cs.nott.ac.uk/~nad/listings/lib/Data.String.html

I'm clearly going blind. I did look for a Data.String before
I emailed, but failed to see it even though it was there.
That should solve my immediate difficulty.

As for primStringEquality, well, I'll uncensor the remark that
"grep Bool" gives an indicator of the health of a library. The
library uses a postulate for the proof that equal strings are
equal, but as things stand, that's gonna mess up computation.

What's the primitive deal? Is there any chance of making
equality decision, rather than Boolean testing, the primitive?
That way, if the strings are equal, you could at least provide
your actual refl. A postulate for the inequality is not such
a problem: no computation can get stuck because a proof of
"happiness" = "money" -> False is merely imagined.

If you look at the signature of the primitives, you'll note the
absence of dependent types. This makes it tricky to get very
far with evidence-producing operations on strings.

The string library's ok as far as *doing* things is concerned:
it's just not so hot for *seeing*. Which is one better than me,
I suppose.

All the best

Conor