首页
学习
活动
专区
圈层
工具
发布
首页
学习
活动
专区
圈层
工具
MCP广场
社区首页 >问答首页 >从上下文` `Show (a,b)`获取` `Show a`

从上下文` `Show (a,b)`获取` `Show a`
EN

Stack Overflow用户
提问于 2016-09-22 21:03:30
回答 3查看 153关注 0票数 8

正如标题所说,我对在拥有Show (a,b)的上下文中使用Show a很感兴趣。这个问题很容易在GADT中出现,如下所示:

代码语言:javascript
运行
复制
data PairOrNot a where
  Pair :: (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a

showFirstIfPair :: Show a => PairOrNot a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show b

错误是:

代码语言:javascript
运行
复制
Could not deduce (Show b) arising from a use of ‘show’
from the context (Show a)
  bound by the type signature for
             showFirstIfPair :: Show a => PairOrNot a -> String
  at app/Main.hs:24:20-50
or from (a ~ (b, c))
  bound by a pattern with constructor
             Pair :: forall b c. (b, c) -> PairOrNot (b, c),
           in an equation for ‘showFirstIfPair’
  at app/Main.hs:26:18-27
Possible fix:
  add (Show b) to the context of the data constructor ‘Pair’
In the expression: show b
In an equation for ‘showFirstIfPair’:
    showFirstIfPair (Pair (b, c)) = show b

我认为实例声明instance (Show a, Show b) => Show (a,b)证明了Show element,但我也可以想象这个问题也与运行时如何实现类型类机制有关。

我发现,如果我们可以修改类的定义,就有可能通过:

代码语言:javascript
运行
复制
class Show' a where
  show' :: a -> String
  unpair :: a -> Dict (a ~ (b,c)) -> Dict (Show' b, Show' c)

-- An example non-pair instance
instance Show' Int where
  show' i = ""
  unpair = undefined -- This is OK, since no one can construct Dict (Int ~ (b,c))

instance (Show' a, Show' b) => Show' (a,b) where
  show' (a,b) = ""
  unpair _ Dict = Dict -- In this context we have access to Show' for elems

然后在使用站点,我们显式地获取字典:

代码语言:javascript
运行
复制
showFirstIfPair :: Show' a => PairOrNot a -> String
showFirstIfPair (Not a) = show' a
showFirstIfPair (Pair a@(b,c)) = 
  case unpair a Dict of -- This is a Dict (a~(b,c))
    Dict -> show' b -- This is Dict (Show' b,Show' c)

我想知道是否有一种非侵入性(或只是不同)的方式来获得Show element。如果没有,你能解释一下为什么会出现这个问题吗?

EN

回答 3

Stack Overflow用户

发布于 2016-09-22 21:40:30

如果您不介意b必须始终是Show实例的限制,那么这是一个简单的解决方案:

代码语言:javascript
运行
复制
data PairOrNot a where
  Pair :: Show b => (b,c) -> PairOrNot (b,c)
  Not :: a -> PairOrNot a
票数 2
EN

Stack Overflow用户

发布于 2016-09-23 20:08:22

我一直在尝试是否能想出更好的办法,下面是我能想到的最好的办法:

在我最初的尝试中,我将Show'类型类与pairs的实例声明耦合在一起。尽管我找不到修改类型类的方法,但我至少已经设法为任何实例声明泛化了这一点。

正如问题的评论中指出的那样,instance (Show a, Show b) => Show (a,b)是一个单向的含义,但我假设它也可以应用于另一个方向,因为没有重叠的实例。不幸的是,GHC并不依赖于此,但我们可以自己断言这一点。我的直觉可以转化为代码:(:=>来自constraints包中的Data.Constraint,而a :=> b意味着在某个地方有一个instance a => b )

代码语言:javascript
运行
复制
class Show' a where
  show' :: a -> String
  noOverlap :: (b :=> Show' a) => Proxy a -> Dict b

在这里,noOverlap函数是一个承诺,如果你能找到一个产生实例Show' a的约束b,我就可以证明给定Show' ab。这个承诺相当于声明将不会有Show'的重叠实例

现在,我们需要一个辅助函数来实际实现noOverlap

代码语言:javascript
运行
复制
basedOn :: forall k a. (k :=> Show' a, k) => 
             (forall b. (b :=> Show' a) => Proxy a -> Dict b)
basedOn _ = unsafeCoerce (Dict :: Dict k)

此函数的作用是,如果在具有实例k :=> Show' a的上下文中调用它,它将返回一个函数,该函数将为任何实例b :=> Show' a返回Dict b。我们必须使用unsafeCoerce来说服GHC Dict kDict b是相同的,但据我所知,这是对unsafeCoerce的安全使用,因为函数依赖a :=> b | b -> a确保对于给定的Show' a只能有一个k :=> Show' a实例。

现在,对于这个帮助器,下面是如何定义实例的

代码语言:javascript
运行
复制
-- An example non-pair instance
instance () :=> Show' Int where ins = Sub Dict 
instance        Show' Int where
  show' i = ""
  noOverlap = basedOn

instance (Show' a, Show' b) :=> Show' (a,b) where ins = Sub Dict
instance (Show' a, Show' b)  => Show' (a,b) where
  show' (a,b) = ""
  noOverlap = basedOn -- GHC does all the plumbing here

我们必须手动定义:=>实例,因为GHC不会自动定义,但没有出错的余地。如果我们在手动定义的:=>的左边给出了一个太弱的约束,ins = Sub Dict将无法编译,如果我们给出一个太强的约束,那么noOverlap = basedOn将无法编译,因此编译器会强制使用样板。

然后,我们可以使用noOverlap,如下所示:

代码语言:javascript
运行
复制
showFirstIfPair :: Show' a => PairOrNot a -> String
showFirstIfPair (Not a) = show' a
showFirstIfPair (Pair a@(b,c)) = 
  -- In this context we have (Show' b, Show' c) :=> Show' a
  case noOverlap Proxy of -- This is a Proxy a
    Dict -> show' b -- This is a Dict (Show' b, Show' c)

好的是,现在我们也可以从Show' [a]转到Show' a,或者任何其他的实例声明。

注意:您需要使用{-# LANGUAGE FlexibleContexts, TypeOperators, RankNTypes, ConstraintKinds, AllowAmbiguousTypes #-}来编译这些代码。

票数 1
EN

Stack Overflow用户

发布于 2016-09-23 20:16:54

下面是user2297560的一个概括,它不需要在GADT中硬编码Show

代码语言:javascript
运行
复制
{-# LANGUAGE ConstraintKinds, KindSignatures #-}
import GHC.Exts (Constraint)

data PairOrNot (cl :: * -> Constraint) (a :: *) where
  Pair :: (cl b, cl c) => (b,c) -> PairOrNot (b,c)
  Not :: cl a => a -> PairOrNot a

然后你就可以

代码语言:javascript
运行
复制
showFirstIfPair :: PairOrNot Show a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show b
票数 1
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/39639892

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档