How to deconstruct an SNat (singletons)

Question

I am experimenting with depedent types in Haskell and came across the following in the paper of the 'singletons' package:

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

So I tried to implement this myself, just toget a feel of how it works:

{-# 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?

Now the problem is that the Sing instance for Nat does not have SZero or SSucc. There is only one constructor called SNat.

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

This is different than other singletons that allow matching, such as STrue and SFalse, such as in the following (useless) example:

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

You can use fromSing to get a base type, but this of course does allow GHC to check the type of the output vector:

-- 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

So my question: how to implement replicateV?

EDIT

The answer given by erisco explains why my approach of deconstructing an SNat does not work. But even with the type-natural library, I am unable to implement replicateV for the V data type using GHC's build-in Nat types.

For example the following code compiles:

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

But this does not seem to give enough information to the compiler to infer whether n is 0 or not. For example the following gives a compiler error:

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

This gives the following error:

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)

So, my original problem still remains, I am still unable to do anything usefull with the SNat.

Answer 1

There are two notions of naturals at play here. One is "literal naturals" (i.e. 0, 1, 2, and so on) and the other is "Peano naturals" (i.e. Z, S Z, S (S Z), and so on). The one the paper is using is clearly Peano naturals but the one singletons uses is literal naturals.

Thankfully there is another package called type-natural which defines Peano naturals as well as conversion to literal naturals and conversion from literal naturals.

Answer 2

From the comments, I'm worried I must be missing something terrifically obvious, but here's my take on it. The whole point of:

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

is that, in order to return VNil :: Vec a 0 when the function has general return type Vec a n, you need to specialize the n to 0, and pattern-matching on GADTs provides a way to do this, as long as you have a constructor, like SZero, that implies n ~ 0.

Now the SNats in the singleton package have no such constructor. The only way to get one, as far as I can see, is to build a whole new singleton type for naturals and implement the necessary type families. Maybe you can do it in a way that wraps the Nats, so you're closer to SZero :: Sing (SN 0), SNonZero :: Sing (SN n) than a Peano construction, but I don't know.

Of course, there's another way to specialize a function that returns Vec a n to return Vec a 0, namely type classes.

If you are willing to abandon some of the explicit singleton machinery and switch to type classes (and also allow overlapping and undecidable instances), the following seems to work. I had to slightly modify the definition of V to use n :- 1 instead of n :+ 1, but I don't think that poses a problem.

{-# 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)