相关疑难解决方法(0)

我正在试验Haskell中的从属类型,并在"单身人士"包的文章中遇到以下内容:

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 …