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

Question

我正在尝试编写一个函数

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

从大小为 n 的向量中检索第 i 个项目.

这些向量定义如下:

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只有一个可能的值；它只是反射(reflect)了原始 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 package 可以为我们生成样板:

{-# 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 而不会受到样板的过多困扰(虽然不是灾难性的样板数量；手动为 sing 实现 Nat 需要一个更多的类型类和几个实例)。

一般来说，经过验证的编程不是验证数据编译时间(正如我们在上面的示例中看到的那样)，而是编写以可证明正确的方式运行的函数，即使是在编译时未知的数据上(你可以说只要验证函数正确，当我们验证数据时它是无关紧要的)。我们的 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 的一个实例，通过 build 。