Description
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.)
Activity
JacquesCarette commentedon Jan 1, 2025
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 commentedon Jan 2, 2025
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 afterFree Ring
and freeR
-module, and needed a warm-up exercise...), and as a way of exploring the space of how to presentFreeX
as a syntactic construction based on the term algebra for the signature ofX
. 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 initialSuccessorSet
, and the flaw in his work in not actually establishing existence properly? Do we wantNat
instdlib
as adata
declaration, or characterised abstractly as an NNO? It's tempting to say, pacelibrary-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 instdlib
timeline where we didn't even have bundled homomorphisms as first-class things?!). Writing down the 'h
is the uniqueX
-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 commentedon Jan 3, 2025
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'sList
). 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 thanFree Ring
(even though it's longer).sum
andproduct
(and their properties) fromData.List.*
#2553jamesmckinna commentedon Jan 20, 2025
I feel strongly that it's (doubleplus emphatically) not a good thing to conflate
FreeMonoid
(as an algebraic concept) withData.List.List
as a computational one... the latter is only the underlying carrier of the former, and worse, the existing constructions onMaybe
/Pointed
mix up two distinct 'free' notions: freely adding a point to make something pointed, and freely adding an identity to aSemigroup
to make aMonoid
... corresponding to distinct left adjoints? (even if related by some distributive law?)Maybe
Data.Polynomial
has a place (whyInfinitary
though?), again as a computational artefact (it certainly appears inTactic.RingSolver
, and might better be lifted out?), but characterising it as the underlying carrier of theFree 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
orFreeSuccessorSet
(NNO)? Surely the latter is of independent interest to the former? cf. #2446Algebra.Lattice.Properties.BooleanAlgebra.Expression
#2702