如何解构 SNat（单例）

Question

我正在 Haskell 中试验相关类型，并在 'singletons' 包的 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?

现在的问题是 Nat 的 Sing 实例没有 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 的内置 Nat 类型为 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

这里有两种自然概念。一种是 "literal naturals"（即 0、1、2 等），另一种是 "Peano naturals"（即 Z、S Z、S (S Z) 等）。这篇论文使用的显然是 Peano naturals，但 singletons 使用的是 literal naturals。

谢天谢地还有另一个包叫 type-natural which defines Peano naturals as well as conversion to literal naturals and conversion from literal naturals。

Answer 2

从评论中，我担心我一定遗漏了一些非常明显的东西，但这是我的看法。整点：

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

是，为了return VNil :: Vec a 0 当函数具有通用return 类型Vec a n 时，您需要将n 专门化为0，并且 GADT 上的模式匹配提供了一种方法来执行此操作，只要您有一个构造函数，例如 SZero，这意味着 n ~ 0.

现在单例包中的SNat没有这样的构造函数。据我所知，获得一个的唯一方法是为 naturals 构建一个全新的单例类型并实现必要的类型族。也许你可以用包裹 Nat 的方式来做，所以你比 Peano 结构更接近 SZero :: Sing (SN 0)、SNonZero :: Sing (SN n)，但我不知道。

当然，还有另一种方法可以将returns Vec a n 特化为return 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)

如何解构 SNat（单例）

How to deconstruct an SNat (singletons)

haskell

singleton

type-theory