有没有办法给withVec提供一个类似id的函数来提取中间向量？
不，withVec的类型是精心制作的，正是为了防止这种情况。
旁注：在库中，这个“技巧”通常用于runST类型，以确保ST s monad的安全性。
任何尝试创建一个函数，它的结果是类型Vec n a已经失败。
实际上，这在设计上是不可能的。
没有一个fromList函数可以从一个列表中创建一个Vec n a。为什么？我们不能创建一个编译时检查的fromList函数来从一个长度为n的列表中创建一个合适的Vec a n，这是有原因的吗？
一开始可能并不明显，但这在现实中并不可行。
假设我们有这样一个fromList，它的类型是什么？让我们猜一下：

fromList :: [a] -> Vec n a

字符串
但这实际上意味着

fromList :: forall a n . [a] -> Vec n a

型
所以它声称能够将任何列表转换为任何长度的任何向量。这不可能是合理的。
问题是forall n部分意味着fromList的 * 调用者 * 可以选择n。但是这样就不能保证n是输入列表的长度，所以存在不匹配。
我们可以尝试让n被fromList选择，而不是被调用者选择。

fromList :: [a] -> exists n . Vec n a    -- pseudo-Haskell

型
然而，这有两个后果。
首先，exists n . Vec n a是一个未知长度的向量类型，因此本质上同构于[a]，使得fromList不是很有用。
第二，我们可以利用一种已知的编码来表示真实的Haskell中的存在类型，但这将是

fromList :: forall a r . [a] -> (forall n . Vec n a -> r) -> r

型
它与withVec非常相似！（实际上withVec比这个变体更有用。）
另一种替代方法是类似于

fromList :: Sing n -> [a] -> Maybe (Vec n a)

型
这里，调用者必须（静态地）预测（动态地）列表的长度n。如果它是正确的，他们得到Just theVector，否则他们得到Nothing。这是否有用取决于我们是否可以在静态时正确地猜测n。
请注意，就我所知，fromList的最后一个变体似乎可以在给定withVec的情况下实现。
最后，在一种完全依赖类型的语言中，我们可以编写

fromList :: (xs :: [a]) -> Vec (length xs) a   -- not Haskell

型
但是Haskell没有真正的依赖类型（因为它的目标是为了效率而允许全类型擦除）。

为什么函数不能将列表转换为向量？

fromList :: [a] -> Vec n a

字符串
应用于空列表，当唯一有意义的类型是Vec 0 a时，这会产生一个任意长度的向量fromList [] :: Vec n a。你可以看到这是一个“某个长度 n”的向量，其中 n 是存在的（proposal）。没有依赖类型，我们不知道。

fromList :: [a] -> exists n. Vec n a

型
这与withVec相同，withVec使用CPS对存在性进行编码。唯一的区别是Sing n：在运行时保留（不删除）长度。

withVec :: [a] -> (forall n. Sing n -> Vec n a -> r) -> r
--                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

型
我不认为exists.有一个相关的名字已经决定了。它可以编码为一个数据类型。

type SomeVec :: Type -> Type
data SomeVec a where
  SomeVec :: Sing n -> Vec n a -> SomeVec a

fromList :: [a] -> SomeVec a

型
这样的存在式非常适合模式同义词，它允许你在普通列表上进行模式匹配并得到一个向量。我也在单例Sing上进行模式匹配，说我们静态地知道长度 n。

{-# Complete AsVec #-}

--                               existential
--                               vvvvvvvvv
pattern AsVec :: forall a. () => forall n. SingI n => Vec n a -> [a]
pattern AsVec vec <- (fromList -> SomeVec Sing vec)
  where AsVec = fromVec

>> case [1..10] of AsVec vec -> show vec
"1 :> (2 :> (3 :> (4 :> (5 :> (6 :> (7 :> (8 :> (9 :> (10 :> VNil)))))))))"

有趣的是，当标识延续传递给(withVec\_ -> id)时会发生什么。