contraintes Contraindre

Question

Je peux écrire ce qui suit:

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

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

Et tout est bon. Vraisemblablement GHC peut dériver Integral de Num alors tout va bien.

Je peux être un peu Tricker, mais je suis toujours très bien:

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 

permet donc de dire que je veux généraliser cela, comme ceci:

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

Maintenant, évidemment, cela va cracher le factice, car GHC ne peut pas dériver c2 de c1, comme c2 n'est pas contraint.

Que dois-je ajouter à la signature de type g pour dire que "vous pouvez dériver c2 de c1"?

Answer 1

Le paquet constraints fournit une solution à ce problème, via ses :- ("impose") type:

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

Puis, en passant un témoin approprié, nous pouvons récupérer l'exemple d'origine:

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

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

En fait, ce g est simplement une version Flipped et spécialisée de l'opérateur \\:

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

g' = flip (\\) 

Si vous avez le temps, la conversation d'Edward Kmett "Type Classes vs the World" est une excellente introduction à la façon dont tout cela fonctionne.