Count type family

[ilyakooo0]

It seems like the functionality of some functions like fromF depends on the fact that the Generic representation of a type is equivalent to its' Bounded/Enum representation (through the Count type family), which in general can be not true.

There isn't really a good way of representing the link between Bounded/Enum and Count in haskell.

The problem I have with this is that it is not explicitly mentioned anywhere in the documentation and can break things in unexpected ways. (If a type has a custom Enum or Bounded instance for some reason)

I think it can be beneficial to expose the ability to define a custom Count instance for arbitrary types to the user.

An approach can be to make Count an open type family. This would most likely require us to remove the base Count d = Count (Rep d R) case, making the user explicitly define an instance of the type family for every type he wants to use as the matrix index.
We could also expose some GenericCount, which would make implementing the removed base case for custom types easier and more idiomatic.

Another thought I have it to make the Count type family not a type family at all and make it a functional dependency in a typeclass, which encapsulates the conversion between the custom type and the Either/() representation.

class MatIndex t (i :: Nat) | t -> i where
  toIndex :: t -> FromNat i
  fromIndex :: FromNat i -> t

This would allow us to completely remove the implicit requirement between the Generic and Enum/Bounded instances. (Although it would still be used in a default implementation of the typeclass, but the connection can be made explicit by making a newtype, which can be used to derive the the typeclass: deriving MatIndex via MatBoundedIndex).

This would remove the "hacky" part of fromF which uses the Enum and Bounded instances explicitly.

[bolt12]

@ilyakooo0 Thanks for opening this issue!

Indeed I found that we cannot guarantee that the Enum/Bounded will be "correct" for some custom type. I find your open type family suggestion interesting but I don't think it justifies changing that yet! I do not know if that would be a common enough use case, for example.

The typeclass idea is nice but we still need some way of normalizing a data type to a tree of Eithers and () at the type-level. What are your thoughts on this?

[ilyakooo0]

The typeclass idea is nice but we still need some way of normalizing a data type to a tree of Eithers and () at the type-level. What are your thoughts on this?

I'm not sure I understand the exact situation you are talking about.

The MatIndex typeclass would already work with normalized datatypes (since FromNat already returns a normalized type).

Normalizing at the type level would be equivalent to:

(MatIndex t i, normalized ~ FromNat i)

(There might be a nicer way of representing this.)

I did not test this thoroughlly, but it seems like the (><) type would change as follows:

class KnowNat i => MatIndex t (i :: Nat) | t -> i where
  toIndex :: t -> FromNat i
  fromIndex :: FromNat i -> t

(><) ::
     forall e m p n q.
     ( Num e,
       CountableDims m n,
       CountableDims p q,
       CountableDimsN (m, n) (p, q),
       FL (Normalize (m, n)) m,
       FL (Normalize (m, n)) n,
       FL (Normalize (p, q)) p,
       FL (Normalize (p, q)) q
     )
     => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))

(><) ::
     forall e m p n q.
     ( Num e,
       MatIndex m mi,
       MatIndex n ni,
       MatIndex p pi,
       MatIndex q qi,
       MatIndex (m, n) mni,
       FL (FromNat mni) m,
       FL (FromNat mni) n,
       MatIndex (p, q) pqi,
       FL (FromNat pqi) p,
       FL (FromNat pqi) q

     )
     => Matrix e m p -> Matrix e n q -> Matrix e (Normalize (m, n)) (Normalize (p, q))

On a side note: it seems like the (a, b) and Either a b cases are not necessary in the Counttype family since they would be caught by the Generic cases.

[bolt12]

I understand now! I'd be more than happy to review a PR that refactored the code and added this functionality. Let's see how it turns out 😄

[ilyakooo0]

Although, I think I was operating under the assumption that

Normalize x ~ FromNat (Count x))

, which is not true strictly speaking.

The "normalization" I am proposing would be more strict (I think). As in, it would have strictly less possible values. (Since it maps the dimension (Count) into a single Either/() representation, while Normalize can return multiple valid types with the same Count (I think).)

In any case, I think making "normalization" more strict would not be an issue and things should work if we implement it across the whole project.

[bolt12]

@ilyakooo0 Yes I agree, I think it just isn't as strict as I'd want it to be because I don't know of any way to tell GHC that it can be. I think your idea might be a nice workaround!

[bolt12]

@ilyakooo0 I gave this a try but got stuck in something that I think should be trivial:

instance (Dimension a ca, Dimension b cb, cc ~ (ca + cb)) => Dimension (Either a b) cc where
  toDim (Left a) = _
  toDim (Right b) = _
  fromDim (Left a) = _
  fromDim (Right b) = _

This needs the restriction that FromNat cc ~ Either (FromNat ca) (FromNat cb) which is not always true... can you think about a simple workaround?

[ilyakooo0]

Did you push this branch? It's not immediately obvious to me why a Dimension typeclass is necessary and what it is.

[bolt12]

@ilyakooo0 oh my bad! I renamed your MatIndex to Dimension, so

class Dimension t (cardinality :: Nat) | t -> cardinality where
  toDim :: t -> FromNat cardinality
  fromDim :: FromNat cardinality -> t

[ilyakooo0]

To be honest, I don't remember the whole picture I had in my head when I opened this issue. I'm now trying to untangle it myself.

instance (Dimension a ca, Dimension b cb, cc ~ (ca + cb)) => Dimension (Either a b) cc where

The problem with this instance declaration is that it assumes that the Either a b is already normalized (since we assume the cardinality of Left and Right cases will not change during normalization (we assume we will need the Dimension a ca and Dimension b cb instances)).

---

A naive way would be to implement two separate operations:

foo :: Either lhs rhs -> Natural 1 (Count (Either lhs rhs))
bar :: Natural 1 n -> FromNat n

(I probably have off-by-one errors somewhere in there)

the bar is the toDim instance for Natural (or something close to it).

The instance for Either would have something close to

toDim = bar . foo

[ilyakooo0]

I was trying to implement indexing a while back and this might be relevant:

class NatIndex dir max | dir -> max where
  natIndex :: Natural 0 max -> dir

instance NatIndex () 0 where
  natIndex _ = ()

instance
  (NatIndex lhs lhs', NatIndex rhs rhs', (lhs' + rhs' + 1) ~ max, KnownNat lhs')
  => NatIndex (Either lhs rhs) max where
  natIndex (Nat n) = if n <= maxLhs
    then Left $ natIndex @lhs @lhs' (Nat n)
    else Right $ natIndex @rhs @rhs' (Nat $ n - maxLhs - 1)
    where maxLhs = fromIntegral (natVal (Proxy @lhs'))

[bolt12]

I'm having trouble even with your suggestion, I don't think it is possible to go via this type class :/

[ilyakooo0]

Admittedly this is slightly ugly, but this works (compiles).

injectNat :: (c <= a, b <= d) => Natural a b -> Natural c d
injectNat = coerce

addNat :: Natural a b -> Natural c d -> Natural (a + c) (b + d)
addNat (Nat a) (Nat b) = Nat $ a + b

class NatIndex dir max | dir -> max where
  fromNatIndex :: Natural 0 max -> dir
  toNatIndex :: dir -> Natural 0 max

instance NatIndex () 0 where
  fromNatIndex _ = ()
  toNatIndex () = nat 0

instance
  (NatIndex lhs lhs', NatIndex rhs rhs', (lhs' + rhs' + 1) ~ max, lhs' <= max, rhs' <= max, KnownNat lhs')
  => NatIndex (Either lhs rhs) max where
  fromNatIndex (Nat n) = if n <= maxLhs
    then Left $ fromNatIndex @lhs @lhs' (Nat n)
    else Right $ fromNatIndex @rhs @rhs' (Nat $ n - maxLhs - 1)
    where maxLhs = fromIntegral (natVal (Proxy @lhs'))
  toNatIndex (Left lhs) = injectNat $ toNatIndex lhs
  toNatIndex (Right rhs) = maxLhs `addNat` toNatIndex rhs `addNat` oneNat
    where
      oneNat :: Natural 0 1
      oneNat = Nat 1
      maxLhs :: Natural 0 lhs'
      maxLhs = Nat $ fromIntegral (natVal (Proxy @lhs'))

class Dimension t (i :: Nat) | t -> i where
  toDim :: t -> FromNat i
  fromDim :: FromNat i -> t

instance (NatIndex (FromNat m) m) => Dimension (Natural 0 m) m where
  toDim = fromNatIndex
  fromDim = toNatIndex

instance (NatIndex (Either lhs rhs) i, NatIndex (FromNat i) i)
  => Dimension (Either lhs rhs) i where
  toDim = fromNatIndex . toNatIndex
  fromDim = fromNatIndex . toNatIndex

[ilyakooo0]

And I just realized that FromNat is indexed from 1, not 0 (but my NatIndex is index from 0)

[ilyakooo0]

This should be fine (didn't test it yet)

class NatIndex dir max | dir -> max where
  fromNatIndex :: Natural 1 max -> dir
  toNatIndex :: dir -> Natural 1 max

instance NatIndex () 1 where
  fromNatIndex _ = ()
  toNatIndex () = nat 1

instance
  (NatIndex lhs lhs', NatIndex rhs rhs', (lhs' + rhs') ~ max, lhs' <= max, rhs' <= max, KnownNat lhs')
  => NatIndex (Either lhs rhs) max where
  fromNatIndex (Nat n) = if n <= maxLhs
    then Left $ fromNatIndex @lhs @lhs' (Nat n)
    else Right $ fromNatIndex @rhs @rhs' (Nat $ n - maxLhs)
    where maxLhs = fromIntegral (natVal (Proxy @lhs'))
  toNatIndex (Left lhs) = injectNat $ toNatIndex lhs
  toNatIndex (Right rhs) = maxLhs `addNat` toNatIndex rhs
    where
      maxLhs :: Natural 0 lhs'
      maxLhs = Nat $ fromIntegral (natVal (Proxy @lhs'))

class Dimension t (i :: Nat) | t -> i where
  toDim :: t -> FromNat i
  fromDim :: FromNat i -> t

instance (NatIndex (FromNat m) m) => Dimension (Natural 1 m) m where
  toDim = fromNatIndex
  fromDim = toNatIndex

instance (NatIndex (Either lhs rhs) i, NatIndex (FromNat i) i)
  => Dimension (Either lhs rhs) i where
  toDim = fromNatIndex . toNatIndex
  fromDim = fromNatIndex . toNatIndex

instance Dimension () 1 where
  toDim () = ()
  fromDim () = ()

[ilyakooo0]

And it currently use the Count type family

I’m currently trying to think if it is even practical to make the type class return normalized Eithers. I have a feeling it might be better to have it return Natural an get a normalized Either after the fact