{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}  -- TEMP

-- | Vector spaces as zippable functors

module ConCat.Free.VectorSpace where

import Prelude hiding (zipWith)
import Data.Monoid (Sum(..),Product(..))
import Data.Semigroup (Semigroup(..))
-- import GHC.Exts (Coercible,coerce)
import GHC.Generics (U1(..),Par1(..),(:*:)(..),(:+:)(..),(:.:)(..))
#ifdef VectorSized
import GHC.TypeLits (KnownNat)
#endif

import Data.Foldable (fold)
import Data.Pointed
import Data.Key (Zip(..))
-- import Data.Vector.Sized (Vector)
-- import Data.Map (Map)
import Data.Constraint ((:-)(..),Dict(..))
import Data.Vector.Sized (Vector)

-- import Control.Newtype.Generics

import ConCat.Orphans ()
import ConCat.Misc ((:*),(:+),(<~),sqr)
import ConCat.Rep
-- import ConCat.Category (UT(..),Constrained(..),FunctorC(..))
import ConCat.AltCat (OpCon(..),Sat,type (|-)(..),fmapC)

{--------------------------------------------------------------------
    Vector spaces
--------------------------------------------------------------------}

infixl 7 *^, <.>, >.<
infixl 6 ^+^, ^-^

#if 1
type Zeroable = Pointed

-- Zero vector
zeroV :: (Pointed f, Num a) => f a
zeroV :: forall (f :: * -> *) a. (Pointed f, Num a) => f a
zeroV = a -> f a
forall a. a -> f a
forall (p :: * -> *) a. Pointed p => a -> p a
point a
0

-- TODO: Maybe use tabulate . const instead of point

#else

-- Experimental alternative to Pointed
class Functor f => Zeroable f where
  zeroV :: Num a => f a
  default zeroV :: (Pointed f, Num a) => f a
  zeroV = point 0

-- The Functor superclass is just for convenience.
-- Remove if needed (and fix other signatures).

instance Zeroable U1 where
  -- zeroV = U1
  -- {-# INLINE zeroV #-}

-- The following instance could be defaulted. I'm tracking down what might be an
-- inlining failure.

instance Zeroable Par1 where
  zeroV = Par1 0
  {-# INLINE zeroV #-}

instance Zeroable ((->) k)

instance Ord k => Zeroable (Map k) where
  zeroV = mempty
  {-# INLINE zeroV #-}

instance (Zeroable f, Zeroable g) => Zeroable (f :*: g) where
  zeroV = zeroV :*: zeroV
  {-# INLINE zeroV #-}

instance (Zeroable f, Zeroable g) => Zeroable (g :.: f) where
  zeroV = Comp1 (const zeroV <$> (zeroV :: g Int))
  {-# INLINE zeroV #-}

#endif

-- TODO: Replace Num constraints with Ring or SemiRing

-- | Scale a vector
scaleV, (*^) :: (Functor f, Num s) => s -> f s -> f s
s
s *^ :: forall (f :: * -> *) s. (Functor f, Num s) => s -> f s -> f s
*^ f s
v = (s
s s -> s -> s
forall a. Num a => a -> a -> a
*) (s -> s) -> f s -> f s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f s
v
scaleV :: forall (f :: * -> *) s. (Functor f, Num s) => s -> f s -> f s
scaleV = s -> f s -> f s
forall (f :: * -> *) s. (Functor f, Num s) => s -> f s -> f s
(*^)
{-# INLINE (*^) #-}
{-# INLINE scaleV #-}

-- | Negate a vector
negateV :: (Functor f, Num s) => f s -> f s
negateV :: forall (f :: * -> *) s. (Functor f, Num s) => f s -> f s
negateV = ((-s
1) s -> f s -> f s
forall (f :: * -> *) s. (Functor f, Num s) => s -> f s -> f s
*^)
{-# INLINE negateV #-}

-- | Add vectors
addV, (^+^) :: (Zip f, Num s) => f s -> f s -> f s
^+^ :: forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
(^+^) = (s -> s -> s) -> f s -> f s -> f s
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith s -> s -> s
forall a. Num a => a -> a -> a
(+)
addV :: forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
addV = f s -> f s -> f s
forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
(^+^)
{-# INLINE (^+^) #-}
{-# INLINE addV #-}

-- | Subtract vectors
subV, (^-^) :: (Zip f, Num s) => f s -> f s -> f s
^-^ :: forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
(^-^) = (s -> s -> s) -> f s -> f s -> f s
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (-)
subV :: forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
subV = f s -> f s -> f s
forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
(^-^)
{-# INLINE (^-^) #-}
{-# INLINE subV #-}

-- | Inner product
dotV, (<.>) :: forall s f. (Zip f, Foldable f, Num s) => f s -> f s -> s
f s
x <.> :: forall s (f :: * -> *).
(Zip f, Foldable f, Num s) =>
f s -> f s -> s
<.> f s
y = f s -> s
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((s -> s -> s) -> f s -> f s -> f s
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith s -> s -> s
forall a. Num a => a -> a -> a
(*) f s
x f s
y)
dotV :: forall s (f :: * -> *).
(Zip f, Foldable f, Num s) =>
f s -> f s -> s
dotV = f s -> f s -> s
forall s (f :: * -> *).
(Zip f, Foldable f, Num s) =>
f s -> f s -> s
(<.>)
{-# INLINE (<.>) #-}
{-# INLINE dotV #-}

-- | Norm squared
#if 1
normSqr :: forall s f. (Functor f, Foldable f, Num s) => f s -> s
normSqr :: forall s (f :: * -> *). (Functor f, Foldable f, Num s) => f s -> s
normSqr = f s -> s
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (f s -> s) -> (f s -> f s) -> f s -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> s) -> f s -> f s
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s -> s
forall a. Num a => a -> a
sqr
#else
normSqr :: forall s f. (Zip f, Foldable f, Num s) => f s -> s
normSqr u = u <.> u
#endif
{-# INLINE normSqr #-}

-- | Distance squared
distSqr :: forall s f. (Zip f, Foldable f, Num s) => f s -> f s -> s
distSqr :: forall s (f :: * -> *).
(Zip f, Foldable f, Num s) =>
f s -> f s -> s
distSqr f s
u f s
v = f s -> s
forall s (f :: * -> *). (Functor f, Foldable f, Num s) => f s -> s
normSqr (f s
u f s -> f s -> f s
forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
^-^ f s
v)
{-# INLINE distSqr #-}

-- | Outer product
outerV, (>.<) :: (Num s, Functor f, Functor g) => g s -> f s -> g (f s)
g s
x >.< :: forall s (f :: * -> *) (g :: * -> *).
(Num s, Functor f, Functor g) =>
g s -> f s -> g (f s)
>.< f s
y = (s -> f s -> f s
forall (f :: * -> *) s. (Functor f, Num s) => s -> f s -> f s
*^ f s
y) (s -> f s) -> g s -> g (f s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g s
x
outerV :: forall s (f :: * -> *) (g :: * -> *).
(Num s, Functor f, Functor g) =>
g s -> f s -> g (f s)
outerV = g s -> f s -> g (f s)
forall s (f :: * -> *) (g :: * -> *).
(Num s, Functor f, Functor g) =>
g s -> f s -> g (f s)
(>.<)
{-# INLINE (>.<) #-}
{-# INLINE outerV #-}

-- | Normalize a vector (scale to unit magnitude)
normalizeV :: (Functor f, Foldable f, Floating a) => f a -> f a
normalizeV :: forall (f :: * -> *) a.
(Functor f, Foldable f, Floating a) =>
f a -> f a
normalizeV f a
xs = (a -> a -> a
forall a. Fractional a => a -> a -> a
/ f a -> a
forall a. Num a => f a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum f a
xs) (a -> a) -> f a -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
xs
{-# INLINE normalizeV #-}

-- Would I rather prefer swapping the arguments (equivalently, transposing the
-- result)?

-- newtype SumV f a = SumV (f a)
data SumV f a = SumV (f a)

instance HasRep (SumV f a) where
  type Rep (SumV f a) = f a
  abst :: Rep (SumV f a) -> SumV f a
abst Rep (SumV f a)
as = f a -> SumV f a
forall (f :: * -> *) a. f a -> SumV f a
SumV f a
Rep (SumV f a)
as
  repr :: SumV f a -> Rep (SumV f a)
repr (SumV f a
as) = f a
Rep (SumV f a)
as
  {-# INLINE abst #-}
  {-# INLINE repr #-}

instance (Zeroable f, Zip f, Num a) => Semigroup (SumV f a) where
  <> :: SumV f a -> SumV f a -> SumV f a
(<>) = (Rep (SumV f a) -> Rep (SumV f a) -> Rep (SumV f a))
-> SumV f a -> SumV f a -> SumV f a
forall p q r.
(HasRep p, HasRep q, HasRep r) =>
(Rep p -> Rep q -> Rep r) -> p -> q -> r
inAbst2 f a -> f a -> f a
Rep (SumV f a) -> Rep (SumV f a) -> Rep (SumV f a)
forall (f :: * -> *) s. (Zip f, Num s) => f s -> f s -> f s
(^+^)

instance (Zeroable f, Zip f, Num a) => Monoid (SumV f a) where
  mempty :: SumV f a
mempty = Rep (SumV f a) -> SumV f a
forall a. HasRep a => Rep a -> a
abst f a
Rep (SumV f a)
forall (f :: * -> *) a. (Pointed f, Num a) => f a
zeroV
  mappend :: SumV f a -> SumV f a -> SumV f a
mappend = SumV f a -> SumV f a -> SumV f a
forall a. Semigroup a => a -> a -> a
(<>)

sumV :: (Functor m, Foldable m, Zeroable n, Zip n, Num a) => m (n a) -> n a
sumV :: forall (m :: * -> *) (n :: * -> *) a.
(Functor m, Foldable m, Zeroable n, Zip n, Num a) =>
m (n a) -> n a
sumV = SumV n a -> n a
SumV n a -> Rep (SumV n a)
forall a. HasRep a => a -> Rep a
repr (SumV n a -> n a) -> (m (n a) -> SumV n a) -> m (n a) -> n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (SumV n a) -> SumV n a
forall m. Monoid m => m m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (m (SumV n a) -> SumV n a)
-> (m (n a) -> m (SumV n a)) -> m (n a) -> SumV n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n a -> SumV n a) -> m (n a) -> m (SumV n a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n a -> SumV n a
forall (f :: * -> *) a. f a -> SumV f a
SumV
{-# INLINE sumV #-}

{--------------------------------------------------------------------
    Conversion
--------------------------------------------------------------------}

type RepHasV s a = (HasRep a, HasV s (Rep a), V s a ~ V s (Rep a))

class HasV s a where
  type V s a :: * -> *
  toV :: a -> V s a s
  unV :: V s a s -> a
  -- Default via Rep.
  type V s a = V s (Rep a)
  default toV :: RepHasV s a => a -> V s a s
  default unV :: RepHasV s a => V s a s -> a
  toV = Rep a -> V s (Rep a) s
forall s a. HasV s a => a -> V s a s
toV (Rep a -> V s (Rep a) s) -> (a -> Rep a) -> a -> V s (Rep a) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a
forall a. HasRep a => a -> Rep a
repr
  unV = Rep a -> a
forall a. HasRep a => Rep a -> a
abst (Rep a -> a) -> (V s (Rep a) s -> Rep a) -> V s (Rep a) s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. V s (Rep a) s -> Rep a
forall s a. HasV s a => V s a s -> a
unV
  {-# INLINE toV #-} ; {-# INLINE unV #-}

inV :: forall s a b. (HasV s a, HasV s b) => (a -> b) -> (V s a s -> V s b s)
inV :: forall s a b.
(HasV s a, HasV s b) =>
(a -> b) -> V s a s -> V s b s
inV = b -> V s b s
forall s a. HasV s a => a -> V s a s
toV (b -> V s b s) -> (V s a s -> a) -> (a -> b) -> V s a s -> V s b s
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ V s a s -> a
forall s a. HasV s a => V s a s -> a
unV

onV :: forall s a b. (HasV s a, HasV s b) => (V s a s -> V s b s) -> (a -> b)
onV :: forall s a b.
(HasV s a, HasV s b) =>
(V s a s -> V s b s) -> a -> b
onV = V s b s -> b
forall s a. HasV s a => V s a s -> a
unV (V s b s -> b) -> (a -> V s a s) -> (V s a s -> V s b s) -> a -> b
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ a -> V s a s
forall s a. HasV s a => a -> V s a s
toV

onV2 :: forall s a b c. (HasV s a, HasV s b, HasV s c) => (V s a s -> V s b s -> V s c s) -> (a -> b -> c)
onV2 :: forall s a b c.
(HasV s a, HasV s b, HasV s c) =>
(V s a s -> V s b s -> V s c s) -> a -> b -> c
onV2 = (V s b s -> V s c s) -> b -> c
forall s a b.
(HasV s a, HasV s b) =>
(V s a s -> V s b s) -> a -> b
onV ((V s b s -> V s c s) -> b -> c)
-> (a -> V s a s) -> (V s a s -> V s b s -> V s c s) -> a -> b -> c
forall a b a' b'. (b -> b') -> (a' -> a) -> (a -> b) -> a' -> b'
<~ a -> V s a s
forall s a. HasV s a => a -> V s a s
toV

-- Can I replace my HasRep class with Newtype?

-- -- Replace by special cases as needed
-- instance HasV s s where
--   type V s s = Par1
--   toV = Par1
--   unV = unPar1

type IsScalar s = (HasV s s, V s s ~ Par1)

instance HasV s () where
  type V s () = U1
  toV :: () -> V s () s
toV () = U1 s
V s () s
forall k (p :: k). U1 p
U1
  unV :: V s () s -> ()
unV U1 s
V s () s
U1 = ()

instance HasV Float Float where
  type V Float Float = Par1
  toV :: Float -> V Float Float Float
toV = Float -> Par1 Float
Float -> V Float Float Float
forall p. p -> Par1 p
Par1
  unV :: V Float Float Float -> Float
unV = Par1 Float -> Float
V Float Float Float -> Float
forall p. Par1 p -> p
unPar1

instance HasV Double Double where
  type V Double Double = Par1
  toV :: Double -> V Double Double Double
toV = Double -> Par1 Double
Double -> V Double Double Double
forall p. p -> Par1 p
Par1
  unV :: V Double Double Double -> Double
unV = Par1 Double -> Double
V Double Double Double -> Double
forall p. Par1 p -> p
unPar1

-- etc

instance (HasV s a, HasV s b) => HasV s (a :* b) where
  type V s (a :* b) = V s a :*: V s b
  toV :: (a :* b) -> V s (a :* b) s
toV (a
a,b
b) = a -> V s a s
forall s a. HasV s a => a -> V s a s
toV a
a V s a s -> V s b s -> (:*:) (V s a) (V s b) s
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b -> V s b s
forall s a. HasV s a => a -> V s a s
toV b
b
  unV :: V s (a :* b) s -> a :* b
unV (V s a s
f :*: V s b s
g) = (V s a s -> a
forall s a. HasV s a => V s a s -> a
unV V s a s
f,V s b s -> b
forall s a. HasV s a => V s a s -> a
unV V s b s
g)
  {-# INLINE toV #-} ; {-# INLINE unV #-}

instance OpCon (:*) (Sat (HasV s)) where
  inOp :: forall a b.
(Sat (HasV s) a && Sat (HasV s) b) |- Sat (HasV s) (a :* b)
inOp = (Con (Sat (HasV s) a && Sat (HasV s) b)
 :- Con (Sat (HasV s) (a :* b)))
-> (Sat (HasV s) a && Sat (HasV s) b) |- Sat (HasV s) (a :* b)
forall a b. (Con a :- Con b) -> a |- b
Entail (((HasV s a, HasV s b) => Dict (HasV s (a :* b)))
-> (HasV s a, HasV s b) :- HasV s (a :* b)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (HasV s (a :* b))
(HasV s a, HasV s b) => Dict (HasV s (a :* b))
forall (a :: Constraint). a => Dict a
Dict)
  {-# INLINE inOp #-}

instance (HasV s a, HasV s b) => HasV s (a :+ b) where
  type V s (a :+ b) = V s a :+: V s b
  toV :: (a :+ b) -> V s (a :+ b) s
toV (Left  a
a) = V s a s -> (:+:) (V s a) (V s b) s
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a -> V s a s
forall s a. HasV s a => a -> V s a s
toV a
a)
  toV (Right b
b) = V s b s -> (:+:) (V s a) (V s b) s
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b -> V s b s
forall s a. HasV s a => a -> V s a s
toV b
b)
  unV :: V s (a :+ b) s -> a :+ b
unV (L1 V s a s
fs) = a -> a :+ b
forall a b. a -> Either a b
Left  (V s a s -> a
forall s a. HasV s a => V s a s -> a
unV V s a s
fs)
  unV (R1 V s b s
gs) = b -> a :+ b
forall a b. b -> Either a b
Right (V s b s -> b
forall s a. HasV s a => V s a s -> a
unV V s b s
gs)
  {-# INLINE toV #-} ; {-# INLINE unV #-}

-- instance (HasV s a, HasV s b, Zeroable (V s a), Zeroable (V s b), Num s)
--       => HasV s (a :+ b) where
--   type V s (a :+ b) = V s a :*: V s b
--   toV (Left  a) = toV a :*: zeroV
--   toV (Right b) = zeroV :*: toV b
--   unV (f :*: g) = error "unV on a :+ b undefined" f g

instance (HasV s a, HasV s b, HasV s c) => HasV s (a,b,c)
instance (HasV s a, HasV s b, HasV s c, HasV s d) => HasV s (a,b,c,d)

-- Sometimes it's better not to use the default. I think the following gives more reuse:

-- instance HasV s a => HasV s (Pair a) where
--   type V s (Pair a) = Pair :.: V s a
--   toV = Comp1 . fmap toV
--   unV = fmap unV . unComp1

-- Similarly for other functors

instance HasV s (U1 a)
instance HasV s a => HasV s (Par1 a)
instance (HasV s (f a), HasV s (g a)) => HasV s ((f :*: g) a)
instance (HasV s (g (f a))) => HasV s ((g :.: f) a)

instance HasV s (f a) => HasV s (SumV f a)

instance HasV s a => HasV s (Sum a)
instance HasV s a => HasV s (Product a)
-- TODO: More newtypes

-- Sometimes it's better not to use the default. I think the following gives more reuse:

-- instance HasV s a => HasV s (Pair a) where
--   type V s (Pair a) = Pair :.: V s a
--   toV = Comp1 . fmap toV
--   unV = fmap unV . unComp1

-- Similarly for other functors

class VComp h where
  vcomp :: forall s c. HasV s c :- (HasV s (h c), V s (h c) ~ (h :.: V s c))

#if 1
instance HasV s b => HasV s (a -> b) where
  type V s (a -> b) = (->) a :.: V s b
  toV :: (a -> b) -> V s (a -> b) s
toV = (a -> V s b s) -> (:.:) ((->) a) (V s b) s
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 ((a -> V s b s) -> (:.:) ((->) a) (V s b) s)
-> ((a -> b) -> a -> V s b s)
-> (a -> b)
-> (:.:) ((->) a) (V s b) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> V s b s) -> (a -> b) -> a -> V s b s
forall a b. (a -> b) -> (a -> a) -> a -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> V s b s
forall s a. HasV s a => a -> V s a s
toV
  unV :: V s (a -> b) s -> a -> b
unV = (V s b s -> b) -> (a -> V s b s) -> a -> b
forall a b. (a -> b) -> (a -> a) -> a -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap V s b s -> b
forall s a. HasV s a => V s a s -> a
unV ((a -> V s b s) -> a -> b)
-> ((:.:) ((->) a) (V s b) s -> a -> V s b s)
-> (:.:) ((->) a) (V s b) s
-> a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) ((->) a) (V s b) s -> a -> V s b s
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1
  {-# INLINE toV #-} ; {-# INLINE unV #-}
#else
instance HasV s b => HasV s (a -> b) where
  type V s (a -> b) = Map a :.: V s b
  toV = Comp1 . ??
  unV = ?? . unComp1
#endif

instance VComp ((->) a) where vcomp :: forall s c.
HasV s c :- (HasV s (a -> c), V s (a -> c) ~ ((->) a :.: V s c))
vcomp = (HasV s c =>
 Dict (HasV s (a -> c), ((->) a :.: V s c) ~ ((->) a :.: V s c)))
-> HasV s c
   :- (HasV s (a -> c), ((->) a :.: V s c) ~ ((->) a :.: V s c))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (HasV s (a -> c), ((->) a :.: V s c) ~ ((->) a :.: V s c))
HasV s c =>
Dict (HasV s (a -> c), ((->) a :.: V s c) ~ ((->) a :.: V s c))
forall (a :: Constraint). a => Dict a
Dict

#ifdef VectorSized

#if 0
-- Until I work out HasL (g :.: f) or stop using it, restrict elements to s.
instance KnownNat n => HasV s (Vector n s) where
  type V s (Vector n s) = Vector n
  toV = id
  unV = id
  {-# INLINE toV #-}
  {-# INLINE unV #-}
#else
instance (HasV s b, KnownNat n) => HasV s (Vector n b) where
  type V s (Vector n b) = Vector n :.: V s b
  toV :: Vector n b -> V s (Vector n b) s
toV = Vector n (V s b s) -> (:.:) (Vector Vector n) (V s b) s
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (Vector n (V s b s) -> (:.:) (Vector Vector n) (V s b) s)
-> (Vector n b -> Vector n (V s b s))
-> Vector n b
-> (:.:) (Vector Vector n) (V s b) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> V s b s) -> Vector n b -> Vector n (V s b s)
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC b -> V s b s
forall s a. HasV s a => a -> V s a s
toV
  unV :: V s (Vector n b) s -> Vector n b
unV = (V s b s -> b) -> Vector n (V s b s) -> Vector n b
forall (k :: * -> * -> *) (h :: * -> *) a b.
(FunctorCat k h, Ok2 k a b) =>
k a b -> k (h a) (h b)
fmapC V s b s -> b
forall s a. HasV s a => V s a s -> a
unV (Vector n (V s b s) -> Vector n b)
-> ((:.:) (Vector Vector n) (V s b) s -> Vector n (V s b s))
-> (:.:) (Vector Vector n) (V s b) s
-> Vector n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:.:) (Vector Vector n) (V s b) s -> Vector n (V s b s)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1
  {-# INLINE toV #-}
  {-# INLINE unV #-}
#endif

#else
instance (HasV s b) => HasV s (Vector n b) where
  type V s (Vector n b) = Vector n :.: V s b
  toV = Comp1 . fmapC toV
  unV = fmapC unV . unComp1
  {-# INLINE toV #-}
  {-# INLINE unV #-}
#endif

-- TODO: find a better alternative to using fmapC explicitly here. I'd like to
-- use fmap instead, but it gets inlined immediately, as do all class
-- operations.

-- instance 
-- #ifdef VectorSized
--          KnownNat n =>
-- #endif
--          VComp (Vector n) where vcomp = Sub Dict

#ifndef VectorSized
instance VComp (Vector n) where vcomp = Sub Dict
#endif

#if 0
-- Example default instance

data Pickle a = Pickle a a a

instance HasRep (Pickle a) where
  type Rep (Pickle a) = (a :* a) :* a
  repr (Pickle a b c) = ((a,b),c)
  abst ((a,b),c) = Pickle a b c

instance HasV s a => HasV s (Pickle a)
#endif

#if 0
-- -- | The 'unV' form of 'zeroV'
-- zeroX :: forall s a. (HasV s a, Zeroable (V s a)) => a
-- zeroX = unV (zeroV :: V s a s)

vfun :: (HasV s a, HasV s b) => (a -> b) -> UT s (V s a) (V s b)
vfun = UT . inV

-- vfun f = UT (toV . f . unV)

-- | Free vector over scalar s
data VFun s

instance FunctorC (VFun s) (Constrained (HasV s) (->)) (UT s) where
  -- type OkF (VFun s) = HasV s
  -- type OkF (VFun s) a = HasV s a
  -- type OkF (VFun s) b a = (HasV s a, HasV s b)
  type VFun s % a = V s a
  fmapC (Constrained f) = UT (inV f)
                          -- vfun f

#endif

#if 0

{--------------------------------------------------------------------
    Coercible
--------------------------------------------------------------------}

-- I don't think I need this stuff.

-- As a second default, we can use coercible types.
coerceToV :: forall s a b. (Coercible a b, HasV s b) => a -> V s b s
coerceToV = toV . (coerce :: a -> b)

coerceUnV :: forall s a b. (Coercible a b, HasV s b) => V s b s -> a
coerceUnV = (coerce :: b -> a) . unV

#if 0

#define CoerceHasV(s,ty,rep) \
instance HasV s (rep) => HasV s (ty) where \
  { type V s (ty) = V s (rep) \
  ; toV = coerceToV @ s @ (ty) @ (rep) \
  ; unV = coerceUnV @ s @ (ty) @ (rep) }

newtype Two s = Two (s :* s)

-- instance HasV s s => HasV s (Two s) where
--   type V s (Two s) = V s (s :* s)
--   toV = coerceToV @ s @ (Two s) @ (s :* s)
--   unV = coerceUnV @ s @ (Two s) @ (s :* s)

CoerceHasV(s,Two s,s :* s)

#endif

#endif

{--------------------------------------------------------------------
    Utilities
--------------------------------------------------------------------}