Haskell 中 Idris 的 Fin 的首选替代方案是什么

我想要一个可以包含 0 到 n 值的类型，其中 n 位于类型级别。

我正在尝试类似的事情：

import GHC.TypeLits
import Data.Proxy

newtype FiniteNat n = FiniteNat { toInteger :: Integer }

smartConstructFiniteNat :: (KnownNat n) => Proxy n -> Integer -> Maybe (FiniteNat (Proxy n))
smartConstructFiniteNat pn i 
  | 0 <= i && i < n = Just (FiniteNat i)
  | otherwise       = Nothing
  where n = natVal pn

基本上可以工作，但不知何故并不真正令人满意。是否有一个“标准”解决方案，甚至是一个库来实现这一目标？关于依赖类型列表长度有很多争论，但我无法找到确切的东西。另外 - 我假设使用GHC.TypeLits是必要的，因为我的n可以取相当大的值，因此归纳定义可能会非常慢。

你可以直接翻译伊德里斯的Fin成通常的 Haskell 的依赖类型特征的混杂。

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

(!) :: Vec n a -> Fin n -> a
(x :> xs) ! FZ = x
(x :> xs) ! (FS f) = xs ! f

With TypeInType你甚至可以有单身人士Fins!

data Finny n (f :: Fin n) where
    FZy :: Finny (S n) FZ
    FSy :: Finny n f -> Finny (S n) (FS f)

这可以让你伪造运行时相关的量化, eg,

type family Fin2Nat n (f :: Fin n) where
    Fin2Nat (S _) FZ = Z
    Fin2Nat (S n) (FS f) = S (Fin2Nat n f)

-- tighten the upper bound on a given Fin as far as possible
tighten :: Finny n f -> Fin (S (Fin2Nat n f))
tighten FZy = FZ
tighten (FSy f) = FS (tighten f)

但是，呃，必须在值和类型级别复制所有内容，并写出所有类型变量，这有点糟糕（n）可能会变得非常乏味。

如果您确实确定需要有效的运行时表示Fin，你基本上可以做你在问题中所做的事情：填充机器Int into a newtype并使用幻像类型作为其大小。但作为库的实现者，你有责任确保Int符合界限！

newtype Fin n = Fin Int

-- fake up the constructors
fz :: Fin (S n)
fz = Fin 0
fs :: Fin n -> Fin (S n)
fs (Fin n) = Fin (n+1)

此版本缺少真正的 GADT 构造函数，因此您无法使用模式匹配来操作类型相等性。你必须自己使用unsafeCoerce。您可以为客户端提供以下形式的类型安全接口fold，但他们必须愿意以高阶风格编写所有代码，并且（因为fold是一种变形现象），一次观察多个层变得更加困难。

-- the unsafeCoerce calls assert that m ~ S n
fold :: (forall n. r n -> r (S n)) -> (forall n. r (S n)) -> Fin m -> r m
fold k z (Fin 0) = unsafeCoerce z
fold k z (Fin n) = unsafeCoerce $ k $ fold k z (Fin (n-1))

哦，你不能进行类型级计算（就像我们所做的那样）Fin2Nat上面）用这个表示Fin，因为类型级别Ints 不允许感应。

就其价值而言，伊德里斯Fin与上面的 GADT 一样效率低下。该文档包含以下警告 https://github.com/idris-lang/Idris-dev/blob/29e271c8dd6af842817156cdb17e203e401b0899/libs/base/Data/Fin.idr#L8-L9:

使用它可能不是一个好主意Fin对于算术来说，它们在运行时效率极低。

我听说伊德里斯的未来版本能够识别“Nat具有类型”风格的数据类型（例如Fin）并自动删除证明并将值打包到机器整数中，但据我所知，我们还没有做到这一点。