[Agda] dimly recalled strings?

[Conor McBride]

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...

I'm just hoping to experiment with naming the elements of
finite enumerations. This is, as ever, in the spirit of
constructing chunks of Epigram 2 inside Agda 2. Below, you
can find a treatment of inductive families as a universe,
which is how we plan to make them. The religiously inclined
will note that these are the Agda 1 families: you must
search your own conscience (or a selection of files called
things like OTT.agda) for equality.

If I had some kind of String (with a decidable equality),
it might be possible to equip this development with
constructors which resemble constructors.

Of course, this does rather raise the question of what a
good presentation of / library for String (or indeed List)
might be. It may be comforting to duplicate Haskell's
libraries, but it's inadequate. (I'm not saying "don't
copy Haskell", I'm saying "expect to bang your head" and
"keep thinking about it" and "don't standardize too
early".) Let me phrase this question more concretely: what
is a good library of *evidence-producing* tests and
decompositions for lists? how might we write a parser as a
view, exposing how a string is given by choosing a layout
for some structured data? But I digress...

Anyhow, universe follows shortly.

All the best

Conor


data Code (I : Set) : Set1 where
  ! : Code I
  _&_ : (S : Set) -> (S -> Code I) -> Code I
  _/_ : I -> Code I -> Code I
  HR : (H : Set) -> (H -> I) -> Code I -> Code I

record One : Set where

data Sig (S : Set)(T : S -> Set) : Set where
  _,_ : (s : S) -> T s -> Sig S T

_*_ : Set -> Set -> Set
S * T = Sig S \ _ -> T

[|_|] : {I : Set} -> Code I -> (I -> Set) -> Set
[| ! |]          R = One
[| S & C |]      R = Sig S \ s -> [| C s |] R
[| i / C |]      R = R i * [| C |] R
[| HR H hi C |]  R = ((h : H) -> R (hi h)) * [| C |] R

data Data {I : Set}(D : I -> Code I)(i : I) : Set where
  [_] : [| D i |] (Data D) -> Data D i

Partout : {I : Set}(C : Code I)(R : I -> Set) -> [| C |] R -> Code  
(Sig I R)
Partout ! R _ = !
Partout (S & C) R (s , c) = Partout (C s) R c
Partout (i / C) R (r , c) = (i , r) / Partout C R c
Partout (HR H hi C) R (f , c) = HR H (\ h -> hi h , f h) (Partout C R c)

partout : {I : Set}(C : Code I)(R : I -> Set)(P : Sig I R -> Set) ->
          ((i : I)(r : R i) -> P (i , r)) ->
          (c : [| C |] R) -> [| Partout C R c |] P
partout ! R P p _ = _
partout (S & C) R P p (s , c) = partout (C s) R P p c
partout (i / C) R P p (r , c) = p i r , partout C R P p c
partout (HR H hi C) R P p (f , c) = (\ h -> p (hi h) (f h)) , partout  
C R P p c

elim : {I : Set}(D : I -> Code I)(P : Sig I (Data D) -> Set) ->
       ((i : I)(d : [| D i |] (Data D)) ->
        [| Partout (D i) (Data D) d |] P -> P (i , [ d ])) ->
       (i : I)(x : Data D i) -> P (i , x)
elim D P p i [ d ] = p i d (partout (D i) (Data D) P (elim D P p) d)