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，您甚至可以拥有单身Fins！

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 的形式为客户提供类型安全的接口，但他们必须愿意以高阶样式编写所有代码，并且（因为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))

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

不管怎样，Idris 的Fin 与上面的 GADT 一样低效。文档包含the following caveat：

将Fin 用于算术可能不是一个好主意，而且它们在运行时效率极低。

我听说 Idris 的未来版本能够识别“Nat with types”风格的数据类型（如Fin）并自动擦除证明并将值打包成机器整数，但目前为止我知道我们还没有。

Answer 2

rampion suggested 模式同义词，我同意，但无可否认，弄清楚如何正确构建它们的签名并不是一件容易的事。因此我想我会写一个正确的答案来给出完整的代码。

首先，通常的样板：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}

module FakeFin (Nat (..), Fin (FZ, FS), FinView (..), viewFin) where
import Numeric.Natural
import Unsafe.Coerce

现在是基本类型：

data Nat = Z | S Nat

-- Fin *must* be exported abstractly (or placed in an Unsafe
-- module). Users can use its constructor to implement
-- unsafeCoerce!
newtype Fin (n :: Nat) = Fin Natural
deriving instance Show (Fin n)

通过视图类型而不是直接工作要容易得多，所以让我们定义一个：

data FinView n where
  VZ :: FinView ('S n)
  VS :: !(Fin n) -> FinView ('S n)
deriving instance Show (FinView n)

重要的是要注意，我们可以使用显式等式约束来定义FinView，因为我们必须用这些术语来思考才能给出正确的模式签名：

data FinView n where
  VZ :: n ~ 'S m => FinView n
  VS :: n ~ 'S m => !(Fin m) -> FinView n

现在实际的视图函数：

viewFin :: Fin n -> FinView n
viewFin (Fin 0) = unsafeCoerce VZ
viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))

模式签名精确地反映了FinView 构造函数的签名。

pattern FZ :: () => n ~ 'S m => Fin n
pattern FZ <- (viewFin -> VZ) where
  FZ = Fin 0

pattern FS :: () => n ~ 'S m => Fin m -> Fin n
pattern FS m <- (viewFin -> VS m) where
  FS (Fin m) = Fin (1 + m)

-- Let GHC know that users need only match on `FZ` and `FS`.
-- This pragma only works for GHC 8.2 (and presumably future
-- versions).
{-# COMPLETE FZ, FS #-}

---

为了完整起见（因为我写这个比我预期的要花更多的精力），如果这个模块不小心导出了Fin 数据构造函数，这里有一种写unsafeCoerce 的方法。我想可能有更简单的方法。

import Data.Type.Equality

type family YahF n a b where
  YahF 'Z a _ = a
  YahF _ _ b = b

newtype Yah n a b = Yah (YahF n a b)

{-# NOINLINE finZBad #-}
finZBad :: 'Z :~: n -> Fin n -> a -> b
finZBad pf q =
  case q of
    FZ -> blah (trans pf Refl)
    FS _ -> blah (trans pf Refl)
  where
    blah :: forall a b m. 'Z :~: 'S m -> a -> b
    blah pf2 a = getB pf2 (Yah a)

    {-# NOINLINE getB #-}
    getB :: n :~: 'S m -> Yah n a b -> b
    getB Refl (Yah b) = b

myUnsafeCoerce :: a -> b
myUnsafeCoerce = finZBad Refl (Fin 0)

finZBad 是所有动作发生的地方，但它并没有做任何不恰当的事情！如果有人真的给了我们一个 Fin 'Z 类型的非底部值，那么就已经出现了严重错误。这里明确的类型相等性证据是必要的，因为如果 GHC 看到代码需要'Z ~ 'S m，它会直接拒绝它； GHC 并不真正喜欢约束中的假设推理。 NOINLINE 注释是必要的，因为 GHC 的简化器本身使用类型信息；处理它非常了解的事物的证据是不可能的，这会使它非常困惑，并产生极其武断的结果。所以我们把它屏蔽了，成功实现了The Evil Function。