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

Question

我正在尝试编写一个函数

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

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

这些向量定义如下:

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不受样板被过多打扰(不是灾难性的样板量虽然,实现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构造的实例.