问题描述
我正在尝试解决一个依赖类型问题，我将其缩小为以下漫画，即从大小的向量中删除索引：
TL;DR 给定 rmIx，我该怎么写 someRmIx？
rmIx :: forall ix n a. Vector (n+1) a -> Vector n a
someRmIx :: forall ix a. SomeVector a -> SomeVector a
在 someRmIx 版本中，我需要见证 rmIx 函数中的约束，并且，如果我无法满足这些约束（例如，您无法从 {{ 1}})，然后返回 Vector 0 a 不变。
SomeVector编译上述内容的必要宣传：
module SomeVector where
import qualified Data.Vector.Sized as V
import Data.Vector.Sized
import GHC.TypeNats
import Data.Proxy
import Type.Reflection
import Data.Type.Equality
import Unsafe.Coerce (unsafeCoerce)
import Data.Data (eqT)
data SomeVector a = forall n. KNownNat n => SomeVector (Vector n a)
-- | Remove an index from an existentially sized 'Vector'.
someRmIx :: forall (ix :: Nat) a m. KNownNat ix => SomeVector a -> SomeVector a
someRmIx (SomeVector (v :: Vector n a)) =
--------------------------------------------------
--------------------------------------------------
--------------------------------------------------
-- WHAT DO I DO HERE???
--------------------------------------------------
--------------------------------------------------
--------------------------------------------------
case ??????? of
nothing -> SomeVector v
Just Refl -> SomeVector $ rmIx @ix v
-- | Remove an index of a 'Vector'.
rmIx :: forall (ix :: Nat) n a (m :: Nat).
(ix <= n,-- in my actual code I clean this up with GHC.TypeLits.normalise
KNownNat ix,(ix + m) ~ n,((n - ix) + 1) ~ (1 + m),(n + 1) ~ (ix + (1 + m))
)
=> Vector (n+1) a -> Vector n a
rmIx v = l V.++ r
where (l :: Vector ix a,r' :: Vector (n-ix+1) a) = V.splitAt' (Proxy @ix) v
(r :: Vector m a) = V.drop' (Proxy @1) r'
----------
-- * Tests
myV :: Vector 5 Int
myV = let Just v = V.fromList [1,2,3,4,5]
in v
test1 :: Vector 4 Int
test1 = rmIx @2 myV
test2 :: SomeVector Int
test2 = someRmIx @2 $ SomeVector myV