約束限制

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"是一個很好的介紹如何這一切工作。