Show more
lyxia boosted

Kind of weird that initial Free was the first variant to become popular, given that it's slow and forces the user to store the continuation in their own datatype

lyxia boosted

The final encoding of freer monads is both faster and more intuitive than the initial encoding. As a ReaderT IO person, I'm convinced final freer is a good alternative for most use cases

I'm gradually moving my workflow from emacs+proofgeneral to vim+coqtail, so I can be back to 100% usage.

lyxia boosted

Exécuter un programme sur Windows, c'est comme lancer une jarre de café par la fenêtre.

lyxia boosted

Why does category theory exist? 

lyxia boosted

In , ever wonder what goes in the brackets in `destruct x as [...]` or `intros [...]`? Wonder no more: coq.inria.fr/distrib/V8.8.2/re

It has some neat features if you're into unreadable one-liner tactics (that noone is going to read anyway) like me.

lyxia boosted

Contemporary Canadian illustrator Julia Iredale, known for her depictions of curious surreal scenes and landscapes #womensart t.co/a5G4NQZbgi

In the Space Dandy there are "book-type aliens", which are not sentient nor moving on their own, but are parasites which manipulate other beings to think and move for them. They feed themselves by filling their pages with information. So, books.

lyxia boosted
lyxia boosted

@davidk01
Interpreters are "just" compilers which target behaviors. ;)

lyxia boosted

This is beautiful and I've never thought about this before:

the convention we have in Unix to pass pre-opened stdin/stdout/stderr fds is not just a nice way to tell the program where to read its input from and output its result/logs to; it is exactly how capability passing should work in a capability-based system. This also is another reason why accepting an -o option (for "output file") is a bad idea.

lyxia boosted

We wrote an open letter (in French) to protest against France's renewal of their Elsevier subscription for 4 more years:

blog.dissem.in/2019/lettre-ouv

lyxia boosted

My, I like new changelog links on @hackage posts!

Now I want to give every package an ActivityPub outbox and a profile page. And that brings me back to implementing a #Fediverse capable feed server.

lyxia boosted
Show more
niu.moe

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !