如何对约束类型变量进行约束？约束？

Question

我正在玩ConstraintKindsGHC 的扩展.我有以下数据类型,它只是满足一个参数约束的一个框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适用于类型参数出现在第一个功能箭头右侧的任何类型类(如第二个a输入(==) :: a -> a -> Bool).

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

Answer 1

我们能够得到的最接近的Class1类是一个类,它将类和单个超类约束之间的关系重新作为一个类.它基于Class来自约束.

首先,我们将简要介绍一下约束包.A Dict捕获字典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).

单一继承

实际上class,仅使用单一继承实现此功能需要使用语言扩展的厨房接收器,包括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 Class1 b h | h -> b where
    cls1 :: h a :- b a

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

 class Show a => A a
 instance A Int

Show 是一个超类 A

instance Class1 Show A where
    cls1 = Sub Dict 

我们想为其编写Show实例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

我们可以Show一Some h每当h有一个超类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