如何解构SNat (单数)

Question

我正在Haskell中尝试使用depedent，并在'singletons‘包的纸中发现了以下内容：

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?

现在的问题是Nat的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库，我也无法使用GHC的内置type-natural replicateV types为V数据类型实现replicateV。

例如，以下代码编译：

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

从这些评论中，我担心我一定是错过了一些非常明显的东西，但下面是我的看法。全部要点是：

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

为了在函数具有通用返回类型VNil :: Vec a 0时返回Vec a n，需要将n指定为0，而GADT上的模式匹配提供了一种实现此功能的方法，只要您有一个构造函数(如SZero )，这就意味着n ~ 0。

现在，单例包中的SNat没有这样的构造函数。据我所见，唯一的方法是为自然物种建立一种全新的独生子女类型，并实现必要的类型家庭。也许你可以用一种封装Nat的方式来做，所以你更接近SZero :: Sing (SN 0)，SNonZero :: Sing (SN n)，而不是Peano结构，但我不知道。

当然，还有一种方法可以专门化返回Vec a n以返回Vec a 0的函数，即类型类。

如果您愿意放弃一些显式的单例机器，转而使用类型类(还允许重叠和不可判定的实例)，那么下面的方法似乎是可行的。我不得不稍微修改V的定义，以使用n :- 1而不是n :+ 1，但我不认为这会带来问题。

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

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE OverlappingInstances  #-}
{-# LANGUAGE UndecidableInstances  #-}

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

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

infixr 5 :>

class VC n a where
  replicateV :: a -> V n a

instance VC 0 a where
  replicateV _ = Nil

instance VC (n :- 1) a => VC n a where
  replicateV x = x :> replicateV x

instance (Show a) => Show (V n a) where
  show Nil = "Nil"
  show (x :> v) = show x ++ " :> " ++ show v

headV :: V (n :+ 1) a -> a
headV (x :> _) = x

tailV :: ((n :+ 1) :- 1) ~ n => V (n :+ 1) a -> V n a
tailV (_ :> v) = v

main = do print (replicateV False   :: V 0 Bool)
          print (replicateV 1       :: V 1 Int)
          print (replicateV "Three" :: V 3 String)

Answer 2

这里有两个自然主义的概念。一种是“字面自然”(即0，1，2等)，另一种是"Peano自然“(即Z，S Z，S (S Z)等)。纸上使用的显然是Peano自然词，但是单字人使用的是字面自然词。

谢天谢地，还有一个名为类型-自然的包，它定义了Peano自然以及向文字自然的转换和从文字自然的转换。