haskell – 如何使用函数依赖和存在量化来删除不必要的参数到我
|
在我正在处理的HLearn库中,我有一些容器数据类型如下所示：
data (Model params model) => Container' params model = Container'
{ baseparams :: params,basemodel :: model
}
问题是这种类型使用起来很难,因为params和model都是彼此唯一确定的： class Model params model | params -> model,model -> params 因此,如果我在指定类型时不必指定它们,那将会更方便.编译器应该能够自动为我完成. 我解决这个问题的想法是创建一个使用存在量化的类型别名： type Container model = forall params . (Model params model) => Container' params model 但这不起作用.如果我像往常一样制作一个Container’实例,一切正常： data ContainerParams params = ContainerParams params instance (Model params model) => Model (ContainerParams params) (Container' params model) 但是当我使用我的Container类型时： instance (Model params model) => Model (ContainerParams params) (Container model) ghc爆炸：
我不知道这个错误信息是什么意思.是否有可能以某种方式修复我的解决方案来制作一个Container类型,而不必指定params？ 编辑：我应该注意到将forall语句移动到Container’声明中似乎需要一堆unsafeCoerces,所以这似乎是一个糟糕的解决方案. 此外,我可以将类型Container更改为数据容器并使其工作,但这需要重新声明Conatiner所属的所有实例,并且我不想这样做.我有许多不同的类型遵循这种模式,所以似乎应该有一种通用的方法来解决这个问题.
我不确定你是否想要普遍或存在量化.无论哪种方式,最好将其包装成新鲜的类型.
强烈建议：不要在普通数据类型上使用约束头.他们会让你的生活更加艰难,而不是更容易.他们没有任何用处. 存在主义 {-# LANGUAGE GADTs #-}
data Container' params model = Container'
{ baseparams :: params,basemodel :: model
}
data Container p m where
Container :: Model params model => Container' params model -> Container params model
普遍 {-# LANGUAGE Rank2Types #-}
data Container' params model = Container'
{ baseparams :: params,basemodel :: model
}
newtype Container model = Container (forall params . Model params model => Container' params model)
您不能在类型类实例中具有通用或限定类型.所以 instance Model (ContainerParams params) (Container model) 由于类型同义词扩展为,因此不被允许 instance Model (ContainerParams params) (forall ...) 在我的GADT解决方案中,我将param和model视为参数.这是因为要知道一些重要的事情：功能依赖性不会融合！并且,编译器不会假定它们为了类型检查而汇合.函数依赖仅在引导约束求解器时有用(在某种程度上它们类似于prolog中的“cut”之类的额外逻辑构造).如果你想要合流,请使用TypeFamilies. class Model model where type Param model ... 或者这样做的绝佳方式 class (model ~ (TheModel param),param ~ (TheParam model)) => Model model param where
type TheModel param
type TheParam model
与fundep具有相同的双向性.而且,这会让你把你的存在主义实例写成 data Container model where Container :: Model model param => Container' model param -> Container model 然后你可以做一些事情,比如将两个具有相同模型类型的容器组合在一起,知道存在量化的参数将匹配.使用它,您可以定义 data HasParam model where HasParam :: Model model param => HasParam model data GADTContainer model where GADTContainer :: Model model param => Container' model param -> GADTContainer model newtype NewContainer model = NewContainer (forall param. Model model param => Container' model param) 然后元组(HasParam模型,NewContainer模型)可证明与GADTContainer模型同构,这也解释了这些类型之间的关系 无论如何,一旦你有了这个,你可以使用适当的包装类型定义你的实例. （编辑：李大同） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |