Turns out breaking tell constraints into tiny pieces is a much bigger pain in the arse than doing it for ask ones because you're not supposed to know anything about what you're writing into

I can't help thinking that whatever else is going on, social media has just inherently become more antisocial for me over the last decade.

I'm not saying I can't nerd out on here, but I don't know if making actual friends without f2f contact is going to be much of a thing.

A lot of that is, tbh, about privacy: the granularity of locking posts on some of the older sites is clearly not compatible with Mastodon. It's always been necessary to have room to be more honest than one can afford in front of the modern internet.

Risks to Mastodon with increasing popularity 

Interesting comment on Hackernews regarding a possible scenario/long term risk should Mastodon threaten the corporate sphere of social media.

news.ycombinator.com/item?id=3

@Ellbee This is me saying hi from another instance and it's as easy as the toot text suggests!

It's more of a pain to see what you've said from here because I don't follow you here, but if I did it'd be just fine. Keeps this instance's running costs down.

I am once again considering bolting on vectors to my toy logic language stuff so I can write zipWithN (with lengths having to match) once and for all...

The very bad solution is to check if I got the exact same input state back - such efficiency!

I think what I want to do for many reasons is build a little consumption machine and rework everything in terms of it

Show thread

Started hacking up a parsing applicative in Agda as an exercise, have got most of it sorted but run smack into an issue I know a very bad solution to and some more sensible approaches

Haskell wouldn't do this one to me, but it'd screw me over when I used it instead: trying a non-consuming parser many times

LaTeX 

$\mathrm{this} \in \mathrm{shitpost}$

$shitpost = 💩​✉️​$

I'm still very much in beginner mode when it comes to Agda. On the bright side this means emacs doesn't get a chance to piss me off.

Meanwhile I'm in a whole universe of pain, but it'll get me a twofer of life being easier later on so I guess I'll take it.

LaTeX support and no preview option I can find doesn't seem great?

Oh look, a world. I'm sure something can infer my response for me.

types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.