约束约束

Question

我可以写下面的内容:

{-# 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"？

Answer 1

该constraints软件包通过其:-("entails")类型提供了解决此问题的方法:

{-# 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"是对这一切如何运作的一个很好的介绍.