Carl Patenaude-Poulin (Jun 29 2020 at 16:38): Carl Patenaude-Poulin (Jun 29 2020 at 16:38):Howdy! I'm playing around with formalizing generalized sudoku in Coq. "Generalized" in the sense that the game is parameterized by two nat values describing grid size. So I'm going to have a big chunk of (interdependent, type-heavy) code with those parameters. I'm going to want to instantiate that chunk of code by providing the parameters once, and receiving an object representing the specialized sudoku library.
Would you recommend using type classes? Modules? Sections? Something else? If you know of a relevant code example I could look at I would love that.
Enrico Tassi (Jun 29 2020 at 16:42):What do you mean by code? It is just definitions and lemmas, or Ltac, Notations, ...
Carl Patenaude-Poulin (Jun 29 2020 at 16:51):Minimally, definitions and lemmas; ideally, all of the above.
Enrico Tassi (Jun 29 2020 at 16:58):Functors can abstract almost anything over a module, that would be the most "generic" abstraction you have. Type Classes and co are nice because instances are found automatically, while you have to manually apply functors. But for your use case this does not seem to be a big issue, I guess.
Karl Palmskog (Jun 29 2020 at 17:13):@Carl Patenaude-Poulin are you aware of this? https://github.com/coq-contribs/sudoku
Karl Palmskog (Jun 29 2020 at 17:14):most people use a combination of (1) sections + ltac + notations and (2) one of: modules, type classes, canonical structures
Carl Patenaude-Poulin (Jun 29 2020 at 17:17):Nice, I'll try functors. Much appreciated.
Carl Patenaude-Poulin (Jun 29 2020 at 17:19):@Karl Palmskog I've heard of the sudoku library, I plan on looking at it once I get stuck
Last updated: Sep 30 2023 at 05:01 UTC