haskell - 无法从列表构造固定长度向量

我正在尝试从列表中构造一个固定长度的向量，但不确定给编译器提供什么样的帮助来推断 fromList 的每次返回都会在类型级别将长度增加一个。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}

import Data.Typeable
import GHC.TypeLits

data Vec :: Nat -> * -> * where
    VNil :: Vec 0 a
    (:+) :: a -> Vec n a -> Vec (n + 1) a

infixr 5 :+

instance Show a => Show (Vec n a) where
    show VNil = " VNil"
    show (h :+ t) = show h ++ " : " ++ show t

deriving instance (Typeable n, Typeable a) => Typeable (Vec n a)

fromList :: [a] -> Vec n a
fromList xs = build xs
  where
    build (x:xs) = x :+ (build xs)
    build ([]) = error "fromList: list too short"

main.hs:27:15: error:
    • Couldn't match expected type ‘n’ with actual type ‘n + 1’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          fromList :: forall a (n :: Nat). [a] -> Vec n a
        at main.hs:26:1-26
    • In the expression: build xs
      In an equation for ‘fromList’:
          fromList xs
            = build xs
            where
                build (x : xs) = x :+ (build xs)
                build ([]) = error "fromList: list too short"
    • Relevant bindings include
        fromList :: [a] -> Vec n a (bound at main.hs:27:1)
   |
27 | fromList xs = build xs
   |

Runnable code at repl.it

最佳答案

您需要编写 fromList 以便它可以提供一些未知(在编译时)Vec n a 的 n 而不是任何给定的 n 。一种方法是用连续传递风格重写它:

{-# LANGUAGE RankNTypes #-}

fromList :: [a] -> (forall n. Vec n a -> r) -> r
fromList (x:xs) cont = fromList xs (\v -> cont (x :+ v))
fromList [] cont = cont VNil

在你的例子中，编译器提示是因为 n 是一个“刚性类型变量”——换句话说，fromList 在它的类型的开头有一个隐式的 forall n，所以 fromList 的调用者可以为 fromList 提供一个任意的 n 并期望它工作.这不是您想要的，因为您希望 fromList 根据列表的长度计算 n，而不是从其调用方接收 n。

因此，解决方案是让 fromList 提供 n ，通过调用本身将 n 作为 forall 类型变量的延续。

在数学术语中，您希望 n 被存在量化——存在一些 n fromList 从给定的输入生成 Vec n a——不是普遍量化的——对于所有 n ， fromList 将从给定的输入生成 Vec n a。

除了延续传递之外，还有其他方法可以在 Haskell 中编码存在量化。这是一个替代方案:

data SomeVec a = forall n. SomeVec (Vec n a)

fromList' :: [a] -> SomeVec a
fromList' (x:xs) = case (fromList' xs) of (SomeVec v) -> SomeVec (x :+ v)
fromList' [] = SomeVec VNil

这种方法在某些情况下可能更清晰，但可能需要您为 SomeVec 实现一堆已经为 Vec 实现的实例。

(您可能还会注意到，这实际上并不是一种完全不同的方法；fromList' xs = fromList xs SomeVec。)

有关更多信息，搜索“Haskell 中的存在类型”应该会找到大量进一步的线索。

关于haskell - 无法从列表构造固定长度向量，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/56295092/