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
.
Nat
type. The impossibility of proving things like(n + 1) - 1 ~ n
, as well as the awkwardness around checking ifn ~ 0
.replicateV2
is a fundamentally recursive operation for which you need induction over the vector length. Without having an inductive definition forNat
you go nowhere. Let me make this explicit: any solution to your problem will have to use something that bypasses the type system (either via a plugin orunsafeCoerce
). On the other hand, you can do everything safely and easily withdata Nat = Z | S Nat
. – Alec Sep 29 '17 at 7:55unsafeCoerce
. – Sam De Meyer Sep 29 '17 at 14:02Nat
is that some of the libraries I am using also use the built-inNat
types. EspeciallyNumeric.LinearAlgebra.Static
fromhmatrix
. I am constantly encountering problems with proofs involvingNat
s when trying even the simplest things such as iterating over matrix rows, etc. – Sam De Meyer Sep 29 '17 at 14:09unsafeCoerce
ing your way through some minimal set of arithmetic axioms. I suggest starting from <hackage.haskell.org/package/constraints-0.9.1/docs/…>. – Alec Sep 29 '17 at 14:59