如何编写通用量化函数的存在版本？

如何解决如何编写通用量化函数的存在版本？

我正在尝试解决一个依赖类型问题，我将其缩小为以下漫画，即从大小的向量中删除索引：

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

解决方法

您将 natVal 与 0 和 unsafeCoerce 进行比较。没有别的选择。您可以将其包装在稍微安全的类型签名中，如 sCmpNat 或类似的。