Implementing complex numbers and FFT with just datatypes (2023)

Summary

Implementing complex numbers and FFT with just datatypes (no floats) In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats. Why implement numbers with ADTs? For most programmers, "real numbers" are a given: they just use floats and call it a day. But, in some cases, it doesn't work well, and I'm not talking about precision issues. When trying to prove statements on real numbers in proof assistants like Coq, we can't use doubles, we must formalize reals using datatypes, which can be very hard. For me, the real issue arises when I'm trying to implement optimal algorithms on HVM. To do that, I need functions to fuse, which is a fancy way of saying that (+ 2) . (+ 2) "morphs into" (+ 4) during execution - yet, machine floats block that mechanism. Because of that, I've been trying to come up with an elegant way to implement numbers with just datatypes. For natural numbers, it is easy: we can just implement them as bitstrings: -- O stands for bit 0 -- I stands for bit 1 -- E stands for end-of-string data Nat = O Nat | I Nat | E deriving (Show) -- Applies 'f' n times to 'x'. rep :: Nat -> (a -> a) -> a -> a rep (O x) f = rep x (\x -> f (f x)) rep (I x) f = rep x (\x -> f (f x)) . f rep E f = id -- Increments a Nat. inc :: Nat -> Nat inc E = O E inc (O x) = I x inc (I x) = O (inc x) -- Adds two Nats. add :: Nat -> Nat -> Nat add a = rep a inc main :: IO () main = do let a = I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I (I E))))))))))))))))))))))))) let b = O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O (O E)))))))))))))...