haskell - 如何使用函数依赖和存在量化来为我的类型删除不必要的参数

Question

在我正在研究的 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 爆炸:

Illegal polymorphic or qualified type: Container model In the instance declaration for `Model (ContainerParams params) (Container model)'

我不知道这个错误信息是什么意思。是否有可能以某种方式修复我的解决方案以制作 Container键入您不必指定参数的地方？

编辑:我应该注意到移动 forall声明到 Container'声明似乎需要一堆 unsafeCoerce s，所以这似乎是一个糟糕的解决方案。

另外，我可以更改 type Container进入 data Container并让事情正常工作，但这需要我重新声明 Conatiner' 的所有实例是其中的一部分，我不想这样做。我有许多遵循这种模式的不同类型，因此似乎应该有一种通用的方法来解决这个问题。

Answer 1

我不确定您是否想要普遍或存在量化。无论哪种方式，最好将其包装成新鲜的类型。

强烈建议:不要对普通数据类型使用约束头。他们会让你的生活更艰难，而不是更轻松。他们没有完成任何有用的事情。

存在的

{-# 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作为参数。这是因为要知道一些重要的事情:函数依赖不是汇合的!而且，为了类型检查，编译器不会假定它们是汇合的。函数依赖仅在指导约束求解器时有用(在某种程度上它们类似于序言中的“切割”等额外的逻辑结构)。如果你想要融合，请使用 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

然后你可以做一些事情，比如将两个容器与相同的 model类型，知道存在量化的 params会匹配。使用它，您可以定义

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 model, NewContainer model)可证明与 GADTContainer model 同构这也解释了这些类型之间的关系

无论如何，一旦你处理好了，你就可以使用适当的包装类型来定义你的实例。