Follow

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 blog.gelez.xyz/type-produit/)

Proofs are done[§], I need to actually write the explanation now x).

[§]: gist.github.com/lthms/8f93f3c4

Another nice lemma to prove :
α * (β + γ) == α * β + α * γ.

Show thread

And… non_empty_list α == α * list α

This one was tricky to prove (I wanted to prove it by rewriting, but couldn’t ): )

Show thread

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)

gist.github.com/lthms/1802b29e

Show thread

@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

@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!

Sign in to participate in the conversation
Mastodon

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!