使用 "constraints" 包来减少包装函数的多态性

Question

我有这个数据类型：

{-# 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 package to write a mapping function over the constraint, using evidence of 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的正文？

Answer 1

您在 Dict 上进行模式匹配太急切了。 Dict 提供约束 less v，但它来自 Sub，只有当您提供 more v 时才会给您 less v，而您还没有在那时候;你甚至没有 v 所以现在专门化 :- 参数

还为时过早

您只会在 Foo 的第二个字段内获得约束 more x，因此在 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

Answer 2

问题是，当您展开 Sub Dict 时，字典要应用的范围内需要有一些 v，但是有 none .所以编译器试图创建一个新的 var v0 以希望最终将它与某些东西统一起来，但最终结果永远不会到来。

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

所以这意味着我们只需要在实际调用 Foo 的第二个参数时才需要解包 Sub Dict 。到那时，调用它的人将提供 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

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

使用 "constraints" 包来减少包装函数的多态性

Using the "constraints" package to make a wrapped function less polymorphic

haskell

polymorphism

typeclass