自然数的单射型族

Question

我正在尝试编写一些函数来操作固定大小的向量(使用vector-sized包(。它们使用GHC.TypeNats对类型本身中的长度进行编码。但是，当我想重复一个操作(在这种情况下getAllVectors(一定次数时，我遇到了一些问题。由于getAllVectors的第二个参数会影响结果类型，因此我似乎需要经历本页中描述的内容。但这不能编译 - Haskell抱怨FromNat1不是注入的，即使我很确定它是。

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE GADTs #-}
import GHC.TypeNats 
import Data.Vector.Sized (Vector)
import qualified Data.Vector.Sized as Vec 
data Nat1 = Zero | Succ Nat1
type family FromNat1 (n :: Nat1) = (c :: Nat) | c -> n 
type instance FromNat1 Zero     = 0
type instance FromNat1 (Succ n) = 1 + FromNat1 n
getAllVectors :: forall s n. [s] -> Nat1 -> [Vector (FromNat1 n) s]
getAllVectors s Zero = [Vec.empty]
getAllVectors s (Succ x) = Vec.cons <$> s <*> getAllVectors s x

有没有更好的方法可以做到这一点？如果有更好的选择，我不严格要求使用vector-sized

Answer 1

通常最好从"真实"的东西开始，然后将它们翻译成"假货"。以下是您真正执行此操作的方法：

data Nat = Z | S Nat
data SNat n where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
data Vec n a where
Nil :: Vec 'Z a
Cons :: a -> Vec n a -> Vec ('S n) a
getAllVectors :: forall s n. [s] -> SNat n -> [Vec n s]
getAllVectors s SZ = [Nil]
getAllVectors s (SS x) = Cons <$> s <*> getAllVectors s x

使用单例将自然数参数的大小与结果中向量的大小联系起来。

为了使这种事情适用于假类型，您可能希望类型家庭双向发展。不要害怕看起来像

(ToTL n ~ n', FromTL n' ~ n)

如果这些被证明是有道理的。

注意其他事情：使用Data.Vector.Sized的实现效率非常低，因为构思向量很慢。你真的需要那个吗？