(类型)安全地检索向量的元素

Question

我正在尝试编写一个函数

getColumn :: Int -> Vector n e -> e

它从大小为n的向量中检索I‘the项。

这些向量的定义如下：

data Natural where
  Zero :: Natural
  Succ :: Natural -> Natural

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two
type Four  = Succ Three

data Vector n e where
  Nil  :: Vector Zero e
  (:|) :: e -> Vector n e -> Vector (Succ n) e

infixr :|

在编写getColumn函数时，如果Int太大而Vector太大，编译器会拒绝代码吗？

我将如何编写这个函数？

Answer 1

首先，我们需要一种单一的自然类型。单例是类型级别数据的运行时表示，它们被称为单例类型，因为它们每个只有一个值。这很有用，因为它在值和表示类型之间建立了一对一的对应关系；只要知道类型或值，就可以推断出另一个类型。

这也使我们能够避免Haskell类型不能依赖Haskell值的限制:我们的类型将依赖于单个实例的类型索引，但是该类型索引可以由单个实例的值确定。在完全依赖的编程语言(如Agda或Idris )中，这种曲折的迂回并不存在，在这些语言中，类型可以依赖于值。

data SNatural (n :: Natural) where
    SZero :: SNatural Zero
    SSucc :: SNatural n -> SNatural (Succ n) 

deriving instance Show (SNatural n) -- requires StandaloneDeriving

我们可以看到，对于任何n，SNatural n只有一个可能的值；它只是反映了原始的Natural定义。

我们可以采用多种方法进行矢量索引。

1.直接定义<约束。

在自然状态下定义<很简单：

{-# LANGUAGE TypeOperators, TypeFamilies #-}

type family a < b where 
    Zero   < Succ b = True
    a      < Zero   = False
    Succ a < Succ b = a < b  

现在，我们可以用类型相等约束来表示有界性：

index :: ((m < n) ~ True) => Vector n a -> SNatural m -> a
index (x :| xs) SZero     = x 
index (x :| xs) (SSucc i) = index xs i
index _         _         = error "impossible"

main = do
    print $ index (0 :| 1 :| Nil) SZero -- 0
    print $ index (0 :| 1 :| Nil) (SSucc (SSucc SZero)) -- type error 

2.使用有界自然的替代表示法。

这是依赖类型编程的标准解决方案，而IMO则是更简单的解决方案，尽管一开始它更难理解。我们称有界自然类型为Fin n (表示“有限”)，其中n是表示上界的自然形式。诀窍是对我们的数字进行索引，使值的大小不能大于索引。

data Fin (n :: Natural) where
    FZero :: Fin (Succ n)
    FSucc :: Fin n -> Fin (Succ n) 

很明显，Fin Zero没有任何价值。Fin (Succ Zero)只有一个值，FZero，Fin (Succ (Succ Zero))有两个值，因此Fin n总是有n可能的值。我们可以将它直接用于安全索引：

index :: Vector n a -> Fin n -> a
index (x :| xs) FZero     = x
index (x :| xs) (FSucc i) = index xs i
index _         _         = error "impossible" 

main = do
    print $ index (0 :| 1 :| Nil) (FSucc (FSucc FZero)) -- type error

增编:使用singletons库并由Int-s进行安全索引。

正如我们所看到的，在Haskell中进行依赖编程需要大量的样板。类型级别的数据和它们的单级数据或多或少是相同的，但仍然需要单独的定义。对它们进行操作的功能也必须类似地重复。幸运的是，singletons包可以为我们生成样板：

{-# LANGUAGE 
    TypeFamilies, GADTs, DataKinds, PolyKinds,
    ScopedTypeVariables, TemplateHaskell #-}

import Data.Singletons.TH

-- We get the "SNat n" singleton generated too. 
$(singletons[d| data Nat = Z | S Nat |])

data Vector n e where
  Nil  :: Vector Z e
  (:|) :: e -> Vector n e -> Vector (S n) e
infixr :|

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

index :: Vector n a -> Fin n -> a
index (x :| xs) FZ     = x
index (x :| xs) (FS i) = index xs i
index _         _      = error "impossible"

该包还包括根据需要从类型生成单例值的方便方法：

foo :: SNat (S (S (S Z)))
foo = sing

sing是一个多态值，可以作为任何单例值的替代值。有时，可以从上下文中推断出正确的值，但其他时候，我们必须注释其类型索引，通常使用ScopedTypeVariables扩展。

现在，我们还可以安全地使用Int-s进行索引，而不会被样板过多所困扰(不过，不是灾难性的样板；手工为Nat实现sing需要多一个类型和几个实例)。

一般来说，经过验证的编程不是关于验证数据编译时间(正如我们在上面的示例中所看到的)，而是编写以一种可证明正确的方式操作的函数，即使是在未知编译时间的数据上(如果验证函数是正确的，您可以说在验证数据时它是不相关的)。我们的index可以被看作是一个半验证的函数，因为不可能实现一个错误抛出版本的类型(模块底部和散度)。

为了安全地由Int-s进行索引，我们只需编写一个从Int到Fin的经过验证的转换函数，然后像往常一样使用index：

checkBound :: Int -> SNat n -> Maybe (Fin n)
checkBound i _ | i < 0 = Nothing
checkBound 0 (SS _)    = Just FZ
checkBound i SZ        = Nothing
checkBound i (SS n)    = case checkBound (i - 1) n of
    Just n -> Just (FS n)
    Nothing -> Nothing

同样，checkBound的神奇之处在于，不可能编写返回违反给定绑定的Fin的定义。

indexInt :: forall n a . SingI n => Vector n a -> Int -> Maybe a
indexInt v i = case checkBound i (sing :: SNat n) of
    Just i  -> Just (index v i)
    Nothing -> Nothing

在这里，我们需要使用一些singletons机制：SingI约束允许我们使用sing调用一个适当的单例值。它是一个无害的类约束，因为通过构造，每个可能的n都是SingI的一个实例。