SingI Instance for data-types

[LeanderK]

I have a fixed-length vector defined by:

data Vec (n :: Nat) a = UnsafeMkVec { getVector :: V.Vector a }
    deriving Show

is there some th-function that generates SingI-Instances for Vec so that I can access the length etc.?

[LeanderK]

What I want to write is an instance for this class:

class InitRandom a where
   init :: MonadRandom m => Sing a -> m a

[RyanGlScott]

If you're looking for something that only generates SingI instances, the answer is no.

If you're looking for something that will generate SingI instances and some other things, the answer is... yes (sort of). There does exist the function genSingletons which, among other things, will generate SingI instances.

That being said, the code that genSingletons would generate for Vec wouldn't typecheck, as you have a type parameter that isn't of kind Type. See #150.

[LeanderK]

I thought I was doing something wrong because, as you said, it didn't typecheck 😉

ok, can I write the instance by hand or is it a limitation of GHC/singletons that it doesn't typecheck??

[RyanGlScott]

You can certainly write SingI instances by hand in general—they follow a pretty predictable pattern. For instance:

data Option a = None | Some a

data instance Sing (z :: Option a) where
  SNone :: Sing None
  SSome :: Sing a -> Sing (Some a)

instance SingI None where
  sing = SNone

instance SingI a => SingI (Some a) where
  sing = SSome sing

The real question is: how are you planning to give Sing/SingI instances for Vector? That's not a conventionally defined datatype (in the sense that it's not a simple ADT), so it's hard to imagine how that would work.

[LeanderK]

I think I confused myself with all these types 😀
This is not what I want, I only care about the type-parameters for Vec.

[LeanderK]

I'll close it because the code above doesn't make sense, or at least is not what I want to do.

[RyanGlScott]

What may interest you is the idea of parameterizing Vec by whether you're using it at the type level or not. For instance, you could conceivably do something like this:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where

import Data.Kind
import Data.Singletons.Prelude
import qualified Data.Vector as V
import GHC.TypeNats

newtype Vec' (p :: Type -> Type) (n :: Nat) a = MkVec (p a)
  deriving Show

-- Value-level
type Vec  = Vec' V.Vector
-- Type-level
type PVec = Vec' []

data instance Sing (z :: PVec n a) where
  SMkVec :: Sing x -> Sing (MkVec x :: PVec n a)

instance SingKind a => SingKind (PVec n a) where
  type Demote (PVec n a) = Vec n (Demote a)
  fromSing (SMkVec sx) = MkVec $ V.fromList $ fromSing sx
  toSing (MkVec x) = withSomeSing (V.toList x) $ SomeSing . SMkVec

instance SingI x => SingI (MkVec x :: PVec n a) where
  sing = SMkVec sing

Of course, you'd still have to write all of this out by hand, and you'd need to expose the constructor to Vec'. But it's technically possible!

[LeanderK]

I think there is a misunderstanding!

[LeanderK]

This does not work, but I think it illustrates what I want to do.
I am sorry for not communicating clearer, I am still a bit confused myself.

data instance Sing (Vec l a) where
    SVec :: Sing l -> Sing a -> Sing (Vec l a)

instance (SingI l, SingI a) => SingI (Vec l a) where
    sing = SVec sing sing

stest = sing @Type @(Vec 13 Int)

everything revolves around this class

class InitRandom a where
   init :: MonadRandom m => Sing a -> m a

I want to initialize a Container polymorphically that is "dependent on it's type" (I don't know whether this makes sense?). Vec itself is not actually used in a type-level way. I essentially want to get it's type-level params out.

[RyanGlScott]

I'm afraid I don't know how to respond, since a good chunk of the code in #303 (comment) is nonsense. For one thing, one never writes a Sing instance like this:

data instance Sing (Vec l a) where ...

Sing instances are intended to be indexed by their kinds, so what you really wanted to write was:

data instance Sing (z :: Vec l a) where ...

Also, the constructor itself makes little sense to me:

    SVec :: Sing l -> Sing a -> Sing (Vec l a)

The return type of a Sing instance is usually of the form Sing (C a1 ... an), where C is a constructor that inhabits the type you put into Sing's kind.

[LeanderK]

I think I just solved it...

data Vec (n :: Nat) a = UnsafeMkVec { getVector :: V.Vector a }
    deriving Show

data instance Sing (Vec l a) where
    SVec :: Sing l -> Sing (Vec l a)

instance (SingI l) => SingI (Vec l a) where
    sing = SVec sing

stest = sing @Type @(Vec 13 Int)

Does this make sense? At least it compiles!
I am not using Vec in the Type-Level world, i just need it's type level argument (the size).
SVec has exactly the signature I need to randomly Init Vecs!

[mstksg]

This is definitely not what you want. A 'Sing a' should represent literally just 'a'. What you wrote isn't really a singleton and definitely does not make sense.

If you want a way to create a random value from the shape, you might want something like:

class InitRandom a where
   init :: MonadRandom m => m a

And you could write an instance for your vector:

instance SingI n => InitRandom (Vec n a) where
   ...

Note that the singleton in this case is a singleton on the 'Nat' in your vector type. This means you are essentially passing in the Nat as an argument to your init:

init :: SingI n => m (Vec n a)

-- equivalent to:
init :: Sing n -> m (Vec n a)

[LeanderK]

I feel a bit stupid 😀

of course

instance SingI n => InitRandom (Vec n a) where
   ...

would solve my problem.
Thank you!