haskell - Haskell单例:排版包

Question

我很难说服编译器我的类型是正确的。定期
具有Nat和Zero构造函数的Succ很简单（目标是为长度索引列表（replicate）编写Vect函数）：

replicate' :: SNat n -> a -> Vect n a
replicate' SZero _ = Nil
replicate' (SSucc n) a = a :> replicate' n a

但是常规的 Nat非常慢。

因此，在单例库中有一个镜像GHC.TypeLits的程序包，可以使Nats更快。
但是我无法使上面的示例适用于它：

sameNat :: forall a b. (KnownNat a, KnownNat b) => SNat a -> SNat b -> Maybe (a :~: b)
sameNat x y
  | natVal (Proxy :: Proxy a) == natVal (Proxy :: Proxy b) = Just (unsafeCoerce Refl)
  | otherwise            = Nothing

replicate'' :: (KnownNat n) => SNat n -> a -> Vect n a
replicate'' n a =
  case sameNat n (sing :: Sing 0) of
    Just Refl -> Nil
    Nothing   -> a ::> replicate'' (sPred n) a

这不会在最后一行进行类型检查：

Couldn't match type ‘n’
                     with ‘(n GHC.TypeNats.- 1) GHC.TypeNats.+ 1’

Answer 1

问题是，在n为零的情况下（当在sameNat n (sing :: Sing 0)上进行模式匹配时），n ~ 0为您提供了可用的Just Refl证明，但是如果n不为零，则仅为您提供Nothing。这完全没有告诉您有关n的任何信息，因此就类型检查器而言，您可以在Nothing分支内完全调用相同的东西集，而无需首先调用sameNat （特别是，您不能使用sPred，因为这需要该1 <= n）。

因此，我们需要对提供n ~ 0证据或1 <= n证据的事物进行模式匹配。像这样：

data IsZero (n :: Nat)
  where Zero :: (0 ~ n) => IsZero n
        NonZero :: (1 <= n) => IsZero n
deriving instance Show (IsZero n)

然后我们可以这样写 replicate''：

isZero :: forall n. SNat n -> IsZero n
isZero n = _

replicate'' :: SNat n -> a -> Vect n a
replicate'' n x = case isZero n
                    of Zero -> Nil
                       NonZero -> x ::> replicate'' (sPred n) x

当然，这只是将问题转移到实现 isZero函数上，该函数实际上并没有给我们买任何东西，但是我会坚持使用它，因为将其作为您想要的任何其他归纳定义的基础很方便使用 Nat进行。

因此，实现 isZero。我们当然可以用 sameNat处理零大小写，但这无助于非零大小写。单例包还提供了 Data.Singletons.Decide，它为您提供了一种基于单例来证明类型相等或不相等的方法。因此，我们可以这样做：

isZero :: forall n. SNat n -> IsZero n
isZero n = case n %~ (SNat @0)
             of Proved Refl -> Zero
                Disproved nonsense -> NonZero

可悲的是，这也不起作用！ Proved的情况很好（基本上与 sameNat赋予我们 Just Refl相同）。但是“不等式的证明”以 nonsense绑定到类型为 (n :~: 0) -> Void的函数的形式出现，并且如果我们假设全部（没有假名），则该函数的存在“证明”我们不能构造一个 n :~: 0值，该值证明 n绝对不是 0。但这与 1 <= n的证明相距太远。我们可以看到，如果 n不为0，那么从自然数的属性来看，它必须至少为1，但是GHC不知道这一点。

另一种方法是在 Ord上使用单例的 SNat @1 :%<= n支持和模式匹配：

isZero :: forall n. SNat n -> IsZero n
isZero n = case (SNat @1) %:<= n
             of STrue -> NonZero
                SFalse -> Zero

但这也不起作用，因为 STrue和 SFalse只是类型级别 True和 False的单例，与原始比较断开了连接。我们从任一方面都没有得到 0 ~ n或 1 <= n的证据（同样，通过与 SNat @0进行比较，也无法使其起作用）。基本上，这是类型检查器布尔盲。

最终，我无法在代码中令人满意地解决此问题。据我所知，我们缺少一个原语。我们要么需要能够以对相应类型赋予 <或 <=约束的方式比较单身人士，要么需要切换 Nat为零还是非零。

所以我作弊：

isZero :: forall n. SNat n -> IsZero n
isZero n = case n %~ (SNat @0)
             of Proved Refl -> Zero
                Disproved _ -> unsafeCoerce (NonZero @1)

由于 NonZero仅包含 n为1或更大的证据，而没有包含有关 n的任何其他信息，因此您可以不安全地强制使用1为1或更大的证据。

这是一个完整的工作示例：

{-# LANGUAGE DataKinds
           , GADTs
           , KindSignatures
           , ScopedTypeVariables
           , StandaloneDeriving
           , TypeApplications
           , TypeOperators
  #-}

import GHC.TypeLits ( type (<=), type (-) )
import Data.Singletons.TypeLits ( Sing (SNat), SNat, Nat )
import Data.Singletons.Prelude.Enum ( sPred )
import Data.Singletons.Decide ( SDecide ((%~))
                              , Decision (Proved, Disproved)
                              , (:~:) (Refl)
                              )
import Unsafe.Coerce ( unsafeCoerce )

data IsZero (n :: Nat)
  where Zero :: (0 ~ n) => IsZero n
        NonZero :: (1 <= n) => IsZero n
deriving instance Show (IsZero n)

isZero :: forall n. SNat n -> IsZero n
isZero n = case n %~ (SNat @0)
             of Proved Refl -> Zero
                Disproved _ -> unsafeCoerce (NonZero @1)


data Vect (n :: Nat) a
  where Nil :: Vect 0 a
        (::>) :: a -> Vect (n - 1) a -> Vect n a
deriving instance Show a => Show (Vect n a)

replicate'' :: SNat n -> a -> Vect n a
replicate'' n x = case isZero n
                    of Zero -> Nil
                       NonZero -> x ::> replicate'' (sPred n) x

head'' :: (1 <= n) => Vect n a -> a
head'' (x ::> _) = x

main :: IO ()
main = putStrLn
     . (:[])
     . head''
     $ replicate''
         (SNat @1000000000000000000000000000000000000000000000000000000)
         '\x1f60e'

请注意，与KA Buhr建议的使用 unsafeCoerce的方法不同，此处的复制代码实际上是使用类型检查器来验证其是否根据提供的 Vect n a构造了 SNat n，而他们的建议则要求您信任代码执行此操作（实际工作的实质是通过 iterate依靠 Int来完成），并且仅确保调用者一致地使用 SNat n和 Vect n a。您只需信任的唯一代码（未经编译器检查）是 Refuted _ :: Decision (n :~: 0)确实在 1 <= n内暗示了 isZero（您可以重复使用它们来编写许多其他功能，这些功能需要打开或关闭） SNat是否为零）。

当您尝试使用 Vect实现更多功能时，您会发现GHC对 Nat属性不了解的许多“显而易见的”东西是很痛苦的。 Data.Constraint.Nat包中的 constraints有很多有用的证明可供您使用（例如，如果您尝试实现 drop :: (k <= n) => SNat k -> Vect n a -> Vect (n - k) a，则可能最终需要 leTrans，这样当您知道 1 <= k然后也可以 1 <= n进行模式匹配以剥离另一个元素）。 K. A. Buhr的方法可以避免此类杂乱无章，这对您很有帮助，如果您只想使用您信任的代码来实现您的操作，并且不安全地强制要排队的类型。