haskell - 如何将列表惰性地转换为这种类型？

Question

考虑这个Vect类型:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}

import Data.Kind (Type)

data Nat = Zero | Succ Nat

data Vect :: Nat -> Type -> Type where
  Nil :: Vect 'Zero a
  Cons :: a -> Vect n a -> Vect ('Succ n) a

我想编写一个函数，它接受一个列表并将其惰性地转换为这种类型。由于长度显然是未知的，我们需要使用存在式。我第一次尝试使用 CPS 和 2 级类型来模拟:

listToVect1 :: [a] -> (forall n. Vect n a -> b) -> b
listToVect1 [] f = f Nil
listToVect1 (x:xs) f = listToVect1 xs (f . Cons x)

但是，这并不懒惰。这只是一个foldl(尽管写为显式递归，因为实际使用foldl需要必然性)，所以f不会开始运行，直到它一直走到最后列表中的。

我想不出一种以右关联方式进行 CPS 的方法，所以我再次尝试，这次使用包装类型:

data ArbitraryVect a = forall n. ArbitraryVect (Vect n a)

nil :: ArbitraryVect a
nil = ArbitraryVect Nil

cons :: a -> ArbitraryVect a -> ArbitraryVect a
cons x (ArbitraryVect xs) = ArbitraryVect (Cons x xs)

listToVect2 :: [a] -> ArbitraryVect a
listToVect2 = foldr cons nil

这种尝试的问题是我必须使用data而不是newtype(或者我得到A newtype构造函数不能有存在类型变量)，并且我需要在 cons 中严格进行模式匹配(或者我得到 An Existential 或 GADT 数据构造函数不能在惰性 (~) 模式内使用)，所以在遍历整个列表之前它不会返回任何内容。

对于如何做到这一点，我没有任何其他想法。这可能吗？如果是这样，怎么办？如果没有，为什么不呢？

Answer 1

这将是一个令人不满意的答案，但无论如何我都会发布它。

<小时/>

我认为这在技术上是不可能的，因为结果的头部应该包含类型 n ，并且类型不能被延迟构造。它们有点“短暂”，在运行时并不真正存在，但逻辑上它们必须被完全了解。

(尽管我不能 100% 确定上述内容是否正确)

<小时/>

但是，如果您确实需要这样做，您可以作弊。观察到多态延续实际上并不了解 n 的任何信息。 。它唯一可能找到的关于n的信息是是否是Zero或Succ ，但即使如此，实际上也没有在运行时以任何方式进行编码。相反，它是从 Vect 的任何构造函数推断出来的。模式匹配期间匹配。这意味着，在运行时，我们实际上不必为 n 传递正确的类型。 。当然，如果编译器不能证明类型是正确的，它在编译过程中会感到焦虑，但我们可以用unsafeCoerce说服它闭嘴。 :

listToVect1 :: [a] -> (forall n. Vect n a -> b) -> b
listToVect1 xs f = f $ go xs
  where
    go :: [a] -> Vect Zero a
    go [] = Nil
    go (x:xs) = unsafeCoerce $ Cons x (go xs)

这里是 go 的第二行构造一个Vect (Succ Zero) a ，但随后删除其 n组件至Zero 。每一步都会发生这种情况，因此最终结果始终是 Vect Zero a 。然后这个结果被传递给延续，这并不明智，因为它并不关心。

当后续尝试匹配 Vect 时的构造函数，它工作得很好，因为构造函数已按正确的顺序正确实例化，反射(reflect)了向量的正确形状，并且通过扩展，反射(reflect)了 n 的正确形状。 .

这有效，尝试一下:

vectLen :: Vect n a -> Int
vectLen Nil = 0
vectLen (Cons _ xs) = 1 + vectLen xs

toList :: Vect n a -> [a]
toList Nil = []
toList (Cons a xs) = a : toList xs

main :: IO ()
main = do
  print $ listToVect1 [1,2,3] vectLen        -- prints 3
  print $ listToVect1 [] vectLen             -- prints 0
  print $ listToVect1 [1,2,3,4,5] vectLen    -- prints 5

  print $ listToVect1 [1,2,3] toList         -- prints [1,2,3]
  print $ listToVect1 ([] :: [Int]) toList   -- prints []
  print $ listToVect1 [1,2,3,4,5] toList     -- prints [1,2,3,5]

<小时/>

当然，上面的内容是脆弱的。它(在某种程度上)依赖于一些较低级别的知识。如果这不仅仅是一次好奇心练习，我宁愿回去重新思考导致您出现此问题的原始问题。

但无论如何，这种“挥手遮丑”的技术在底层库中使用得比较普遍。