如何对“Constraint”类型的变量施加约束？

Question

我正在研究 GHC 的 ConstraintKinds 扩展。我有以下数据类型，它只是一个盒子，用于满足某个参数约束 c:

data Some (c :: * -> Constraint) where
    Some :: forall a. c a => a -> Some c

例如，我可以用某种数字构造一个盒子（可以说不是很有用）。

x :: Some Num
x = Some (1 :: Int)

现在，只要 c 包含约束 Show，我就可以提供 Show (Some c).

的实例

instance ??? => Show (Some c) where
    show (Some x) = show x    -- Show dictionary for type of x should be in scope here

但是我如何在实例上下文中表达这个需求（标记为???）？

我不能使用等式约束（c ~ Show），因为两者不一定相等。 c 可能是 Num，这意味着但不等于 Show.

编辑

我意识到这在一般情况下是不可能的。

如果您有两个 Some Eq 类型的值，则无法比较它们是否相等。它们可以是不同的类型，每个类型都有自己的平等概念。

适用于 Eq 的内容适用于任何类型 class，其中类型参数出现在第一个函数箭头的右侧（如 [= 中的第二个 a 26=]).

考虑到没有办法创建约束表达"this type variable is not used beyond the first arrow"，我认为不可能写出我想写的实例。

Answer 1

您不能使 Some c 成为 Show 的实例，除非是微不足道的。

您想 show Some 中的 a，但该变量是存在量化的，因此我们不能依赖任何关于 a 类型的知识。特别是，我们无法知道 a 是 Show.

的实例

编辑： 我将扩展我的答案。即使有更多的机器，并放弃 Show 实例，我仍然不认为你想要的是可能的，因为存在量化。

首先我会以更熟悉的形式重写Some

data Dict p where
    Dict :: p a => a -> Dict p

谈论 "constraints implying constraints" 的通常方式是使用约束蕴含的概念。

data p :- q where
    Sub :: p a => Dict q -> p :- q

我们可以将 p :- q 类型的值视为如果约束 forall a. p a 成立，则 forall a. q a 成立的证明。

现在我们试着写一个合理的 show-ish 函数

showD :: p :- Show -> Dict p -> String
showD (Sub (Dict a)) (Dict b) = show b

乍一看，这可能行得通。我们将以下约束纳入范围（请原谅伪exists语法）

(0) p :: * -> Constraint
(1) exists a. p a           -- (Dict p)
(2) exists b. p b => Show b -- (p :- Show)

但现在事情分崩离析，GHC 理所当然地抱怨：

main.hs:10:33:
    Could not deduce (Show a2) arising from a use of `show' 
    from the context (p a)
      bound by a pattern with constructor
                 Sub :: forall (p :: * -> Constraint) (q :: * -> Constraint) a.
                        (p a) => 
                        Dict q -> p :- q,
               in an equation for `showD' 
      at main.hs:10:8-19                    
    or from (Show a1) 
      bound by a pattern with constructor
                 Dict :: forall (p :: * -> Constraint) a. (p a) => a -> Dict p, 
               in an equation for `showD'
      at main.hs:10:13-18 
    or from (p a2)
      bound by a pattern with constructor
                 Dict :: forall (p :: * -> Constraint) a. (p a) => a -> Dict p,
               in an equation for `showD'
      at main.hs:10:23-28

因为(1)的a和(2)的b是不可能统一的。

这与评论中提到的 constraints 包中使用的基本思想相同。

Answer 2

我们能得到的最接近的是 Class1 class，它将 class 和单个 superclass 约束之间的关系具体化为 class.它基于 Class from constraints.

首先，我们将简要介绍一下约束包。一个Dict captures the dictionary for a Constraint

data Dict :: Constraint -> * where
  Dict :: a => Dict a

:- 捕捉到一个约束需要另一个约束。如果我们有 a :- b，只要我们有约束 a，我们就可以为约束 b.

生成字典

newtype a :- b = Sub (a => Dict b)

我们需要一个类似于:-的证明，我们需要知道forall a. h a :- b a，或者h a => Dict (b a).

单一继承

实际为 classes 实现这个只有一个继承需要语言扩展的厨房水槽，包括 OverlappingInstances。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Data.Constraint

我们将定义类型 k -> Constraint 的约束的 class，其中约束具有单个 superclass.

class Class1 b h | h -> b where
    cls1 :: h a :- b a

我们现在可以解决示例问题了。我们有一个 class A 需要一个 Show 实例。

 class Show a => A a
 instance A Int

Show 是 A

的超级class

instance Class1 Show A where
    cls1 = Sub Dict

我们想为 Some

编写 Show 个实例

data Some (c :: * -> Constraint) where
    Some :: c a => a -> Some c

我们可以Show一个Some Show.

instance Show (Some Show) where
    showsPrec x (Some a) = showsPrec x a

我们可以 Show 一个 Some h 每当 h 有一个超级 class b 并且我们可以显示 Some b.

instance (Show (Some b), Class1 b h) => Show (Some h) where
    showsPrec x (Some (a :: a)) = 
        case cls1 :: h a :- b a of
            Sub Dict -> showsPrec x ((Some a) :: Some b)

这让我们写

x :: Some A
x = Some (1 :: Int)

main = print x

Answer 3

新的 QuantifiedConstraints 扩展允许这样做。

class (a => b) => Implies a b where
instance (a => b) => Implies a b where
instance (forall a. c a `Implies` Show a) => Show (Some c) where
  show (Some x) = show x

在Show实例体内，就好像有一个

instance forall a. Implies (c a) (Show a)

范围内。如果您随后拥有 T :: Type 并知道 c T，那么专用 Implies (c T) (Show T) 实例的 c T => Show T 的超类允许您派生 Show T。有必要使用 Implies 而不是直接的 forall a. c a => Show a 约束。这个不正确的约束就像

instance forall a. c a => Show a

与每个 Show 个实例重叠，。通过一个无用约束的超类强制间接修复一切。

如何对“Constraint”类型的变量施加约束？

How to put constraints on type variable of kind `Constraint`?

haskell

ghc

typeclass

gadt

单一继承