正如标题所说,我对在拥有Show (a,b)的上下文中使用Show a很感兴趣。这个问题很容易在GADT中出现,如下所示:
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错误是:
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,但我也可以想象这个问题也与运行时如何实现类型类机制有关。
我发现,如果我们可以修改类的定义,就有可能通过:
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然后在使用站点,我们显式地获取字典:
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。如果没有,你能解释一下为什么会出现这个问题吗?
发布于 2016-09-22 21:40:30
如果您不介意b必须始终是Show实例的限制,那么这是一个简单的解决方案:
data PairOrNot a where
Pair :: Show b => (b,c) -> PairOrNot (b,c)
Not :: a -> PairOrNot a发布于 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 )
class Show' a where
show' :: a -> String
noOverlap :: (b :=> Show' a) => Proxy a -> Dict b在这里,noOverlap函数是一个承诺,如果你能找到一个产生实例Show' a的约束b,我就可以证明给定Show' a的b。这个承诺相当于声明将不会有Show'的重叠实例
现在,我们需要一个辅助函数来实际实现noOverlap
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 k和Dict b是相同的,但据我所知,这是对unsafeCoerce的安全使用,因为函数依赖a :=> b | b -> a确保对于给定的Show' a只能有一个k :=> Show' a实例。
现在,对于这个帮助器,下面是如何定义实例的
-- 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,如下所示:
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 #-}来编译这些代码。
发布于 2016-09-23 20:16:54
下面是user2297560的一个概括,它不需要在GADT中硬编码Show:
{-# 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然后你就可以
showFirstIfPair :: PairOrNot Show a -> String
showFirstIfPair (Not a) = show a
showFirstIfPair (Pair (b,c)) = show bhttps://stackoverflow.com/questions/39639892
复制相似问题