使用“constraints”包来减少一个被包装的函数的多态性

如何解决使用“constraints”包来减少一个被包装的函数的多态性

我有这个数据类型：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy
import Data.Constraint
import Data.Kind

type Foo :: (Type -> Constraint) -> Type
data Foo c = Foo (Proxy c) (forall x. c x => x -> x)

它看起来不是很有用，但它是有用的数据类型的简化版本。

我想使用 constraints 包来编写约束的映射函数，使用 entailment 的证据：

restrictFoo :: forall less more. (forall v. more v :- less v) -> Foo less -> Foo more

这个想法是，如果 more 约束比 less 约束更强，那么应该可以将 Foo 中约束较少的函数转换为约束较大的函数。>

我认为 forall v 在正确的位置。如果它涵盖所有签名，则调用者将是选择 v 的人，这在使用多态函数时似乎适得其反。

这种幼稚的尝试是行不通的：

restrictFoo :: forall less more. (forall v. more v :- less v) -> Foo less -> Foo more 
restrictFoo (Sub Dict) (Foo proxy f) = 
     Foo (Proxy @more) f

它失败了

* Could not deduce: more v0 arising from a pattern
* In the pattern: Dict
  In the pattern: Sub Dict
...
* Could not deduce: less x arising from a use of `f'
  from the context: less v0

如何正确书写restrictFoo的正文？

解决方法

您对 Dict 的模式匹配过于急切。 Dict 提供约束 less v，但它来自 Sub，只有当您提供 less v 时才会给您 more v，而您还没有在那时候;你甚至没有 v 所以现在专门化那个 :- 论点还为时过早

您只会在 more x 的第二个字段内得到一个约束 Foo，因此在 Sub 上进行模式匹配。

restrictFoo :: forall less more. (forall v. more v :- less v) -> Foo less -> Foo more 
restrictFoo sub (Foo proxy f) = Foo (Proxy @more) g where
  g :: forall x. more x => x -> x
  g = case sub @x of
    Sub Dict -> f

问题是，当您解开 Sub Dict 时，需要有一些 v 字典将应用到的范围内，但没有。因此，编译器尝试创建一个新的 var v0，希望最终将其与某些东西统一起来，但这种可能性永远不会到来。

但是让我们想想：v 最终来自哪里？那么，展开 Sub Dict 会给我们带来什么？它给了我们一个 less v（对于一些未知的 v），前提是我们可以给它 more v。我们刚好拥有 more v 并且需要 less v 的地方是什么？为什么它当然在 Foo 的第二个参数中！

所以这意味着只有当 Sub Dict 的第二个参数被实际调用时，我们才需要解包 Foo。届时，调用它的人将提供一个 more v 实例，因此我们将能够将其提供给 Sub Dict 并获得 less v。

太天真了，它看起来像这样：

restrictFoo e (Foo proxy f) =
     Foo (Proxy @more) \x -> case e of Sub Dict -> f x

但这仍然不起作用：编译器不知道 x 的类型与它需要用于 Sub Dict 的类型相同。两者之间没有任何联系！

要创建这样的连接，我们需要明确地量化 x 的类型，为此，我们需要给新函数一个类型签名：

restrictFoo e (Foo proxy f) =
     Foo (Proxy @more) f'
     where
        f' :: forall x. more x => x -> x
        f' x = case e of Sub (Dict :: Dict (less x)) -> f x

现在这有效：每当有人从 f' 中取出 Foo 并调用它时，他们将不得不提供 more x 的实例，并且将该实例置于范围内将允许我们把它交给 Sub 并得到一个 Dict (less x)，它为我们提供了一个 less x 的实例，它最终允许我们调用原始的 f。