Multi-classed Software Engineer/Constructive Mathematician. Sometimes plays video games sort of fast. Puts topoi in your computer. https://nitter.cf/t.co/iFlKRVeGpN
Joined March 2019
- Tweets5.9K
- Following21
- Followers727
- Likes556
The foldl hackage.haskell.org/package/… package is one of the most remarkable bit of the Haskell ecosystem. Turns out, we can make it better. I mean worse. I mean… maybe? 1/11
Apparently, State is already slower than an hand-rolled scan, and Day doesn't really make things worse. On the other hand it seems to do (much!) better than a zipless Arrow-based implementation with foldl (which produces pairs original/computed on the first scan). 10/11
So maybe the Arrow implementation is significantly better than that of foldl. But I don't know that for even remotely sure. Anyway, this was a short experiment, we didn't carry it very far. You can find it here github.com/jameshaydon/janus… 11/11
So, I was thinking. When we write ⊢A→B ∧ ⊢A ⟹ ⊢B in inference rules. What is the pattern A→B as a mathematical object? 1/8
Now our conditions become g∘f≤id and id≤f∘g (hint: id is minimal). That is f and g form a Galois connection (equivalently ∀a x, x≤f(a) ⟺ g(x)≤a). I think it generalises: in a subtyping situation, you don't typically have x=f(a) only x≤f(a). Exactly what shows up! 7/8
This is important dl.acm.org/doi/10.1145/38286… . For instance, when you have a linear Int# in Haskell, it's the same as having an unrestricted Int#. You want the type system to understand that, that's what the authors call mode crossing. 1/2
