6

我可以写以下内容：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}

f :: Integral a => (forall b. Num b => b) -> a
f = id

一切都很好。据推测，GHC 可以从中得到Integral一切Num都很好。

我可能有点狡猾，但我仍然很好：

class Integral x => MyIntegral x
instance Integral x => MyIntegral x

class Num x => MyNum x
instance Num x => MyNum x

f' :: MyIntegral a => (forall b. MyNum b => b) -> a
f' = id

所以可以说我想概括一下，就像这样：

g :: c2 a => (forall b. c1 b => b) -> a
g = id

现在显然这会吐出假人，因为 GHC 不能派生c2自c1，因为c2不受约束。

我需要在类型签名中添加什么g才能说“您可以c2从c1”派生？

4

1 回答 1

7

该软件包通过其（“enttails”）类型constraints提供了解决此问题的方法：:-

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts

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

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

g, g' :: c2 a => c2 a :- c1 a -> (forall b. c1 b => b) -> a
g (Sub Dict) x = x

然后，通过传入适当的见证，我们可以恢复原始示例：

integralImpliesNum :: Integral a :- Num a
integralImpliesNum = Sub Dict

f :: Integral a => (forall b. Num b => b) -> a
f = g integralImpliesNum

实际上，这g只是\\运算符的翻转和专用版本：

(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
infixl 1 \\

g' = flip (\\)

如果你有时间，Edward Kmett 的演讲“Type Classes vs the World”很好地介绍了这一切是如何运作的。

于 2017-05-07T05:02:53.770 回答