I’ve finally started to work on my next blogpost: Why algebraic datatypes are “algebraic,” explained.
Inspired by @na and her nice write-up (in French, here https://blog.gelez.xyz/type-produit/)
Proofs are done[§], I need to actually write the explanation now x).
[§]: https://gist.github.com/lthms/8f93f3c4b9527b97997cada2a05b8902
Oh, and also, list α == unit + α * list α
And… non_empty_list α == α * list α
This one was tricky to prove (I wanted to prove it by rewriting, but couldn’t ): )
Ltac can be used to do fun tricks, like computing the type of a fold function for any given datatype, as long as we can provide the “canonical form” (like unit + a * list a for lists)
https://gist.github.com/lthms/1802b29ea4b3afa06ca625808da19ebc
@lthms j'étais jamais allée aussi « loin », mais du coup c'est vrai que ça marche aussi 😲
@na C’est avec ce genre de tricks qu’on peut générer des fold automatiquement pour n’importe quel dataype :D
@lthms I don't get it but I appreciate it
@charlag Yeah. Explaining it, like, really explaining it for other to get it will be challenging x).
@lthms I think I just don't know what's "fold function" unless it's... "fold" function
@charlag It’s just “fold” function indeed; a la fold_right of OCaml for instance
@lthms hey lthms! eager to read it, your blog got me interested in Coq, especially its article on the formalization of a stack!
@jco glay you like my articles! Although I am not sure to know which one you are referring to when you mention stack formalization tbh!
@lthms yeah it was more about annotating functions with their specification, taking the exemple of a list or something like that...
@jco oh yeah, I see which ones. Glad you liked it!
Server run by the main developers of the project 
It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!
Another nice lemma to prove :
α * (β + γ) == α * β + α * γ.