had a question about singletons
I have a promoted data type a
where I instanced data family Sing (a :: Foo)
appropriately.
I also have a type family Bar (a :: Foo) (b :: Foo) :: Foo
In the middle of a busy function, I have:
(\(x :: Sing n) (y :: Sing m) -> doThingsWith (sing :: Sing (Bar n m)))
But I'm not sure where I should put my SingI
constraint.
For more details, my type is
data PNat = NZ | NS PNat
data instance Sing (n :: PNat) where
SNZ :: Sing 'NZ
SNS :: Sing (m :: PNat) -> Sing ('NS m)
and my type family is
type family NPlus (n :: PNat) (m :: PNat) :: PNat where
NPlus NZ y = y
NPlus (NS x) y = NS (NPlus x y)
Now, I'm actually able to manually write out explicit singleton shuffling:
nPlus :: forall n m nm. (NPlus n m ~ nm) => Sing n -> Sing m -> Sing nm
nPlus SNZ y = y
nPlus (SNS x) y = SNS (nPlus x y)
And this compiles fine...I can do
\x y -> nPlus x y
but I feel like I should be able to just use singI
here and let the type family do both of the work. Besides, I have a lot of functions like this, too, and would prefer to not have to do it for each one.
I do have ScopedTypeVariables turned on.
thank you all
Edit: Ah, I just realized that SingI
instances aren't automatically derived; I whipped one up:
instance SingI NZ where
sing = SNZ
instance SingI n => SingI (NS n) where
sing = SNS sing
Unfortunately, GHC is still telling me that there is no instance of SingI
when I use sing
in the lambda above :/
I feel like I should be able to just use singI here and let the type family do both of the work.
This can't be done. The reason why we have the many TH facilities in singletons
is that data and function definitions must be duplicated in the current state of affairs.
The idiomatic usage would be defining everything on the term level once, and deriving the rest with TH.
-- LANGUAGE KitchenSink
import Data.Singletons.TH
import Data.Singletons.Prelude
$(singletons [d|
data PNat = NZ | NS PNat deriving (Eq, Show, Ord)
nPlus :: PNat -> PNat -> PNat
nPlus NZ y = y
nPlus (NS x) y = NS (nPlus x y) |])
This creates the Sing
definition,the type family for nPlus
, SingI
instances, SingKind
instances, the kind-restricted SPNat
type synonym for Sing
, defunctionalization symbols for type families and constructors, and also type-level analogues for Eq
and Ord
, and also decidable equality. You can hit :bro
on the module and :i PNat
to find out exactly what got generated.
Now nPlus
and the type family NPlus
work as intended.
To provide a bit of explanation regarding SingI
: SingI a => t
is equivalent to Sing a -> t
. They even compile to the exact same Core code. The only difference between them is that Sing
-s are passed explicitly and SingI
-s implicitly. sing
provides conversion from SingI
to Sing
, and singInstance
converts backwards.
In the light of this, something like
(SingI (NPlus n m)) => Sing n -> Sing m -> Sing (NPlus n m)
is pretty awkward, since it's equivalent to
Sing (NPlus n m) -> Sing n -> Sing m -> Sing (NPlus n m)
which can be implemented as a constant function that doesn't do any addition.
So when should we use SingI
or Sing
? The most convenient way is to perform computation on Sing
-s, since we can pattern match on them, and use SingI
only when we just need to plug in or pass along a value somewhere, but don't need to pattern match or recurse.