如何在约束类型的约束上施加约束? [英] How to put constraints on type variable of kind `Constraint`?

问题描述

我正在使用GHC的 ConstraintKinds 扩展名.我有以下数据类型，这只是满足某些参数约束 c 的框:

I'm playing around with the ConstraintKinds extension of GHC. I have the following data type, which is just a box for things fulfilling some one parameter constraint c:

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

例如，我可以构造一个带有某种数字的盒子(据说不是很有用).

For example, I could construct a box with some kind of number (arguably not very useful).

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

现在，只要 c 包含约束 Show ，我就可以提供 Show(某些c)的实例.

Now, as long as c includes the constraint Show, I could provide an instance of Show (Some c).

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

但是我如何在实例上下文(用 ??? 标记)中表达此要求?

But how do I express this requirement in the instance context (marked with ???)?

我不能使用等式约束( c〜Show )，因为两者不一定相等. c 可以是 Num ，这意味着但不等于 Show .

I cannot use an equality constraint (c ~ Show), because the two are not necessarily equal. c could be Num, which implies, but is not equal to, Show.

修改

我意识到这通常是不可能的.

I realised that this cannot be possible in general.

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

If you have two values of type Some Eq, it is not possible to compare them for equality. They could be of different types that each have their own notion of equality.

适用于 Eq 的内容适用于类型参数出现在第一个功能箭头右侧的任何类型类(例如 a >(==):: a-> a->布尔).

What applies to Eq applies to any type class in which the type parameter appears on the right hand side of the first function arrow (like the second a in (==) :: a -> a -> Bool).

考虑到无法创建表示未在第一个箭头之外使用此类型变量"的约束，我认为不可能编写我要编写的实例.

Considering that there is no way to create a constraint expressing "this type variable is not used beyond the first arrow", I don't think it is possible to write the instance I want to write.

推荐答案

我们能够获得的最接近的是一个 Class1 类，该类可将一个类与单个超类约束作为一个类进行关系化..它基于 Class 约束中的a>.

The closest we are able to get is a Class1 class that reifys the relationship between a class and a single superclass constraint as a class. It's based on the Class from constraints.

首先，我们将简短浏览一下约束包. Dict 捕获 约束 的字典a>

First, we'll take a short tour of the constraints package. A Dict captures the dictionary for a Constraint

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

:-捕获一个约束带来另一个约束.如果我们有 a:-b ，则每当我们有约束 a 时，我们都可以为约束 b 生成字典.

:- captures that one constraint entails another. If we have a :- b, whenever we have the constraint a we can produce the dictionary for the constraint b.

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

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

We need a proof similar to :-, we need to know that forall a. h a :- b a, or h a => Dict (b a).

实际上，仅通过单个继承就可以为 class 实现此功能，这需要语言扩展的厨房工具，包括 OverlappingInstances .

Actually implementing this for classes with just single inheritance requires the kitchen sink of language extensions, including 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->的约束类别.约束，其中约束具有单个超类.

We'll define the class of constraints of kind k -> Constraint where the constraint has a single superclass.

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

我们现在有能力解决示例问题.我们有一个类 A ，它需要一个 Show 实例.

We're now equipped to tackle our example problem. We have a class A that requires a Show instance.

 class Show a => A a
 instance A Int

Show 是 A

instance Class1 Show A where
    cls1 = Sub Dict 

我们要为 Some

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

只要 h 有一个超类 b ，我们就可以显示一个h >有些b .

We can Show a Some h whenever h has a single superclass b and we could show 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

这篇关于如何在约束类型的约束上施加约束?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！