Shifting functors: Alternative for numerical towers?
I've been longing for a functional programming language that'd double as a computer algebra system. One of the problems has been that numerical types in these languages do not compose very well.
People usually build up some sort of a numerical tower. You get integers, then real numbers from integers, then complex numbers.. However, if something is missing in this tower then you won't have it. Or alternatively you have it, but you don't have something else.
What if we could build structures that do compose well? What kind of properties would they have? I think they'd be functors.
Now in case I write something silly here, this is the first time I'm doing something with category theory. I just watched halfway through Bartosz Milewski's category theory lectures (There are also second and third part of these lectures).
Also this is not something that could be just picked up and used. The question mark in the title is for that reason.
Functor is a transform from types and functions that preserves composition.
F (g.f) = F g . F f
F id = id
So if we'd have a cartesian category with a carrier number object and some functions for those numbers:
zero : 1 -> n
succ : n -> n
neg : n -> n
add : (n * n) -> n
mul : (n * n) -> n
A functor from this category would preserve the composition of these functions.
Eg, for every morphism
g in our category we'd have:
F (g . add) = F g . F add
F (add . f) = F add . F f
What does this mean for addition? It means that if we add in the target category, it behaves the same as in the category that we started from.
In this case if we do
(g . add . (zero * succ))
it must be similar as if we did
F g . F add . (F zero * F succ).
We should have a functor to every base numerical value that we want to use. Eg. We'd have:
zero :: Num a => () -> a
succ :: Num a => a -> a
neg :: Num a => a -> a
add :: Num a => (a, a) -> a
mul :: Num a => (a, a) -> a
Note that we aren't writing an endofunctor, the source category is outside of the type/function category of Haskell.
Next we should have a functor to structures that we want to use. For example if we had polynomials we'd then have:
zero :: () -> Poly a
succ :: Poly a -> Poly a
neg :: Poly a -> Poly a
add :: (Poly a, Poly a) -> Poly a
mul :: (Poly a, Poly a) -> Poly a
For complex numbers we'd have:
zero :: () -> Complex a
succ :: Complex a -> Complex a
neg :: Complex a -> Complex a
add :: (Complex a, Complex a) -> Complex a
mul :: (Complex a, Complex a) -> Complex a
Next we'd have a natural transformation from
Poly a and to
Eg. This means that things must stay same if we transform from
Poly a at anywhere in our computation.
alpha :: a -> Poly a
alpha.zero = zero.alpha
alpha.succ = succ.alpha
alpha.neg = neg.alpha
alpha.add = add.alpha
alpha.mul = mul.alpha
alpha.(f,g) = (f,g).alpha
alpha.fst = fst.alpha
alpha.snd = snd.alpha
Next we additionally want to have a natural isomorphism between the structure types we use:
beta :: (Poly . Complex) a -> (Complex . Poly) a
delta :: (Complex . Poly) a -> (Poly . Complex) a
Or more generally:
beta' :: ShiftingFunctor f => (f . Poly) a -> (Poly . f) a
delta' :: ShiftingFunctor f => (f . Complex) a -> (Complex . f) a
So we should be able to shift around the representation or refactorize the expression such that all these operations stay composible.
If we were able to build a structure that can satisfy all these rules. We could build types that can compose to build larger arithmetic structures without needing to consider other possible structures when declaring such new structures.
Though this whole problem isn't as interesting as it used to be. It would seem that geometric algebra unifies enough structures to make it quite convenient to work with arithmetic structures anyway. Also things such as polynomials and automatic differentation would seem to partially fall out of the functional programming itself.
Polynomials and complex numbers
Finally here's some sketch structures to operate with polynomials and complex numbers in Haskell. They shouldn't be that interesting themselves because I don't have a way to check that they form shifting functors.
type Poly a = [a]
class Arith a where
zero :: a
is_zero :: a -> Bool
neg :: a -> a
add :: a -> a -> a
mul :: a -> a -> a
instance Arith Int where
zero = 0
is_zero = (==0)
neg a = -a
add = (+)
mul = (*)
lift :: a -> Poly a
lift a = [a]
norm :: Arith a => Poly a -> Poly a
norm  = 
norm (x:xs) = case x : norm xs of
[a] -> if is_zero a then  else [a]
ys -> ys
The substitution should be a bit different here.
subs :: Num a => Poly a -> a -> a
subs poly x = f poly x 0
where f (c:xs) x n = c*(x^n) + f xs x (n+1)
f  _ _ = 0
instance Arith a => Arith (Poly a) where
zero = 
is_zero = all is_zero
neg xs = fmap neg xs
add   = 
add xs  = xs
add  ys = ys
add (x:xs) (y:ys) = add x y : add xs ys
mul xs = norm . foldl add  . fmap f . indexed
where f (n,c) = replicate n zero ++ fmap (mul c) xs
indexed :: [a] -> [(Int,a)]
indexed = f 0
where f n (x:xs) = (n,x) : f (n+1) xs
f n  = 
x :: Num a => Poly a
x = [0,1]
polymap :: (a -> b) -> Poly a -> Poly b
polymap f xs = fmap f xs
merge :: (Num a, Num b) => Poly a -> Poly b -> Poly (a,b)
merge   = 
merge (x:xs)  = (x,0) : merge xs 
merge  (y:ys) = (0,y) : merge  ys
merge (x:xs) (y:ys) = (x,y) : merge xs ys
type Complex a = (a,a)
lift' :: Num a => a -> Complex a
lift' a = (a,0)
i :: Num a => Complex a
i = (0,1)
real :: Complex a -> a
real (a,_) = a
imag :: Complex a -> a
imag (_,a) = a
instance Arith a => Arith (Complex a) where
zero = (zero, zero)
is_zero (x,y) = is_zero x && is_zero y
neg (x,y) = (neg x, neg y)
add (a,b) (c,d) = (add a c, add b d)
mul (a,b) (c,d) = (add (mul a c) (neg (mul b d)), add (mul a d) (mul b c))
complexmap :: (a -> b) -> Complex a -> Complex b
complexmap f (x,y) = (f x, f y)
Conversions between structures:
beta :: Poly (Complex a) -> Complex (Poly a)
beta poly = (polymap real poly, polymap imag poly)
delta :: Num a => Complex (Poly a) -> Poly (Complex a)
delta (r,v) = merge r v
Note that the
merge for each type should be enough
to build up a system where the structure can be freely permuted.
The problem is in verifying somehow
that the conversion forms a natural isomorphism between permutations.
There might be some simple rules that allow such structures to be constructed and work together without needing to but I'm likely not going to explore deeper into it yet.
I'll watch the remaining videos and then get back to looking at the wordprocessing format again. I still may need to write few filler blogposts before getting to it though.