如何构建具有依赖类型长度的列表？

Question

将我的脚趾浸入依赖类型的水域，我对规范的“具有静态类型长度的列表”示例感到满意。

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

-- a kind declaration
data Nat = Z | S Nat

data SafeList :: (Nat -> * -> *) where
    Nil :: SafeList Z a
    Cons :: a -> SafeList n a -> SafeList (S n) a

-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x

这似乎有效：

ghci> :t Cons 5 (Cons 3 Nil)
Cons 5 (Cons 3 Nil) :: Num a => SafeList ('S ('S 'Z)) a

ghci> safeHead (Cons 'x' (Cons 'c' Nil))
'x'

ghci> safeHead Nil
Couldn't match type 'Z with 'S n0
Expected type: SafeList ('S n0) a0
  Actual type: SafeList 'Z a0
In the first argument of `safeHead', namely `Nil'
In the expression: safeHead Nil
In an equation for `it': it = safeHead Nil

但是，为了使这种数据类型真正有用，我应该能够从运行时数据构建它，而您在编译时不知道其长度。我天真的尝试：

fromList :: [a] -> SafeList n a
fromList = foldr Cons Nil

编译失败，类型错误：

Couldn't match type 'Z with 'S n
Expected type: a -> SafeList n a -> SafeList n a
  Actual type: a -> SafeList n a -> SafeList ('S n) a
In the first argument of `foldr', namely `Cons'
In the expression: foldr Cons Nil
In an equation for `fromList': fromList = foldr Cons Nil

我明白为什么会发生这种情况：Cons 的返回类型对于折叠的每次迭代都不同 - 这就是重点！但是我看不到解决方法，可能是因为我对该主题的阅读不够深入。 （我无法想象所有这些努力都被投入到一个无法在实践中使用的类型系统中！）

那么：我如何从“正常”简单类型的数据中构建这种依赖类型的数据？

---

按照@luqui 的建议，我能够使fromList 编译：

data ASafeList a where
    ASafeList :: SafeList n a -> ASafeList a

fromList :: [a] -> ASafeList a
fromList = foldr f (ASafeList Nil)
    where f x (ASafeList xs) = ASafeList (Cons x xs)

这是我解压ASafeList 并使用它的尝试：

getSafeHead :: [a] -> a
getSafeHead xs = case fromList xs of ASafeList ys -> safeHead ys

这会导致另一个类型错误：

Couldn't match type `n' with 'S n0
  `n' is a rigid type variable bound by
      a pattern with constructor
        ASafeList :: forall a (n :: Nat). SafeList n a -> ASafeList a,
      in a case alternative
      at SafeList.hs:33:22
Expected type: SafeList ('S n0) a
  Actual type: SafeList n a
In the first argument of `safeHead', namely `ys'
In the expression: safeHead ys
In a case alternative: ASafeList ys -> safeHead ys

再次，直观地说，这将无法编译是有道理的。我可以使用空列表调用fromList，因此编译器不能保证我能够在结果SafeList 上调用safeHead。这种缺乏知识大致就是存在主义ASafeList 所捕捉到的。

这个问题能解决吗？我觉得我可能已经走上了一个合乎逻辑的死胡同。

Answer 1

如果您想对运行时数据使用依赖类型的函数，那么您需要确保该数据不违反类型签名法中的编码。通过一个例子更容易理解这一点。这是我们的设置：

data Nat = Z | S Nat

data Natty (n :: Nat) where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

data Vec :: * -> Nat -> * where
  VNil :: Vec a Z
  VCons :: a -> Vec a n -> Vec a (S n)

我们可以在Vec上写一些简单的函数：

vhead :: Vec a (S n) -> a
vhead (VCons x xs) = x

vtoList :: Vec a n -> [a]
vtoList  VNil        = []
vtoList (VCons x xs) = x : vtoList xs

vlength :: Vec a n -> Natty n
vlength  VNil        = Zy
vlength (VCons x xs) = Sy (vlength xs)

为了编写lookup 函数的规范示例，我们需要finite sets 的概念。它们通常被定义为

data Fin :: Nat -> where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

Fin n代表所有小于n的数字。

但是就像Nats — Nattys 的类型级别等价物一样，Fins 的类型级别等价物也是如此。但是现在我们可以合并值级别和类型级别Fins：

data Finny :: Nat -> Nat -> * where
    FZ :: Finny (S n) Z
    FS :: Finny n m -> Finny (S n) (S m)

第一个Nat 是Finny 的上限。第二个Nat 对应于Finny 的实际值。 IE。它必须等于toNatFinny i，其中

toNatFinny :: Finny n m -> Nat
toNatFinny  FZ    = Z
toNatFinny (FS i) = S (toNatFinny i)

现在定义lookup 函数很简单：

vlookup :: Finny n m -> Vec a n -> a
vlookup  FZ    (VCons x xs) = x
vlookup (FS i) (VCons x xs) = vlookup i xs

还有一些测试：

print $ vlookup  FZ               (VCons 1 (VCons 2 (VCons 3 VNil))) -- 1
print $ vlookup (FS FZ)           (VCons 1 (VCons 2 (VCons 3 VNil))) -- 2
print $ vlookup (FS (FS (FS FZ))) (VCons 1 (VCons 2 (VCons 3 VNil))) -- compile-time error

这很简单，但是take 函数呢？这并不难：

type Finny0 n = Finny (S n)

vtake :: Finny0 n m -> Vec a n -> Vec a m
vtake  FZ     _           = VNil
vtake (FS i) (VCons x xs) = VCons x (vtake i xs)

我们需要Finny0 而不是Finny，因为lookup 要求Vec 不为空，所以如果有Finny n m 类型的值，那么对于某些n'，n = S n' .但是vtake FZ VNil 是完全有效的，所以我们需要放宽这个限制。所以Finny0 n 代表所有小于或等于n 的数字。

但是运行时数据呢？

vfromList :: [a] -> (forall n. Vec a n -> b) -> b
vfromList    []  f = f VNil
vfromList (x:xs) f = vfromList xs (f . VCons x)

即“给我一个列表和一个函数，它接受任意长度的Vec，我会将后者应用于前者”。 vfromList xs 返回一个延续（即 (a -> r) -> r 类型的东西）模更高级别的类型。让我们试试吧：

vmhead :: Vec a n -> Maybe a
vmhead  VNil        = Nothing
vmhead (VCons x xs) = Just x

main = do
    print $ vfromList ([] :: [Int]) vmhead -- Nothing
    print $ vfromList  [1..5]       vmhead -- Just 1

有效。但我们不只是重复自己吗？为什么vmhead，已经有vhead？我们是否应该以不安全的方式重写所有安全函数，以便在运行时数据上使用它们？那太傻了。

我们只需要确保所有不变量都成立。让我们在vtake 函数上试试这个原理：

fromIntFinny :: Int -> (forall n m. Finny n m -> b) -> b
fromIntFinny 0 f = f FZ
fromIntFinny n f = fromIntFinny (n - 1) (f . FS)

main = do       
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i' ->
        vfromList xs   $ \xs' ->
        undefined -- what's here?

fromIntFinny 就像vfromList。看看这些类型是有启发性的：

i'  :: Finny n m
xs' :: Vec a p

但是vtake 有这种类型：Finny0 n m -> Vec a n -> Vec a m。所以我们需要强制i'，使它成为Finny0 p m类型。而且toNatFinny i' 必须等于toNatFinny coerced_i'。但这种强制转换一般是不可能的，因为如果S p < n，那么Finny n m 中的元素不在Finny (S p) m 中，因为S p 和n 是上限。

coerceFinnyBy :: Finny n m -> Natty p -> Maybe (Finny0 p m)
coerceFinnyBy  FZ     p     = Just FZ
coerceFinnyBy (FS i) (Sy p) = fmap FS $ i `coerceFinnyBy` p
coerceFinnyBy  _      _     = Nothing

这就是为什么这里有Maybe。

main = do       
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i' ->
        vfromList xs   $ \xs' ->
        case i' `coerceFinnyBy` vlength xs' of
            Nothing  -> "What should I do with this input?"
            Just i'' -> show $ vtoList $ vtake i'' xs'

在Nothing 的情况下，从输入中读取的数字大于列表的长度。在Just 的情况下，一个数字小于或等于列表的长度并强制转换为适当的类型，因此vtake i'' xs' 是正确类型的。

这可行，但我们引入了coerceFinnyBy 函数，它看起来相当临时。可判定的“小于或等于”关系将是适当的选择：

data (:<=) :: Nat -> Nat -> * where
    Z_le_Z :: Z :<= m                 -- forall n, 0 <= n
    S_le_S :: n :<= m -> S n :<= S m  -- forall n m, n <= m -> S n <= S m

type n :< m = S n :<= m

(<=?) :: Natty n -> Natty m -> Either (m :< n) (n :<= m) -- forall n m, n <= m || m < n
Zy   <=? m    = Right Z_le_Z
Sy n <=? Zy   = Left (S_le_S Z_le_Z)
Sy n <=? Sy m = either (Left . S_le_S) (Right . S_le_S) $ n <=? m

还有一个安全的注入功能：

inject0Le :: Finny0 n p -> n :<= m -> Finny0 m p
inject0Le  FZ     _          = FZ
inject0Le (FS i) (S_le_S le) = FS (inject0Le i le)

即如果n 是某个数字的上限并且n <= m，那么m 也是该数字的上限。还有一个：

injectLe0 :: Finny n p -> n :<= m -> Finny0 m p
injectLe0  FZ    (S_le_S le) = FZ
injectLe0 (FS i) (S_le_S le) = FS (injectLe0 i le)

现在的代码如下所示：

getUpperBound :: Finny n m -> Natty n
getUpperBound = undefined

main = do
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i'  ->
        vfromList xs   $ \xs' ->
        case getUpperBound i' <=? vlength xs' of
            Left  _  -> "What should I do with this input?"
            Right le -> show $ vtoList $ vtake (injectLe0 i' le) xs'

它可以编译，但是getUpperBound 应该有什么定义？好吧，你无法定义它。 Finny n m 中的 n 仅存在于类型级别，您无法提取或获取它。如果我们不能执行“downcast”，我们可以执行“upcast”：

fromIntNatty :: Int -> (forall n. Natty n -> b) -> b
fromIntNatty 0 f = f Zy
fromIntNatty n f = fromIntNatty (n - 1) (f . Sy)

fromNattyFinny0 :: Natty n -> (forall m. Finny0 n m -> b) -> b
fromNattyFinny0  Zy    f = f FZ
fromNattyFinny0 (Sy n) f = fromNattyFinny0 n (f . FS)

比较：

fromIntFinny :: Int -> (forall n m. Finny n m -> b) -> b
fromIntFinny 0 f = f FZ
fromIntFinny n f = fromIntFinny (n - 1) (f . FS)

因此，fromIntFinny 中的延续在n 和m 变量上普遍量化，而fromNattyFinny0 中的延续在m 上普遍量化。并且fromNattyFinny0 收到Natty n 而不是Int。

有Finny0 n m而不是Finny n m，因为FZ是forall n m. Finny n m的一个元素，而FZ不一定是forall m. Finny n m的一个元素，对于某些n，特别是FZ是不是forall m. Finny 0 m 的元素（所以这种类型是无人居住的）。

毕竟，我们可以一起加入fromIntNatty和fromNattyFinny0：

fromIntNattyFinny0 :: Int -> (forall n m. Natty n -> Finny0 n m -> b) -> b
fromIntNattyFinny0 n f = fromIntNatty n $ \n' -> fromNattyFinny0 n' (f n')

达到与@pigworker 的答案相同的结果：

unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t
unLenList (LenList xs) k = k natty xs

一些测试：

main = do
    xs <- readLn :: IO [Int]
    ns <- read <$> getLine
    forM_ ns $ \n -> putStrLn $
        fromIntNattyFinny0 n $ \n' i' ->
        vfromList xs         $ \xs'   ->
        case n' <=? vlength xs' of
            Left  _  -> "What should I do with this input?"
            Right le -> show $ vtoList $ vtake (inject0Le i' le) xs'

为

[1,2,3,4,5,6]
[0,2,5,6,7,10]

返回

[]
[1,2]
[1,2,3,4,5]
[1,2,3,4,5,6]
What should I do with this input?
What should I do with this input?

代码：http://ideone.com/3GX0hd

编辑

嗯，你不能定义它。 Finny n m 中的 n 只存在于类型 级别，你无法提取或获取它。

那不是真的。有了SingI n => Finny n m -> ...，我们可以得到n作为fromSing sing。

Answer 2

永远不要扔掉任何东西。

如果您要不厌其烦地沿着列表转动以创建一个长度索引列表（在文献中称为“向量”），您不妨记住它的长度。

所以，我们有

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where -- old habits die hard
  VNil :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

但我们也可以为静态长度提供运行时表示。 Richard Eisenberg 的“Singletons”包将为您完成此任务，但基本思想是为静态数字提供一种运行时表示。

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

至关重要的是，如果我们有一个 Natty n 类型的值，那么我们可以查询该值以找出 n 是什么。

Hasochists 知道运行时可表示性通常很无聊，甚至机器都可以管理它，因此我们将其隐藏在类型类中

class NATTY (n :: Nat) where
  natty :: Natty n

instance NATTY Z where
  natty = Zy

instance NATTY n => NATTY (S n) where
  natty = Sy natty

现在我们可以对您从列表中获得的长度进行更丰富的存在主义处理。

data LenList :: * -> * where
  LenList :: NATTY n => Vec n a -> LenList a

lenList :: [a] -> LenList a
lenList []        = LenList VNil
lenList (x : xs)  = case lenList xs of LenList ys -> LenList (VCons x ys)

您获得与长度破坏版本相同的代码，但您可以随时获取长度的运行时表示，而无需沿着向量爬行来获取它。

当然，如果您希望长度为Nat，那么对于某些n 使用Natty n 仍然很痛苦。

把口袋弄得乱七八糟是错误的。

编辑我想我会补充一点，以解决“安全头”使用问题。

首先，让我为LenList 添加一个解包器，它会为您提供您手中的号码。

unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t
unLenList (LenList xs) k = k natty xs

现在假设我定义

vhead :: Vec (S n) a -> a
vhead (VCons a _) = a

执行安全属性。如果我有一个向量长度的运行时表示，我可以查看它以查看 vhead 是否适用。

headOrBust :: LenList a -> Maybe a
headOrBust lla = unLenList lla $ \ n xs -> case n of
  Zy    -> Nothing
  Sy _  -> Just (vhead xs)

所以你看一件事，并在这样做的过程中了解另一件事。

Answer 3

在

fromList :: [a] -> SafeList n a

n 是普遍量化的——即这个签名声称我们应该能够从列表中构建一个任意长度的SafeList。相反，您想要量化存在性，这只能通过定义新的数据类型来完成：

data ASafeList a where
    ASafeList :: SafeList n a -> ASafeList a

那么你的签名应该是

fromList :: [a] -> ASafeList a

您可以通过ASafeList上的模式匹配来使用它

useList :: ASafeList a -> ...
useList (ASafeList xs) = ...

在正文中，xs 将是一个带有未知（刚性）n 的 SafeList n a 类型。您可能必须添加更多操作才能以任何重要的方式使用它。