You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
> (reifyVectorNat (Data.Vector.fromList [2, 3, 4]) $ reifyVectorNat (Data.Vector.fromList [5, 6, 7]) $ \(v1 :: V (n :: Nat) Int) (v2 :: V (m :: Nat) Int) ->case sameNat (Proxy :: Proxy n) (Proxy :: Proxy m) of Just Refl -> Linear.Metric.dot v1 v2) :: Int
56
My implementation uses GHC.TypeNats but maybe it would be better to use peano numbers. It would mean that plusCancellative and plusNat could be removed. My implementation also incurs a dependency on constraints package, but the relevant parts could be inlined
The text was updated successfully, but these errors were encountered:
I'm a bit surprised to not see a structure like the following in the package:
Compared to
Linear.V
, this allows us to write:> Linear.Metric.dot (2 :. 3 :. 4 :. LNil) (5 :. 6 :. 7 :. LNil) 56
instead of:
My implementation uses
GHC.TypeNats
but maybe it would be better to use peano numbers. It would mean thatplusCancellative
andplusNat
could be removed. My implementation also incurs a dependency onconstraints
package, but the relevant parts could be inlinedThe text was updated successfully, but these errors were encountered: