Haskell——双向类实例类型含义或 GADT 存在类型限定?

发布于 2024-11-04 00:44:50 字数 1178 浏览 4 评论 0原文

我有一个像(缩写)这样定义的 GADT,

{-# LANGUAGE StandaloneDeriving #-}
data D t where
    C :: t -> D t
    R :: D b -> D (Either a b)
deriving instance Show t => Show (D t)

编译器正确地抱怨它无法为 R 派生 Show。在这种情况下,我们有(任一 ab)属于 Show 类,但我们无法知道这是真的 iff b属于Show类。错误消息是,

Could not deduce (Show b) from the context (t ~ Either a b)
  arising from a use of `showsPrec' at tmp.hs:37:0-37
Possible fix: add (Show b) to the context of the constructor `R'
In the second argument of `(.)', namely `(showsPrec 11 b1)'
In the second argument of `showParen', namely
    `((.) (showString "R ") (showsPrec 11 b1))'
In the expression:
    showParen ((a >= 11)) ((.) (showString "R ") (showsPrec 11 b1))
When typechecking a standalone-derived method for `Show (D t)':
  showsPrec a (C b1)
              = showParen ((a >= 11)) ((.) (showString "C ") (showsPrec 11 b1))
  showsPrec a (R b1)
              = showParen ((a >= 11)) ((.) (showString "R ") (showsPrec 11 b1))

似乎需要能够对存在类型进行限定,对于存在类型 b 可以说“Show b => Show (D (Either ab))”,或者升级含义“(Show a, Show b) => Show (Either ab)" 所以它是双向的。

非常感谢!

(请随意清理标题或描述。)

I have a GADT defined like (abbreviated),

{-# LANGUAGE StandaloneDeriving #-}
data D t where
    C :: t -> D t
    R :: D b -> D (Either a b)
deriving instance Show t => Show (D t)

The compiler correctly complains that it cannot derive Show for R. In this case, we have that (Either a b) is of class Show, but we can't know that this is true iff b is of class Show. The error message is,

Could not deduce (Show b) from the context (t ~ Either a b)
  arising from a use of `showsPrec' at tmp.hs:37:0-37
Possible fix: add (Show b) to the context of the constructor `R'
In the second argument of `(.)', namely `(showsPrec 11 b1)'
In the second argument of `showParen', namely
    `((.) (showString "R ") (showsPrec 11 b1))'
In the expression:
    showParen ((a >= 11)) ((.) (showString "R ") (showsPrec 11 b1))
When typechecking a standalone-derived method for `Show (D t)':
  showsPrec a (C b1)
              = showParen ((a >= 11)) ((.) (showString "C ") (showsPrec 11 b1))
  showsPrec a (R b1)
              = showParen ((a >= 11)) ((.) (showString "R ") (showsPrec 11 b1))

It seems that one needs to be able to qualify over the existential type, saying something like "Show b => Show (D (Either a b))" for existential types b, or upgrade the implication "(Show a, Show b) => Show (Either a b)" so it is bidirectional.

Thanks very much!

(Please feel free to clean up the title or description.)

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(1

风柔一江水 2024-11-11 00:44:50

Show 约束添加到存在性中,

data D t where
    C :: t -> D t
    R :: Show b => D b -> D (Either a b)

然后您就可以开始工作了。

Prelude> :r
[1 of 1] Compiling A                ( A.hs, interpreted )
Ok, modules loaded: A.
*A> R (C 7)
R (C 7)

Add the Show constraint to the existential,

data D t where
    C :: t -> D t
    R :: Show b => D b -> D (Either a b)

and you're in business.

Prelude> :r
[1 of 1] Compiling A                ( A.hs, interpreted )
Ok, modules loaded: A.
*A> R (C 7)
R (C 7)
~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文