The Haskell Unfolder Episode 27: duality
ฝัง
- เผยแพร่เมื่อ 21 ก.ย. 2024
- "Duality" is the idea that two concepts are "similar but opposite" in some precise sense. The discovery of a duality enables us to use our understanding of one concept to help us understand the dual concept, and vice versa. It is a powerful technique in many disciplines, including computer science. In this episode of the Haskell Unfolder we discuss how we can use duality in a very practical way, as a guiding principle leading to better library interfaces and a tool to find bugs in our code.
This episode focuses on design philosophy rather than advanced Haskell concepts, and should consequently be of interest to beginners and advanced Haskell programmers alike (we will not use any Haskell beyond Haskell 2010). Indeed, the concepts apply in other languages also (but we will assume familiarity with Haskell syntax).
Further reading:
* Wikipedia has a list of dualities across many disciplines:
en.wikipedia.o...
* Dagstuhl seminar 13311 was dedicated to the study of (more precise) dualities in computer science.
www.dagstuhl.d...
References for the examples of duality shown in the introduction:
1. en.wikipedia.o...
Yin Yang symbol
Attribution: Klem - This vector image was created with Inkscape by Klem,
and then manually edited by Mnmazur.
2. en.wikipedia.o...
Photo of a page from the Yijing
Attribution: Franklin Perkins in "Leibniz and China: A Commerce of Light"
3. iep.utm.edu/du...
Duality in logic.
Attribution: Lorenz Demey and Hans Smessaert
4. onlinelibrary....
Duality in electronic circuit design.
Attribution: David F. Peelo. "Current Interruption Transients Calculation"
(appendix B: Principle of Duality)
5. en.wikipedia.o...
Dual graphs in mathematics.
Attribution: wikipedia.
6. • But what is the Fourie...
"Almost-fourier transform".
Attribution: 3Blue1Brown (Grant Sanderson): "But what is the Fourier
Transform? A visual introduction"
7. • The Haskell Unfolder E...
Duality of `fold` and `unfold` in Haskell.
Attribution: The Haskell Unfolder Episode 24: generic (un)folds
I love how you can mechanically reason about the other half of the implementation and it just makes sense in the end
Yes! So satisfying :)
Thank you so much. This is really interesting topic! Esp Yin & Yang (!; ;)
Great video on a very interesting topic! I liked that you start by showing that duality is used on other scientific and engineering disciplines and then proceed to discuss how it can inform the Haskell implementations. This is really drives the point that it is not just an elegant theoretical observation but rather a useful tool for problem solving.
I have a single question regarding the first example of compression and decompression: in the final solution there is still some asymmetry between the two functions because decompression may fail with an error. Any thoughts on why this is?
I guess it's the asymmetry between encoding and decoding.
Whereas you can probably encode any ByteString, it's unlikely that any random ByteString represents valid encoding of some data.
This is a similar situation to when you encode Int to String, so you have total function `Int -> String`,
but not every string can be decoded into Int, so `String -> Int` would be partial function.
@@JackSchpeck Yes, I think I agree with this reply. Perhaps if one could make the types more precise, one could prevent the error condition and make the symmetry even more complete.
Yeah, I've been wondering about this as well. @JackSchpeck 's reply is true of course, but it feels like we might be able to express that fact (decompression can fail, compression cannot) a bit more formally to make that duality more clear. Not totally obvious to me right now how though. If anyone has any suggestions, I'd love to hear them :)
Is it possible to automatically infer dual types?
I'm not sure what exactly you mean. There's some design flexibility in what one wants "dual" to mean in a particular setting. There are generally multiple concepts / instances of concepts involved, and only some of them have to be flipped. If the rules are sufficiently clear in a particular scenario, then one can implement a type family that computes the dual type from a given type. There are some instances where this is being done, e.g. in various experiments of encoding session types in Haskell.