Brent Yorgey

I wrote something for my students reflecting on the current cultural and technological moment - a collection of important things I want to say that I'm never quite sure how or when to say in class.

http://ozark.hendrix.edu/~yorgey/forest/00FD/index.xml

Finally finished a just-for-fun, completely-from-scratch constructive proof of the Fundamental Theorem of Arithmetic (just the existence part, not uniqueness (yet)) in #Agda. Took me about 10 hours and 750 lines of code. Fun times! Will probably turn it into a blog post at some point.

I was testing out a Swarm scenario that starts by generating a random permutation of characters. I ran it and this is the first random permutation that was generated. 👻 😱

So far I've managed to prove that

map length . transpose . map (replicate ()) = foldr (\n -> zipWithExt (+) 0 (replicate n 1)) []

where

zipWithExt :: (a -> a -> b) -> a -> [a] -> [a] -> [b]

zips the lists together with the given function, using the provided value of type a to fill in missing values from the shorter list.

This is very similar to @oantolin@mathstodon.xyz 's implementation, and does indeed get rid of the unit values, but it turns out the unit values themselves weren't the problem: the real problem is that we want to avoid the use of replicate to encode Int values in unary. This version with foldr is still O(sum p), i.e. linear in the total size of the partition, but we want an implementation which is O(length p + maximum p), i.e. linear in the number of parts plus the size of the maximum part. I think my fiddly directly recursive implementation achieves that, as does @das_g@chaos.social 's implementation, but I want to figure out a way to derive those from the direct specification.

I guess the idea would be to expand the definition of transpose and then start commuting/fusing the map length and map (replicate ()) with things until they "cancel out" and there are no unit values left anywhere in the computation.

@jer_gib@functional.cafe More concretely, what's the nicest way you know of to define transpose? The actual implementation in the Haskell standard library is gross. The best I've come up with is

transpose = foldr (zipWithExt (++) . map pure) []

where zipWithExt :: (a -> a -> a) -> [a] -> [a] -> [a] is the analogue of zipWith which extends to the longer of its two list arguments instead of truncating to the shorter.