length-indexed lists

[alang9]

I'm a bit surprised to not see a structure like the following in the package:

data L n a where
  LNil :: L 0 a
  (:.) :: (KnownNat n) => a -> L n a -> L (1 + n) a

infixr 5 :.

deriving instance (Show a) => Show (L n a)

instance (Eq a) => Eq (L n a) where
  LNil == LNil = True
  LNil == (_ :. _) = error "impossible"
  (_ :. _) == LNil = error "impossible"
  (a1 :. (t1 :: L p a)) == (a2 :. (t2 :: L q a)) = case plusIsCancellative @1 @p @q of
    Sub Dict -> a1 == a2 && t1 == t2

deriving instance Functor (L n)

instance (KnownNat n) => Applicative (L n) where
  pure :: forall a. a -> L n a
  pure a = go LNil
    where
      go :: forall m. (KnownNat m, KnownNat n) => L m a -> L n a
      go as = case sameNat (Proxy :: Proxy (m :: Nat)) (Proxy :: Proxy (n :: Nat)) of
        Nothing -> case plusNat @1 @m of
          Sub Dict -> go @ (1 + (m :: Nat)) (a :. as)
        Just Refl -> as
  LNil <*> LNil = LNil
  LNil <*> _ = error "impossible"
  _ <*> LNil = error "impossible"
  f :. (fs :: L p (a -> b)) <*> a :. (as :: L q a) = case plusIsCancellative @1 @p @q of
    Sub Dict -> f a :. (fs <*> as)

instance Foldable (L n) where
  foldMap _ LNil = mempty
  foldMap f (x :. xs) = f x <> foldMap f xs

instance (KnownNat n) => Additive (L n) where
  zero = pure 0
  liftU2 _ LNil LNil = LNil
  liftU2 _ LNil _ = error "impossible"
  liftU2 _ _ LNil = error "impossible"
  liftU2 f (a:.(as :: L p a)) (b :. (bs :: L q a)) = case plusIsCancellative @1 @p @q of
    Sub Dict -> f a b :. liftU2 f as bs
  liftI2 _ LNil LNil = LNil
  liftI2 _ LNil _ = error "impossible"
  liftI2 _ _ LNil = error "impossible"
  liftI2 f (a:.(as :: L p a)) (b :. (bs :: L q b)) = case plusIsCancellative @1 @p @q of
    Sub Dict -> f a b :. liftI2 f as bs

instance (KnownNat n) => Metric (L n)

Compared to Linear.V, this allows us to write:

> Linear.Metric.dot (2 :. 3 :. 4 :. LNil) (5 :. 6 :. 7 :. LNil)
56

instead of:

> (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