-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Count type family #14
Comments
@ilyakooo0 Thanks for opening this issue! Indeed I found that we cannot guarantee that the The typeclass idea is nice but we still need some way of normalizing a data type to a tree of |
I'm not sure I understand the exact situation you are talking about. The 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 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 |
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 😄 |
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 ( 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. |
@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! |
@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 |
Did you push this branch? It's not immediately obvious to me why a |
@ilyakooo0 oh my bad! I renamed your class Dimension t (cardinality :: Nat) | t -> cardinality where
toDim :: t -> FromNat cardinality
fromDim :: FromNat cardinality -> t |
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 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 The instance for toDim = bar . foo |
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')) |
I'm having trouble even with your suggestion, I don't think it is possible to go via this type class :/ |
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 |
And I just realized that |
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 () = () |
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 |
Awesome! I will try and also test this out 😄 I'll report back with any findings! |
Where are these types used? Count (M1 _ _ f p) = Count (f p)
Count (K1 _ _ _) = 1
Count (V1 _) = 0
Count (U1 _) = 1
Count ((:*:) a b p) = Count (a p) * Count (b p)
Count ((:+:) a b p) = Count (a p) + Count (b p)
Count d = Count (Rep d R) |
And the function type Count (a -> b) = (^) (Count b) (Count a) |
We can't easily make functions an instance of |
The generic representations are used when using the Matrix.Type module. They are not directly used in Matrix dimensions but are indirectly used by types that implement the
This is not used, I just added the function type because it could be useful to model matrix dimensions with function types but I never encountered an use case for it. I think we can ditch it. |
It seems like the functionality of some functions like
fromF
depends on the fact that theGeneric
representation of a type is equivalent to its'Bounded
/Enum
representation (through theCount
type family), which in general can be not true.There isn't really a good way of representing the link between
Bounded
/Enum
andCount
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
orBounded
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 baseCount 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 theEither
/()
representation.This would allow us to completely remove the implicit requirement between the
Generic
andEnum
/Bounded
instances. (Although it would still be used in a default implementation of the typeclass, but the connection can be made explicit by making anewtype
, which can be used to derive the the typeclass:deriving MatIndex via MatBoundedIndex
).This would remove the "hacky" part of
fromF
which uses theEnum
andBounded
instances explicitly.The text was updated successfully, but these errors were encountered: