约束限制

Question

我可以写：

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

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

，一切都很好。据推测GHC可以从Num派生Integral，所以一切都很好。

我可以有一些技巧，但我还是罚款：

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不能从c1派生c2，因为c2不受约束。

我需要添加到g的类型签名以说“您可以从c1中派生c2”？

Answer 1

的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 (\\) 

如果您有时间，爱德华Kmett的演讲"Type Classes vs the World"是一个很好的介绍如何这一切工作。