难以实现长度索引向量的类型安全 `at`。

huangapple go评论76阅读模式
英文:

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

问题

I have just learnt about the DataKinds extension, type-level literals, and found out that type-levels natural numbers can be compared using constraints provided in the Data.Type.Ord such as (>), and manipulated using type-level operations provided in GHC.TypeNats such as (+)).

我刚学到了DataKinds扩展、类型级别的文字,发现可以使用Data.Type.Ord提供的约束来比较类型级别的自然数,例如(>),并且可以使用GHC.TypeNats提供的类型级别操作,例如(+)

With these in mind, I came across the idea of implementing a safe version of !! for length-indexed vectors. The idea is simple: you pass in an ix :: Natural as the index, and a vec :: Vec len a with length len and type a, and you get the element at index ix. The compiler should detect and shout at you for any illegal ix (ix < 0 || ix >= len) or vec (whose len == 0).

考虑到这些,我想到了实现一个安全版本的!!用于长度索引向量的想法。这个想法很简单:你传入一个ix :: Natural作为索引,以及一个长度为len且类型为avec :: Vec len a,你会得到索引ix处的元素。编译器应该会检测到并警告你关于任何非法的ixix < 0 || ix >= len)或vec(其len == 0)。

So I began by defining the type signature for such safeAt (imports and magic comments of extensions ignored):

因此,我首先定义了这样的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

Working as intended:

按预期工作:

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

Here I made use of a proxy to hold the ix at the type-level so it can be checked by the type-level constraints. This however became a problem when I try to implement safeAt:

在这里,我使用了一个代理来在类型级别上保存ix,以便可以通过类型级别的约束进行检查。然而,当我尝试实现safeAt时,这成为了一个问题:

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

I need to promote (n - 1) to Proxy :: Proxy (n - 1). I cannot work out such function, not even writing out its type signature, and came to doubt if such a type-dependent function would even exist in the Haskell's typing system. I know you can pull down a Nat from type-level to term-level using natVal, but is there a "reverse" of this? Maybe there's a magic function out there that I don't know? Also I believe there are other problems in this implementation, such as how would you comfort the compiler that (ix - 1) is KnownNat and (len - 1) >= 1 still given the proxy p is not holding a 0. Maybe there are some alternative approaches out there to implement safeAt in a non-recursive way? I have so much confusions.

我需要将(n - 1) 提升为 Proxy :: Proxy (n - 1)。我无法编写出这样的函数,甚至无法编写出它的类型签名,因此开始怀疑在Haskell的类型系统中是否存在这样的类型相关函数。我知道你可以使用natVal将一个类型级别的Nat转换为项级别,但是否有相反的方法呢?也许有我不知道的神奇函数?此外,我认为这个实现中还存在其他问题,比如如何让编译器相信 (ix - 1)KnownNat,并且 (len - 1) >= 1 仍然成立,尽管代理 p 不包含 0。也许有一些替代方法可以以非递归方式实现 safeAt?我有很多困惑。

英文:

I have just learnt about the DataKinds extension, type-level literals, and found out that type-levels natural numbers can be compared using constraints provided in the Data.Type.Ord such as (>), and manipulated using type-level operations provided in GHC.TypeNats such as (+).

With these in mind, I came across the idea of implementing a safe version of !! for length-indexed vectors. The idea is simple: you pass in an ix :: Natural as the index, and a vec :: Vec len a with length len and type a, and you get the element at index ix. The compiler should detect and shout at you for any illegal ix (ix < 0 || ix >= len) or vec (whose len == 0).

So I began by defining the type signature for such safeAt (imports and magic comments of extensions ignored):

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

Working as intended:

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

Here I made use of a proxy to hold the ix at the type-level so it can be checked by the type-level constraints. This however became a problem when I try to implement safeAt:

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

I need to promote (n - 1) to Proxy :: Proxy (n - 1). I cannot work out such function, not even writing out its type signature, and came to doubt if such a type-dependent function would even exist in the Haskell's typing system. I know you can pull down a Nat from type-level to term-level using natVal, but is there a "reverse" of this? Maybe there's a magic function out there that I don't know? Also I believe there are other problems in this implementation, such as how would you comfort the compiler that (ix - 1) is KnownNat and (len - 1) >= 1 still given the proxy p is not holding a 0. Maybe there are some alternative approaches out there to implement safeAt in a non-recursive way? I have so much confusions.

答案1

得分: 1

代理是一种基本上已经过时的/遗留的东西,自从 -XTypeApplications-XAllowAmbiguousTypes 可用以来。 使用这些扩展与 -XScopedTypeVariables 一起使用几乎可以完成代理所能做的一切。

在许多情况下,包括你的情况下,这还不够:你需要比代理更强大的东西来传播 KnownNat 约束。单例 提供了这种能力。对于 n :: NatSing n 封装了像代理一样的 KnownNat 约束,以一种可以进行计算的方式。

引入 单例基础包(有点过分了),你可以从以下开始:

{-# 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

当然这还不是全部:如何表示这些大小约束呢?<br> 看起来 ix &lt; len 暗示着 ix-1 &lt; len-1,但这是编译器往往不同意的那种琐碎的事情。

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

...肯定有一些工作可以让这种东西顺利运行,无论是在 GHC 本身还是 singletons-presburger 插件 中,但我不确定它的运行情况。

从实用的角度来说,也许你可以选择另一种方法更好:要么

  • 不要费心进行依赖类型的递归。 相反,只需在底层使用不安全的实现,并在上面添加类型约束。在我看来,这是解决这类问题的惯用 Haskell 解决方案。当然,它不能提供与完全依赖性-总体版本相同的正确性验证水平,但如果你需要这个,那么你应该使用 Agda 或 Idris 而不是 Haskell。
  • 用 Peano 数表示它。 对这些进行归纳只是普通的模式匹配。
  • 将索引放入值级别(这可能更有用),但使用限制范围的类型。 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)
英文:

Proxies are a mostly obsolete/legacy thing since -XTypeApplications and -XAllowAmbiguousTypes have been available. Using these extensions together with -XScopedTypeVariables gives you almost everything proxies can do.

In many cases, including yours, that's not enough though: you need something stronger than proxies to propagate the KnownNat constraint. Singletons offer that capability. A Sing n for n :: Nat packs the KnownNat constraint in a value like a proxy, in a way that you can carry out computations with it.

Throwing in the big singletons-base package (kinda overkill), you can start with the following:

{-# LANGUAGE TypeApplications #-}

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

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

Of course that's not all: how do we express those size constraints?<br>It seems obvious that ix &lt; len implies ix-1 &lt; len-1, but this is the kind of trivial thing compilers tend to disagree with.

Welcome to the joy of dependently-typed programming!

...There's definitely work on getting this kind of thing behaving smoothly, both in GHC itself and the singletons-presburger plugin but I'm not sure how well it works.

Pragmatically speaking, you may be better off with a different approach: either

  • Don't bother doing dependently-typed recursion. Instead, just use an unsafe implementation underneath and add the type constraints on top. This is IMO the idiomatic Haskell solution for problems like this. Of course it doesn't offer the same correctness-verification level as a fully-dependent-total version, but if you need that then you should use Agda or Idris instead of Haskell.
  • Express it with Peano numbers. Induction over these is just ordinary pattern matching.
  • Put the indexing into the value level (which is probably more useful anyway), but with a range-limited type. finite-typelits offers that.

In the first version, you don't need any proxies or singletons. This will do:

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

unsafeAt :: Integer -&gt; Vec len a -&gt; a
unsafeAt = ...

safeAt :: ∀ ix len a . (KnownNat len, KnownNat ix, ix &gt;= 0, ix &lt; len)
  =&gt; Vec len a -&gt; a
safeAt = unsafeAt (natVal @ix Proxy)

huangapple
  • 本文由 发表于 2023年5月20日 21:01:37
  • 转载请务必保留本文链接:https://go.coder-hub.com/76295368.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定