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