Haskell :: 如何创建任意长度的向量？答案

【问题标题】：Haskell :: How do I create a Vector of arbitrary length?Haskell :: 如何创建任意长度的向量？
【发布时间】：2022-02-18 17:08:24
【问题描述】：

想在 Haskell 中实现类型安全的矩阵乘法。定义如下：

{-# LANGUAGE TypeFamilies, DataKinds, GADTs  #-}
module Vector where

data Nat = Succ Nat | Zero

data Vector (n :: Nat) a where
    Nil :: Vector 'Zero a
    (:::) :: a -> Vector n a -> Vector (Succ n) a
type Matrix n m a = Vector m (Vector n a)

instance Foldable (Vector n) where
    foldr f b (a ::: as) = f a (foldr f b as)
    foldr _ b Nil = b

instance Functor (Vector n) where
    fmap f (x ::: xs) = f x ::: fmap f xs
    fmap _ Nil = Nil

zipV :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
zipV f (a ::: as) (b ::: bs) = f a b ::: zipV f as bs
zipV f Nil Nil = Nil

终于有实现的需要

transpose :: Matrix n m a -> Matrix m n a

但我在 Haskell 中能做的最好的事情是：

transpose :: Matrix n (Succ m) a -> Matrix (Succ m) n a
transpose (h ::: rest@(_ ::: _)) = zipV (:::) h (transpose rest)
transpose (h ::: Nil) = fmap (::: Nil) h

因为我无法实现，所以限制为 m > 0

nils :: {n :: Nat} -> Vector n (Vector Zero a)

改用 Idris 只是为了练习并且做得更好：

matrix : Nat -> Nat -> Type -> Type
matrix n m a = Vector n (Vector m a)

nils : {n: Nat} -> Vector n (Vector Z a)
nils {n = Z}   = Nil
nils {n = S k} = Nil ::: nils

transpose : matrix n m a -> matrix m n a
transpose (h ::: rest) = zipV (:::) h (transpose rest)
transpose Nil = nils

我有实现 nils 的冲动，但是 Haskell 中的类型级编程很尴尬。我还必须在 Haskell 中对 rest@(_ ::: _) 进行模式匹配，但我在 Idris 中没有。如何实现“nil”？

【问题讨论】：

我认为这是不可行的。在 Haskell 中，类型被擦除，因此从 Vector n t 恢复 n 的唯一方法是模式匹配此类向量类型的某些值。当您只有Vector 0 (Vector n t) 类型的值时，这是一个问题。解决此问题的一种方法是将singleton 存储在矩阵类型中，例如Matrix n m a = (Sing n, Vector m (Vector n a))。否则，需要将单例作为 transpose 中的参数。

标签： haskell vector polymorphism dependent-type type-level-computation

【解决方案1】：

这基本上就是singletons 的用途。这是一个类型类的价值级别见证，它使您可以访问这个（概念上是冗余的）信息，每个数字实际上都可以用标准形式来描述。一个最小的实现：

data NatSing n where
  ZeroSing :: NatSing Zero
  SuccSing :: KnownNat n => NatSing (Succ n)

class KnownNat n where
  natSing :: NatSing n
instance KnownNat Zero where natSing = ZeroSing
instance KnownNat n => KnownNat (Succ n) where natSing = SuccSing

现在可以写了

{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}
nils :: ∀ n a . KnownNat n => Vector n (Vector Zero a)
nils = case natSing @n of
  ZeroSing ->     Nil
  SuccSing -> Nil ::: nils

【讨论】：