Mapping a Dependent Type over a List of Types

Question

I think my question is fairly straightforward to understand from simple code, but I'm not, on the other hand, sure about the answer! Intuitively, what I want to do is given a list of types [*] and some dependent type Foo, generate the type [Foo *]. That is, I want to 'map' the dependent type over the base type.

Firstly, I'm working with the following extensions

{-# LANGUAGE TypeOperators,DataKinds,GADTs,TypeFamilies #-}

Let's say we have some dependent type

class Distribution m where
    type SampleSpace m :: *

which characterizes the sample space of some probability distribution. If we want to define a product distribution over potentially heterogeneous values, we might write something like

data PDistribution (ms :: [*]) where
    DNil :: PDistribution ('[])
    (:*:) :: Distribution m => m -> (PDistribution ms) -> PDistribution (m ': ms)

and complement it with

data PSampleSpace (m :: [*]) where
    SSNil :: PSampleSpace ('[])
    (:+:) :: Distribution m => SampleSpace m -> (PSampleSpace ms) -> PSampleSpace (m ': ms)

so that we may define

instance Distribution (PDistribution ms) where
    type SampleSpace (PDistribution ms) = PSampleSpace ms

Now this is all fairly nice, except that the type of PSampleSpace will lead to some problems down the line. In particular, if we want to construct a PSampleSpace directly, e.g.

ss = True :+: 3.0 :+: SNil

we have to explicitly give it a set of distributions that generate it or come up against the monomorphism restriction. Moreover, since two distributions can certainly share a SampleSpace (Normals and Exponentials both describe Doubles) it seems silly to pick one distribution just to fix the type. What I'd really like to define is to define a simple heterogeneous list

data HList (xs :: [*]) where
    Nil :: HList ('[])
    (:+:) :: x -> (HList xs) -> HList (x ': xs)

and write something like

instance Distribution (PDistribution (m ': ms)) where
    type SampleSpace (PDistribution (m ': ms)) = HList (SampleSpace m ': mxs)

where mxs has somehow been converted to the list of SampleSpaces that I want. Of course, this last bit of code doesn't work, and I don't know how to fix it. Cheers!

Edit

Just as a solid example of the problem of the proposed solution I'm having, suppose I have the class

class Distribution m => Generative m where
    generate :: m -> Rand (SampleSpace m)

Even though it seems like it should type check, the following

instance Generative (HList '[]) where
    generate Nil = return Nil

instance (Generative m, Generative (HList ms)) => Generative (HList (m ': ms)) where
    generate (m :+: ms) = do
        x <- generate m
        (x :+:) <$> generate ms

does not. GHC complains that it

Could not deduce (SampleSpace (HList xs) ~ HList (SampleSpaces xs))

Now I can get things working with my PDistribution GADT, because I force the required type classes on the sub distributions.

Final Edit

So there are a few ways to go at this problem. The TypeList is the most general. My question is more than answered at this point.

Answer 1

Why make the product of distributions out of a list? Will an ordinary tuple (the product of two types) work in place of :*:?

{-# LANGUAGE TypeOperators,TypeFamilies #-}

class Distribution m where
    type SampleSpace m :: *

data (:+:) a b = ProductSampleSpaceWhatever
    deriving (Show)

instance (Distribution m1, Distribution m2) => Distribution (m1, m2) where
    type SampleSpace (m1, m2) = SampleSpace m1 :+: SampleSpace m2

data NormalDistribution = NormalDistributionWhatever

instance Distribution NormalDistribution where
    type SampleSpace NormalDistribution = Doubles

data ExponentialDistribution = ExponentialDistributionWhatever

instance Distribution ExponentialDistribution where
    type SampleSpace ExponentialDistribution = Doubles

data Doubles = DoublesSampleSpaceWhatever

example :: SampleSpace (NormalDistribution, ExponentialDistribution)
example = ProductSampleSpaceWhatever

example' :: Doubles :+: Doubles
example' = example

-- Just to prove it works:
main = print example'

The difference between a tree of tuples and a list is that trees of tuples are magma-like (there's a binary operator), while lists are monoid-like (there's a binary operator, an identity, and the operator is associative). So there's no single, picked out DNil that is the identity, and the type doesn't force us to discard the difference between (NormalDistribution :*: ExponentialDistribution) :*: BinaryDistribution and NormalDistribution :*: (ExponentialDistribution :*: BinaryDistribution).

Edit

The following code makes type lists with an associative operator, TypeListConcat, and an identity, TypeListNil. Nothing guarantees that there won't be other instances of TypeList than the two types provided. I couldn't get TypeOperators syntax to work for everything I'd like it to.

{-# LANGUAGE TypeFamilies,MultiParamTypeClasses,FlexibleInstances,TypeOperators #-}

-- Lists of types

-- The class of things where the end of them can be replaced with something
-- The extra parameter t combined with FlexibleInstances lets us get away with essentially
--  type TypeListConcat :: * -> *
-- And instances with a free variable for the first argument
class TypeList l a where
    type TypeListConcat    l    a :: * 
    typeListConcat      :: l -> a -> TypeListConcat l a

-- An identity for a list of types. Nothing guarantees it is unique
data TypeListNil = TypeListNil
    deriving (Show)

instance TypeList TypeListNil a where
    type TypeListConcat TypeListNil a = a
    typeListConcat      TypeListNil a = a

-- Cons for a list of types, nothing guarantees it is unique.
data (:::) h t = (:::) h t
    deriving (Show)

infixr 5 :::

instance (TypeList t a) => TypeList (h ::: t) a where
    type TypeListConcat (h ::: t) a = h ::: (TypeListConcat t a)
    typeListConcat      (h ::: t) a = h ::: (typeListConcat t a)

-- A Distribution instance for lists of types
class Distribution m where
    type SampleSpace m :: *

instance Distribution TypeListNil where
    type SampleSpace TypeListNil = TypeListNil

instance (Distribution m1, Distribution m2) => Distribution (m1 ::: m2) where
    type SampleSpace (m1 ::: m2) = SampleSpace m1 ::: SampleSpace m2

-- Some types and values to play with
data NormalDistribution = NormalDistributionWhatever

instance Distribution NormalDistribution where
    type SampleSpace NormalDistribution = Doubles

data ExponentialDistribution = ExponentialDistributionWhatever

instance Distribution ExponentialDistribution where
    type SampleSpace ExponentialDistribution = Doubles

data BinaryDistribution = BinaryDistributionWhatever

instance Distribution BinaryDistribution where
    type SampleSpace BinaryDistribution = Bools

data Doubles = DoublesSampleSpaceWhatever
    deriving (Show)

data Bools = BoolSampleSpaceWhatever
    deriving (Show)

-- Play with them

example1 :: TypeListConcat (Doubles ::: TypeListNil) (Doubles ::: Bools ::: TypeListNil)
example1 = (DoublesSampleSpaceWhatever ::: TypeListNil) `typeListConcat` (DoublesSampleSpaceWhatever ::: BoolSampleSpaceWhatever ::: TypeListNil)

example2 :: TypeListConcat (Doubles ::: Doubles ::: TypeListNil) (Bools ::: TypeListNil)
example2 = example2

example3 :: Doubles ::: Doubles ::: Bools ::: TypeListNil
example3 = example1

example4 :: SampleSpace (NormalDistribution ::: ExponentialDistribution ::: BinaryDistribution ::: TypeListNil)
example4 = example3

main = print example4

Edit - code using TypeLists

Here's some code that is similar to the code you added in your edit. I couldn't figure out what Rand is supposed to be, so I made up something else.

-- Distributions with sampling

class Distribution m => Generative m where
    generate :: m -> StdGen -> (SampleSpace m, StdGen)

instance Generative TypeListNil where
    generate TypeListNil g = (TypeListNil, g)

instance (Generative m1, Generative m2) => Generative (m1 ::: m2) where
    generate (m ::: ms) g =
        let
            (x, g') = generate m g
            (xs, g'') = generate ms g'
        in (x ::: xs, g'')

-- Distributions with modes

class Distribution m => Modal m where
    modes :: m -> [SampleSpace m]

instance Modal TypeListNil where
    modes TypeListNil = [TypeListNil]

instance (Modal m1, Modal m2) => Modal (m1 ::: m2) where
    modes (m ::: ms) = [ x ::: xs | x <- modes m, xs <- modes ms]