约束约束

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 的类型签名中添加什么来表示 "you can derive c2 from 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" 很好地介绍了这一切是如何运作的。

约束约束

Constraining constraints

haskell

ghc

constraint-kinds