haskell - 如何解构 SNat(单例)

Question

我正在使用 Haskell 中的依赖类型进行试验，并在 paper 中遇到以下情况“单例”套餐:

replicate2 :: forall n a. SingI n => a -> Vec a n
replicate2 a = case (sing :: Sing n) of
  SZero -> VNil
  SSucc _ -> VCons a (replicate2 a)

所以我尝试自己实现这个，只是为了了解它是如何工作的:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

import           Data.Singletons
import           Data.Singletons.Prelude
import           Data.Singletons.TypeLits

data V :: Nat -> * -> * where
  Nil  :: V 0 a
  (:>) :: a -> V n a -> V (n :+ 1) a

infixr 5 :>

replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
  where replicateV' :: Sing n -> a -> V n a
        replicateV' sn a = case sn of
            SNat -> undefined -- what can I do with this?

现在的问题是 Sing Nat 的实例没有 SZero或 SSucc .只有一个构造函数叫做 SNat .

> :info Sing
data instance Sing n where
  SNat :: KnownNat n => Sing n

这与其他允许匹配的单例不同，例如 STrue和 SFalse ，例如在以下(无用的)示例中:

data Foo :: Bool -> * -> * where
  T :: a -> Foo True a
  F :: a -> Foo False a

foo :: forall a b. SingI b => a -> Foo b a
foo a = case (sing :: Sing b) of
  STrue -> T a
  SFalse -> F a

您可以使用 fromSing获取基本类型，但这当然允许 GHC 检查输出向量的类型:

-- does not typecheck
replicateV2 :: SingI n => a -> V n a
replicateV2 = replicateV' sing
  where replicateV' :: Sing n -> a -> V n a
        replicateV' sn a = case fromSing sn of
              0 -> Nil
              n -> a :> replicateV2 a

所以我的问题是:如何实现 replicateV ?

编辑

erisco 给出的答案解释了为什么我解构 SNat 的方法不起作用。但即使使用 type-natural库，我无法实现 replicateV对于 V数据类型 使用 GHC 的内置 Nat类型 .

例如下面的代码编译:

replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
  where replicateV' :: Sing n -> a -> V n a
        replicateV' sn a = case TN.sToPeano sn of
            TN.SZ       -> undefined
            (TN.SS sn') -> undefined

但这似乎并没有为编译器提供足够的信息来推断 n是 0或不。例如，以下给出了编译器错误:

replicateV :: SingI n => a -> V n a
replicateV = replicateV' sing
  where replicateV' :: Sing n -> a -> V n a
        replicateV' sn a = case TN.sToPeano sn of
            TN.SZ       -> Nil
            (TN.SS sn') -> undefined

这给出了以下错误:

src/Vec.hs:25:28: error:
    • Could not deduce: n1 ~ 0
      from the context: TN.ToPeano n1 ~ 'TN.Z
        bound by a pattern with constructor:
                   TN.SZ :: forall (z0 :: TN.Nat). z0 ~ 'TN.Z => Sing z0,
                 in a case alternative
        at src/Vec.hs:25:13-17
      ‘n1’ is a rigid type variable bound by
        the type signature for:
          replicateV' :: forall (n1 :: Nat) a1. Sing n1 -> a1 -> V n1 a1
        at src/Vec.hs:23:24
      Expected type: V n1 a1
        Actual type: V 0 a1
    • In the expression: Nil
      In a case alternative: TN.SZ -> Nil
      In the expression:
        case TN.sToPeano sn of {
          TN.SZ -> Nil
          (TN.SS sn') -> undefined }
    • Relevant bindings include
        sn :: Sing n1 (bound at src/Vec.hs:24:21)
        replicateV' :: Sing n1 -> a1 -> V n1 a1 (bound at src/Vec.hs:24:9)

所以，我原来的问题仍然存在，我仍然无法对 SNat 做任何有用的事情.

Answer 1

这里有两个自然的概念。一种是“literal naturals”(即 0、1、2 等)，另一种是“Peano naturals”(即 Z、S Z、S (S Z) 等)。论文使用的显然是 Peano naturals，但单例使用的是字面自然。

值得庆幸的是，还有一个名为 type-natural 的包。它定义了 Peano naturals 以及 conversion to literal naturals和 conversion from literal naturals .