尝试为长度索引向量实现类型安全的“at”时遇到困难-解网

问：

我刚刚了解了扩展，类型级文字，并发现可以使用中提供的约束来比较类型级别的自然数，并使用中提供的类型级操作进行操作。DataKindsData.Type.Ord(>)GHC.TypeNats(+)

考虑到这些，我萌生了实现长度索引向量的安全版本的想法。这个想法很简单：你传入一个作为索引，一个有长度和类型，然后你得到索引处的元素。编译器应该检测并大声喊叫任何非法（）或（其）。!!ix :: Naturalvec :: Vec len alenaixixix < 0 || ix >= lenveclen == 0

因此，我首先定义了此类类型的签名（忽略扩展的导入和魔术注释）：safeAt

infixr 5 :.
data Vec :: Nat -> * -> * where
  Nil :: Vec 0 a
  (:.) :: a -> Vec m a -> Vec (m + 1) a

safeAt :: forall (ix :: Nat) (len :: Nat) (proxy :: Nat -> *) a.
            (KnownNat ix, {- ix >= 0, -} len >= 1, ix < len) =>
              proxy ix -> Vec len a -> a
safeAt = undefined

按预期工作：

v :: Vec 10 Int
v = 1 :. 2 :. 3 :. 4 :. 5 :. 6 :. 7 :. 8 :. 9 :. 10 :. Nil

ok :: Int
ok = safeAt (Proxy :: Proxy 3) v

oops :: Int
oops = safeAt (Proxy :: Proxy 10) v  -- expected compilation error

在这里，我使用了一个代理来保存类型级别的，以便可以通过类型级别的约束来检查它。然而，当我尝试实现以下内容时，这成为一个问题：ixsafeAt

safeAt p (x:.xs) = case natVal p of
                     0 -> x
                     n -> safeAt (??? (n - 1)) xs

我需要晋升到 .我无法计算出这样的函数，甚至没有写出它的类型签名，并且开始怀疑这样的类型依赖函数是否存在于 Haskell 的类型系统中。我知道您可以使用将 Nat 从类型级别拉到术语级别，但是有“反面”吗？也许那里有一个我不知道的神奇功能？此外，我相信此实现中还有其他问题，例如您如何安慰编译器，并且仍然给定代理不持有 .也许有一些替代方法可以以非递归方式实现？我有很多困惑。(n - 1)Proxy :: Proxy (n - 1)natVal(ix - 1)KnownNat(len - 1) >= 1p0safeAt

Haskell 矢量型安全 VEC

{-# LANGUAGE TypeApplications #-}

import Prelude.Singletons (SNum(..), sing)
import Data.Kind (Type)

safeAt :: forall (ix :: Nat) (len :: Nat) a.
              Sing ix -> Vec len a -> a
safeAt i (x:.xs) = case fromSing i of
                     0 -> x
                     _ -> safeAt (i %- sing @1) xs

当然，这还不是全部：我们如何表达这些尺寸限制？
这似乎很明显，但这是编译器倾向于不同意的琐碎事情。ix < lenix-1 < len-1

欢迎来到依赖类型编程的乐趣！

...无论是在 GHC 本身还是在 singletons-presburger 插件中，肯定都有努力让这种事情顺利运行，但我不确定它的效果如何。

从实用的角度来说，你最好采用不同的方法：要么

不要费心去做依赖类型的递归。相反，只需在下面使用不安全的实现，并在顶部添加类型约束。这是 IMO 针对此类问题的惯用 Haskell 解决方案。当然，它没有提供与完全依赖总版本相同的正确性验证级别，但如果您需要，则应使用 Agda 或 Idris 而不是 Haskell。
用皮亚诺数字表示。对这些的归纳只是普通的模式匹配。
将索引放入值级别（无论如何这可能更有用），但使用范围限制类型。Finite-TypeLits 提供了这一点。

在第一个版本中，您不需要任何代理或单例。这将执行以下操作：

{-# LANGUAGE ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes #-}

unsafeAt :: Integer -> Vec len a -> a
unsafeAt = ...

safeAt :: ∀ ix len a . (KnownNat len, KnownNat ix, ix >= 0, ix < len)
  => Vec len a -> a
safeAt = unsafeAt (natVal @ix Proxy)

尝试为长度索引向量实现类型安全的“at”时遇到困难

Difficulty in trying to implement a type-safe `at` for length-indexed vectors

评论

评论