Agda-stdlib: Proposal: Setoid + Show + Parse

[mechvel]

[mechvel]

I propose to add to Setoid the fields of

showInstance : Show Carrier
parseInstance : Parse Carrier

The Show class is similar as in Haskell, this has been proposed earlier.
The Parse class has

     field  parse : Lexemes → (A × Lexemes) ⊎ String

Lexeme = String,
parse parses an element of A from a list of lexemes, it returns also the remaining lexemes.
If fails, it returns (inj₂ error-message).

Motivation:

1. Evidently Parse is as needed as Show is needed.
   For example, "2*x + (1/3)*x*y^2" is parsed to a polynomial with rational coefficients.
   It is not practically possible to write applications without Show or Parse.

1. These two fields would not give any difficulty for users, because if the user wants to ignore them, one sets defaultShow, defaultParse.

2. parse for a particular domain usually is composed with the parse parse instance for an argument domain. For example, parsing to A \times B applies the Parse instances for A and B respectively.

3. To add these two fields to Setoid is much better than only to keep separately the classes of Show
   and Parse. Because if they are separate, then one needs to define parametric modules like

module Foo (R : Ring _ _) ... (showInst : Show Carrier) (parseInst : Parse Carrier) ...

while it is more natural to write simply module Foo (R : Ring _ _) where.
Show and Parse instances need to be transmitted not as module parameters but as a part of Setoid instance.

In Haskell there is something similar to Parse (may be it is Read, readS, I do not recall), only this class (and also Show) is used as separate.
The function lexLots breaks a string to a list of lexemes, it needs to combine with ``parse''.

In DoConA Parse is called Read.

[gallais]

A few remarks:

• I don't see why this should be bundled with Setoid rather than being in its own class. I expect there are instances for which we won't have good definitions of show / parse (e.g. setoids of functions)
• With these types, it won't compose well: Parse has no notion that the leftovers Lexemes are smaller than the input and thus you can't write parseList : Parse A -> Parse (List A) as a guaranteed total function
• What about more informative types? We've discovered in https://github.com/gallais/agdarsec that a sum type as a result could make it hard to pinpoint where the error came from. Hence instrumented parsers.

[MatthewDaggitt]

I agree with @gallais. It's almost a near universal design pattern that display logic should not be entangled with the data itself.

One additional point:

• this would be non-backwards compatible in a major way, as users would have to adjust every single setoid construction, often in a non-trivial way

[mechvel]

G> I don't see why this should be bundled with Setoid rather than being in its own class. I expect there
G> are instances for which we won't have good definitions of show / parse (e.g. setoids of functions)

For such instances one sets showInstance = defaultShow; parseInstance = defaultParse,
where defaultShow returns always "dummy show",
and defaultParse always returns (inj₂ "dummy parse").

G> With these types, it won't compose well: Parse has no notion that the leftovers Lexemes are smaller G> than the input and thus you can't write parseList : Parse A -> Parse (List A) as a guaranteed total
G> function

a) It can be made total because (inj₂ "parse fail") is always possible.
b) For parsing a list, apply (map parse).
For example, in the DoCon system (written in Haskell) I write

coneEquations = map (smParse un) 
                                    [" u^2   - v^2 - x ",       " 2*u*v - y",      " u^2   + v^2 - z "]

In Agda, this will be

  map parse  (" u^2  - v^2 - x "    ∷     " 2*u*v - y"     ∷    " u^2  + v^2 - z "    ∷  [])

Most often, this is an easy way to input examples.

G> What about more informative types? We've discovered in https://github.com/gallais/agdarsec that a
G> sum type as a result could make it hard to pinpoint where the error came from.

I have experience in writing algebra in Haskell, and I see that even without more informative types the Parse class in very usable. And it is better to have it in the base of algebra hierarchy.
Also you can suggest and implement the corresponding optimization with a more informative type.

D> this would be non-backwards compatible in a major way, as users would have to adjust every
D> single setoid construction, often in a non-trivial way

Is adding defaultShow and defaultParse is a non-trivial way?
Also Standard library becomes non-backwards compatible usually each three months (probably it has to be so, for a while).

[gallais]

a) It can be made total because (inj₂ "parse fail") is always possible.

But then I'd argue it's a bug in the library: if we promise parsers, we should deliver
parsers rather than constantly failing functions.

b) For parsing a list, apply (map parse).

This presumes that we can generically split up the list of Lexemes into sublists
corresponding to each of the elements. I do not believe it is possible.

[mechvel]

a) It can be made total because (inj₂ "parse fail") is always possible.

But then I'd argue it's a bug in the library: if we promise parsers, we should deliver
parsers rather than constantly failing functions.

Why "constantly"? Each parser will say "cannot parse" for some unlucky input.

b) For parsing a list, apply (map parse).

This presumes that we can generically split up the list of Lexemes into sublists
corresponding to each of the elements. I do not believe it is possible.

The goal is not "to generically split up the list of Lexemes". The goal is to organize input in a possibly easy way in each particular case. For example, if one has the parse instance for A, then
(map parse) works for inputting to List A, as I show above.

The programmer
(map parse) is applies

[mechvel]

In my example above (map parse) is not applied to a list of lexemes. In this call parse is applied to each string, and each string for a element of A is input by hand. This is just an easy way to input things, only this.
Also there is a small difference between parse and parseFromString, the latter includes splitting a string to lexemes by lexLots. I my example with map I would rather write parseFromSring.
I do not know, may be this has made a confusion.

[mechvel]

Let me give an example.

Q = Rational              -- Fractions over ℤ.  It has a Field instance (with _+_, _*_; _/_, ...).
P = Pol Q ["x", "y"]     -- Polynomials in x, y with coefficients in Q.
                             -- It has a CommutativeRing instance  (with _+_, _*_; ...).
PP = P × P           -- Pairs over P. It has a CommutativeRing instance.

Inputting an example of an element of PP:

 res :  (PP × String) ⊎ String
 res =   parseFromString " ( ((-1/2)*x*y^2 + y^3),  (x + y - 1) ) "

It splits to the lexemes: "(" ∷ ... "," ∷ ... ∷ ")".
According to the Parse instance for PP (for its _×_ constructor) it breaks the list by "," and applies the Parse instance of P to the lexemes obtained from "((-1/2)*x*y^2 + y^3)", and then to the
lexemes obtained from "(x + y - 1)".
According to the specified types and Parse instances, "(-1/2)" is recognized as an input for a coefficient in Q and is parsed to a rational number,
where the lexeme "/" separates the lexemes for numerator and the lexemes
for denominator.
Further, "-1" is parsed to ℤ. And so on.

For the input of "x + //z", it will return (inj₂ <some error message>),

Seeing the result, the user needs to fix the input syntax in the example.
It depends on how the user implements the corresponding instance of Parse.

Here Parse works for the composition of constructors Fraction, Polynomial, _×_.

Example of inputting a list:

  res :  List ((P × String) ⊎ String)
  res =   map parseFromString  ("(1/2)*x + y"  ∷  "(-2/3)*y"   ∷  "y^3"   ∷ [])

Then, one can extract the values of P from the parses of kind (inj₁ _) in this list.
This is not parsing a list, it is inputting an example of a list of concrete polynomials by applying
(map parseFromString).

This is a tool for organizing input of examples.

What is wrong here?

[mechvel]

I need to add the folloiwng.
I programmed such things in Haskell, and what I demonstrate above for Agda, is a project, it has not been tested.

[gallais]

According to the Parse instance for PP (for its _×_ constructor) it breaks the list by "," and applies the Parse instance of P to the lexemes obtained from "((-1/2)xy^2 + y^3)", and then to the lexemes obtained from "(x + y - 1)".

Now do the parser for (PP × PP): there are 3 commas and I'm betting the input
string will be split the wrong way.

Parsing a pair (A × B) goes like this:

consume '('
parse an A
consume ','
parse a B
consume ')'

which is not equivalent to breaking the string on the first comma you find
and parsing an A on the first part and a B on the second part.

[mechvel]

This is only an usual _parsing_. For an opening parenthesis it finds its closing parenthesis, and so on.
In an Agda program you write things like

((1 , 2) , [ true ])  ∷  ((3 , 4) , [ false ])  ∷  []

, and the Agda parser (hopefully) parses this. And you are not surprised by this.
Similarly each programmer has to define the Parse instances -- if she/he needs to parse elements according to the constructors defined in one's program. An user will program it own parser by implementing Parse instances.
If one does not need such, and if a field for Parse is in Setoid, then one sets only two words instead: parseInstance = defaultParse.

Haskell standard library has the Read class for this, and the function reads.
And it puts String = List Char, Lexeme = Char.
For example,

 s  :: String
 s = ...
 case  reads s  ::  [(Integer, String)]    -- using a standard Read instance for Integer
 of 
  [(n, _)] -> ([n], "")                           -- an integer parsed successfully 
  _         -> ([] , <error message>)    -- parse failed 

Agda standard library has not such items.
I have discovered that it is better to additionally introduce a more generic parser, with Lexeme = String, with the user program providing a table of operator lexemes, a list of parenthesis lexemes,
with the Parse class.

To start with:
if Agda standard library introduces something similar to the Read class of Haskell standard library,
and its standard instances, this will be good.
For example, is it natural that we have not a standard way to read Integer from String ?
To read Rational from String ?
(Haskell standard library has such, as I recall).
Further "Rational" is a poor approach. Agda is a good language that fits scientific symbolic computation. A sensible approach, that deserves Agda, is more generic: Fraction R, where R is an instance of GCDRing. Then, the programmer (or better, Standard library) needs to implement the Parse instance for (Fraction R) as depending on the Parse instance for R.

If Agda standard library decides to introduce an analogue of Haskell's Read class, then may be, it has
sense to consider a more generic approach of Lexeme = String and the "parse" operation signature as I suggest above.

Apart from the Parse question, why has it sense to keep showInstance : Show Carrier
in Setoid ?
I expect that most users need to print their program results to String. Need they?
A program often returns an element of an instance of standard classes Magma, Semigroup, Monoid, Group, Semiring, Ring, ...
"main" needs to print such an element to String, and then to output.
This needs implementing Show for the corresponding instances of the above classes.
Such an implementation of Show usually appears in a parametric module. For example,

module _ ... (G : Group _ _) (showInst : Show (Group.Carrier G))
  where

Another module has (M : Magma _ _) in parameters, the third module has
(R : Ring_ _) in parameters. And there are a dozen of such modules.
And all their headers are polluted with (showInst : Show (Foo.Carrier Foo1)).
If showInstance is a field in Setoid, then this pollution is removed.

Also it is natural to expect that in programming any element of almost anything can be printed to String. For a domain of another nature one sets showInstance = defaultShow.
That is what is suggested.

People do not think of such things, probably, because there are too few users, and they use Agda not for practical computation but as somehow a toy system. This is why Agda library has not fast Nat arithmetic, has not Show, Parse, has not a generic GCD class, Fraction constructor, and other important items.

This subject of Show and Parse is not so extremely important for me, though. Because I can define them as non-standard, and continue polluting module headers with
(showInst : Show (Foo.Carrier foo1)).

[JacquesCarette]

I am strongly against adding non-mathematical features to mathematical structures such as Setoid.

This kind of experiment has been done in OO for a long time (look at all the stuff thrown in to the base Object class in Java), and has been deemed a mistake. And, of course, there are MANY kinds of Setoid (and Group and ...) which are not Showable at all. So it would be a severe mathematical mistake to force them to have such an implementation. And having a dummy Show for those would defeat the point entirely -- both of having Show at all, and of being in a 'total' language!

Yes, there should be a structure for Show, and Parse, and it should be easy to do 'mixins' so that one can decide to have "showable groups" easily. But it should not be done as suggested here.

Underlying this proposal (and buried in the rationale above) are true needs of users that ought to be addressed.

[mechvel]

I need to correct myself a bit.
I wrote "Haskell Read puts Lexeme = Char".
This is not so, it is still String. Because Haskell has lexLots that returns a list of strings (and something else). But reads parses from String.

[MatthewDaggitt]

Strongly agree with @JacquesCarette.

@mechvel, I think we all agree that the standard library needs both parsing and display classes. However I think there's agreement amongst others that this proposal is not the way to about it. It should be possible to build combinators that combine the display and parse constructs Setoids and other structures in the way you desire. As for concern about module pollution parameters, in a properly designed project the program output should be centralised in just a few files, so it shouldn't be a widespread problem.

I'm closing this issue, but feel free to continue the design discussion in #569

[mechvel]

I am strongly against adding non-mathematical features to mathematical structures such as Setoid.

Well, "showInstance" does not look as "mathematical" as Setoid.
But we deal not with mathematics itself but with programs for mathematics.
I somehow doubt.