Create a list of values from type-level list

Question

I have a type-level list like this

data TList (ixs :: [*]) (f :: * -> *) where
  TNil  :: TList '[] f
  (:-:) :: f ix -> TList ixs f -> TList (ix ': ixs) f

And I'm trying to generate a new TList using an existing one. The idea is to have a function

genTList :: TList ixs f -> t -> TList ixs g

where 't' is some function able to construct a value of type 'g x' where 'x' is one of types form the list 'ixs'.

So that given

data Foo x

and (some kind of)

generate :: forall x . Bar x

I could get something like this

genTList (Foo Int :-: Foo String) generate = Bar :-: Bar

So essentially for every item 'x' in the type list I want to have a type 'Bar x' and also construct its value with parameterless constructor, because I know that 'Bar x' doesn't have constructor parameters.

I tried to implement something (https://gist.github.com/lolepezy/30820595afd9217083c5ca629e350b55) but it wouldn't typecheck (reasonably).

So how should I approach the problem?

kosmikus · Accepted Answer · 2017-05-29 17:29:32Z

You define

class TListGen ixs (g :: * -> *) where
  genTList :: Proxy ixs -> g ix -> TList ixs g

but this means that the caller of the function can choose what to instantiate all of the type variables with, so in particular also how to instantiate ix.

So for example,

genTList (Proxy :: Proxy '[Int, String]) (Just False)

would be a type-correct call of this function, choosing g to be Maybe and ix to be Bool. But that can't be correct. We need to pass in something that is sufficiently polymorphic that it works at least for all the elements occuring in the type-level list, or even better, for any possible choice of ix. This is what a rank-2 polymorphic type achieves:

class TListGen ixs (g :: * -> *) where
  genTList :: Proxy ixs -> (forall ix . g ix) -> TList ixs g

This requires the RankNTypes language extension.

Now the caller can only pass a function that is polymorphic in the argument type of g. So passing Just False would no longer work, but passing Nothing would be ok.

The definition of the cases is in principle ok, but you can actually remove the OVERLAPS pragma and even the proxy argument, because nothing is overlapping, and the ixs can be inferred from the result type, as it occurs as an argument to the TList datatype:

class TListGen ixs (g :: * -> *) where
  genTList :: (forall ix . g ix) -> TList ixs g

instance TListGen '[] g where
  genTList _ = TNil

instance TListGen ixs g => TListGen (ix ': ixs) g where
  genTList g = g :-: genTList g

Now we can try to use it:

GHCi> genTList Nothing :: TList '[ Int, String ] Maybe

Unfortunately, this leads to an error, because there's no Show instance:

• No instance for (Show (TList '[Int, String] Maybe))
    arising from a use of ‘print’
• In a stmt of an interactive GHCi command: print it

Defining a Show instance for TList is possible, but a bit tricky.

I'm not sure whether this is primarily an exercise, but if you're ok with just reusing code, then all this is available in the generics-sop package.

Your TList is called NP (with the arguments being in flipped order), and your genTList is called pure_NP, so you can write

GHCi> import Generics.SOP.NP
GHCi> pure_NP Nothing :: NP Maybe '[ Int, String ]
Nothing :* (Nothing :* Nil)

Thanks! It's half-exercise indeed, but mainly I would like to have less dependencies and keep it simple.

Collectives™ on Stack Overflow

Create a list of values from type-level list

1 Answer 1

1 Comment

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

1 Comment

Your Answer

Sign up or log in

Post as a guest

Related