我认为我的问题通过简单的代码很容易理解,但另一方面,我不确定答案!直观地说,我想要做的是给定一个类型 [*] 和一些依赖类型 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
我们必须明确地给它一组生成它的分布或遇到单态限制。此外,由于两个分布当然可以共享一个 SampleSpace(法线和指数都描述 double 型),选择一个分布只是为了修复类型似乎很愚蠢。我真正想定义的是定义一个简单的异构列表
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 列表。当然,这最后一点代码不起作用,我不知道如何修复它。干杯!
编辑
正如我所提出的解决方案的问题的一个可靠例子,假设我有这门课
class Distribution m => Generative m where
generate :: m -> Rand (SampleSpace m)
即使它看起来应该类型检查,以下
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 来处理事情,因为我在子发行版上强制使用所需的类型类。
最终编辑
所以有几种方法可以解决这个问题。 TypeList 是最通用的。在这一点上,我的问题不仅仅是回答。
最佳答案
这是 DataKinds
的解决方案.我们需要更多的扩展,FlexibleContexts
和 FlexibleInstances
.
{-# LANGUAGE TypeOperators,DataKinds,GADTs,TypeFamilies,FlexibleInstances,FlexibleContexts #-}
我们将继续使用您的
Distribution
类作为依赖类型的示例class Distribution m where
type SampleSpace m :: *
借用the TypeMap example you found , 我们会有
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
关于haskell - 在类型列表上映射依赖类型,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/22788819/