Сопоставление зависимого типа со списком типов

Я думаю, что мой вопрос довольно прост для понимания из простого кода, но, с другой стороны, я не уверен в ответе! Интуитивно, то, что я хочу сделать, это дать список типов [*] и некоторый зависимый тип Foo, генерирующий тип [Foo *]. То есть я хочу "сопоставить" зависимый тип с базовым типом.

Во-первых, я работаю со следующими расширениями 

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

Предположим, что у нас есть некоторый зависимый тип 

class Distribution m where
    type SampleSpace m :: *

Что характеризует образец пространство некоторого распределения вероятностей. Если мы хотим определить распределение продукта по потенциально неоднородным значениям, мы могли бы написать что-то вроде 

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

И дополнить его 

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

Чтобы мы могли определить 

instance Distribution (PDistribution ms) where
    type SampleSpace (PDistribution ms) = PSampleSpace ms
Теперь все это довольно хорошо, за исключением того, что тип PSampleSpace приведет к некоторым проблемам в будущем. В частности, если мы хотим построить PSampleSpace напрямую, например 
ss = True :+: 3.0 :+: SNil

Мы должны явно дать ему набор распределения, которые генерируют его или сталкиваются с ограничением мономорфизма. Более того, поскольку два распределения, безусловно, могут иметь общее пространство выборки (нормали и экспоненты описывают двойников), кажется глупым выбирать одно распределение только для того, чтобы зафиксировать тип. Что я действительно хотел бы определить, так это определить простой гетерогенный список 

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

И напишите что-нибудь вроде 

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

Где mxs каким-то образом был преобразован в список SampleSpaces, которые я хочу. Конечно, этот последний бит код не работает, и я не знаю, как это исправить. Ура!

Edit

Просто в качестве убедительного примера задачи предложенного решения предположим, что у меня есть класс 

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

Хотя кажется, что он должен ввести check, следующее 

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

Нет. GHC жалуется, что он 

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

Теперь я могу заставить вещи работать с моим PDistribution GADT, потому что я заставляю необходимые классы типов на sub распределения.

Окончательное Редактирование

Таким образом, есть несколько способов решить эту проблему. Этот тип является наиболее общим. На данный момент на мой вопрос более чем дан ответ.
2 5
haskell type-families

2 ответа:

Зачем делать продукт распределений из списка? Будет ли обычный кортеж (продукт двух типов) работать вместо :*:?

{-# 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'
Разница между деревом кортежей и списком состоит в том, что деревья кортежей похожи на магму (есть бинарный оператор), в то время как списки моноидны (есть бинарный оператор, тождество, и оператор ассоциативен). Таким образом, нет единого, выделенного DNil, который является идентичностью, и тип не заставляет нас отбрасывать различие между (NormalDistribution :*: ExponentialDistribution) :*: BinaryDistribution и NormalDistribution :*: (ExponentialDistribution :*: BinaryDistribution).

Edit

Следующий код создает списки типов с ассоциативным оператором TypeListConcat и идентификатором TypeListNil. Ничто не гарантирует, что не будет других экземпляров TypeList, кроме указанных двух типов. Я не мог заставить синтаксис TypeOperators работать для всего, что я хотел бы. 
{-# 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-код с использованием TypeLists

Вот код, похожий на тот, что вы добавили при редактировании. Я не мог понять, что Rand так и должно быть, поэтому я придумал кое-что еще.

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

Вот решение с DataKinds. Нам понадобится еще пара расширений, FlexibleContexts и FlexibleInstances.

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

Мы будем продолжать использовать ваш класс Distribution в качестве примера зависимого типа 

class Distribution m where
    type SampleSpace m :: *

Заимствуя из примера типовой карты, который вы нашли , мы получили бы 

type family   TypeMap (f :: * -> *) (xs :: [*]) :: [*]
type instance TypeMap t             '[]         =  '[]
type instance TypeMap t             (x ': xs)   =  t x ': TypeMap t xs

В списке типов мы хотели бы иметь возможность TypeMap SampleSpace. К сожалению, мы не можем частично применить тип из семейства типов, поэтому вместо этого мы специализируемся на TypeMap для SampleSpace. Идея здесь такова SampleSpaces = TypeMap SampleSpace 

type family   SampleSpaces (xs :: [*]) :: [*]
type instance SampleSpaces '[]         =  '[]
type instance SampleSpaces (x ': xs)   =  SampleSpace x ': SampleSpaces xs

Мы продолжим использовать ваш HList, но добавим для него экземпляр Show: 

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

infixr 5 :+:

instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
    showsPrec p (x :+: xs) = showParen (p > plus_prec) $
            showsPrec (plus_prec+1) x       .
            showString              " :+: " .
            showsPrec (plus_prec) xs
        where plus_prec = 5

instance Show (HList '[]) where
    show _ = "Nil"
Теперь мы все настроены на получение экземпляров для гетерогенных списков Distribution s. обратите внимание, как тип справа от ': использует SampleSpaces, который мы определили выше. 
instance (Distribution m, Distribution (HList ms)) => Distribution (HList (m ': ms)) where
    type SampleSpace (HList (m ': ms)) = HList (SampleSpace m ': SampleSpaces ms)

instance Distribution (HList '[]) where
    type SampleSpace (HList '[]) = HList '[]
Теперь мы можем поиграть с ним и увидеть, что множество типов эквивалентны 
-- 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 :: HList [Doubles, Doubles, Bools]
example1 = DoublesSampleSpaceWhatever :+: DoublesSampleSpaceWhatever :+: BoolSampleSpaceWhatever :+: Nil

example2 :: SampleSpace (HList [NormalDistribution, ExponentialDistribution, BinaryDistribution])
example2 = example1

example3 :: SampleSpace (HList [ExponentialDistribution, NormalDistribution, BinaryDistribution])
example3 = example2

main = print example3
1