haskell - Haskell 中 Idris 的 Fin 的首选替代品是什么

Question

我想要一个可以包含值 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可以取相当大的值，所以归纳定义可能会很慢。

Answer 1

可以直接翻译 idris 的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

与 TypeInType你甚至可以拥有单例 Fin !

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

这允许您在运行时的东西上伪造依赖量化，例如，

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变成 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 的形式为客户端提供类型安全的接口(interface)。 ，但他们必须愿意以高阶风格编写所有代码，并且(因为 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 所做的那样)。 , 因为类型级别 Int s 不允许感应。

对于它的值(value)， idris 的 Fin与上面的 GADT 一样低效。文档包含 the following caveat :

It's probably not a good idea to use Fin for arithmetic, and they will be exceedingly inefficient at run time.

我听说过关于 Idris 的 future 版本能够发现“ Nat 与类型”风格的数据类型(如 Fin )并自动删除证明并将值打包成机器整数的噪音，但据我所知我们还没有。