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.
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]