The design of 'free objects'

[JacquesCarette]

This issue is a place to discuss the design of what we'd like. @jamesmckinna gave a first PR (#1962 ) that has been long stalled (because of, well, me!)

So let's try to get it going again. My biggest worry is the ridiculous amount of boilerplate. This is not @jamesmckinna 's fault, it is inherent to attempting to define 'free object' completely by hand by unrolling all the definitions. Not only are the definitions unrolled, a whole lot of useful 'kit' is also provided (normally a wonderful thing!) also by unrolling all the definitions. Wikipedia's Free object article is quite readable to get a sense of what all that is. Its list of free objects shows us how much this is going to explore. Plus that list is far from complete.

Maybe we should instead bite the bullet and do this properly categorically.

Another approach would be to follow something largely along @jamesmckinna 's design but, rather than doing it all by hand, doing it via meta-programming. We couldn't do it using Agda's own meta-programming features (I don't think) but we could certainly do it in Haskell -- maybe even by using Agda itself as a library. (Maybe @TOTBWF might be interested in that.)

[JacquesCarette]

I should also link in #2287 "Mechanize the Algebra hierarchy". I think that the design space for both are quite similar and should likely have a similar solution.

[jamesmckinna]

Thanks @JacquesCarette for opening this issue after all my nagging about it.

I guess my original 'by hand' version(s) were a ham-fisted attempt towards provoking such discussion (as well as attempts to contribute a version of Free to a library that did not have it in any recognisable form... when I was actually after Free Ring and free R-module, and needed a warm-up exercise...), and as a way of exploring the space of how to present FreeX as a syntactic construction based on the term algebra for the signature of X. And... syntax breeds boilerplate? (I don't think it's merely a consequence of my own more verbose, 'didactic' style of writing Agda?)

The abstract 'universal property' version of FreeX seems much closer to a 'finally tagless' semantic (Church-style) characterisation, which clearly has advantages in (any) functional context... but for the 'usual' problems of Church-style wrt induction/pattern-matching as a 'programmer's API' for the construction, as well as universe level polymorphism in the predicative setting.

(Omitted: Potential digression about Dedekind's (1887) approach to Nat as the initial SuccessorSet, and the flaw in his work in not actually establishing existence properly? Do we want Nat in stdlib as a data declaration, or characterised abstractly as an NNO? It's tempting to say, pace library-design guidelines about non-duplication of concepts and proofs, that we want both... but 'programmers' seem definitely to want 'data+pattern-matching=programs'... ;-))

As well as, perhaps, a lot of hidden 'boilerplate' (shared between all approaches?) as to what is required even to state the required universal property for a given X... again which I ended up rolling by-hand (at a point in stdlib timeline where we didn't even have bundled homomorphisms as first-class things?!). Writing down the 'h is the unique X-homomorphism which agrees with blah on generators' definition is already boilerplate of its own, surely?

Each representation will then cash out differently as to proving the relevant 'existence' and 'uniqueness' properties of such h, again with a strong bias on my part towards the syntax/data 'programmer's API' approach esp. to existence...

(More later, but I thought it worth putting those two markers down: I think each approach carries 'boilerplate' with it, but we seem to have different tolerance levels regarding the two, as well perhaps as ideological/religious positions as to what is tolerable, and why...? If what I have written so far seems too ranty, happy to re-edit ...)

As to meta-programming as an approach to making such constructions generic/generative wrt a given signature+axioms, that would be good (modulo the fitness-to-purpose of existing tooling), and all the better if it can be internalised via an Agda universe construction. We should also look more closely at the frex work esp. implementation in idris2 on this?

[JacquesCarette]

Yes, definitely need to look at FREX and its idris implementation.

All these ponderings have made me realize one thing: we already have, at least, all of "FreeMonoid" already implemented in stdlib (because it's List). And we don't have it under "FreeMonoid". And maybe that's a good thing.

Maybe we should implement 'Free' via universal properties, and implement a handful of specific cases "by hand" because they are so pervasive. And we don't have to give them overly fancy names (Maybe isn't called FreePointed after all).

Data.Polynomial.Infinitary is probably nicer than Free Ring (even though it's longer).

[jamesmckinna]

I feel strongly that it's (doubleplus emphatically) not a good thing to conflate FreeMonoid (as an algebraic concept) with Data.List.List as a computational one... the latter is only the underlying carrier of the former, and worse, the existing constructions on Maybe/Pointed mix up two distinct 'free' notions: freely adding a point to make something pointed, and freely adding an identity to a Semigroup to make a Monoid... corresponding to distinct left adjoints? (even if related by some distributive law?)

Maybe Data.Polynomial has a place (why Infinitary though?), again as a computational artefact (it certainly appears in Tactic.RingSolver, and might better be lifted out?), but characterising it as the underlying carrier of the Free Ring is another matter? Or have I not understood your point? esp. if we end up using/needing different polynomial representations for different applications?

In a simpler setting: Data.Nat or FreeSuccessorSet (NNO)? Surely the latter is of independent interest to the former? cf. #2446