Kind for dimensions

[dwincort]

I notice for dimensions, you use Either and (). This is fine, but it seems like it might be a little cleaner if you used a custom kind. For instance, consider if you added:

data Dim = One | Plus Dim Dim

type family CountDim (d :: Dim) :: Nat where
  CountDim One = 1
  CountDim (Plus x y) = CountDim x + CountDim y

and then defined Matrix as:

data Matrix e (cols :: Dim) (rows :: Dim) where
  Singleton :: e -> Matrix e One One
  Join :: Matrix e a rows -> Matrix e b rows -> Matrix e (Plus a b) rows
  Fork :: Matrix e cols a -> Matrix e cols b -> Matrix e cols (Plus a b)

There are a few other changes you'd have to make (like in FromNat and Normalize), but one benefit is that it would keep you honest and clear in your type families. That is, there would be a clear distinction between Nat, Type, and Dim rather than having Type and Dim muddied together.

[bolt12]

Thank you for the suggestion! I remember trying something like this but ended up giving up on the idea, dont remember why! I'll give it another try!