Haskell : Contrainte d'égalité dans une instance

Question

Je lisais l'annonce de ClassyPrelude et on en est arrivé là :

instance (b ~ c, CanFilterFunc b a) => CanFilter (b -> c) a where
    filter = filterFunc

L'écrivain a alors mentionné que cela ne fonctionnerait pas :

instance (CanFilterFunc b a) => CanFilter (c -> c) a where
    filter = filterFunc

Ce qui est logique pour moi, car c n'est absolument pas liée à la contrainte de gauche.

Cependant, ce qui n'est pas mentionné dans l'article et ce que je ne comprends pas, c'est pourquoi cela ne fonctionnerait pas :

instance (CanFilterFunc b a) => CanFilter (b -> b) a where
    filter = filterFunc

Quelqu'un pourrait-il expliquer pourquoi cette définition est différente de la première ? Peut-être qu'un exemple concret d'inférence de type GHC serait utile ?

Answer 1

Michael a déjà donné une bonne explication dans son article de blog, mais je vais essayer de l'illustrer avec un exemple (artificiel, mais relativement petit).

Nous avons besoin des extensions suivantes :

{-# LANGUAGE FlexibleInstances, TypeFamilies #-}

Définissons une classe qui est plus simple que CanFilter avec un seul paramètre. Je définis deux copies de la classe, car je veux démontrer la différence de comportement entre les deux instances :

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

Maintenant, définissons une instance pour chaque classe. Pour Twice1 nous fixons les variables de type pour qu'elles soient directement les mêmes, et pour Twice2 nous leur permettons d'être différents, mais nous ajoutons une contrainte d'égalité.

instance Twice1 (a -> a) where
  twice1 f = f . f

instance (a ~ b) => Twice2 (a -> b) where
  twice2 f = f . f

Afin de montrer la différence, définissons une autre fonction surchargée comme ceci :

class Example a where
  transform :: Int -> a

instance Example Int where
  transform n = n + 1

instance Example Char where
  transform _ = 'x'

Nous en sommes maintenant à un point où nous pouvons voir une différence. Une fois que nous avons défini

apply1 x = twice1 transform x
apply2 x = twice2 transform x

et demander à GHC les types déduits, nous obtenons que

apply1 :: (Example a, Twice1 (Int -> a)) => Int -> a
apply2 :: Int -> Int

Pourquoi ? Eh bien, l'instance pour Twice1 ne se déclenche que lorsque le type source et le type cible de la fonction sont identiques. Pour transform et le contexte donné, nous ne le savons pas. GHC n'appliquera une instance que lorsque le côté droit correspondra, donc nous restons avec le contexte non résolu. Si nous essayons de dire apply1 0 il y aura une erreur de type indiquant qu'il n'y a pas encore assez d'informations pour résoudre la surcharge. Nous devons spécifier explicitement que le type de résultat doit être Int dans ce cas pour passer.

Cependant, en Twice2 l'instance est pour tout type de fonction. GHC la résoudra immédiatement (GHC ne revient jamais en arrière, donc si une instance correspond clairement, elle est toujours choisie), et essaiera ensuite d'établir les préconditions : dans ce cas, la contrainte d'égalité, qui force alors le type de résultat à être Int et nous permet de résoudre le Example contrainte, aussi. Nous pouvons dire apply2 0 sans autres annotations de type.

Il s'agit donc d'un point assez subtil concernant la résolution d'instance de GHC, et la contrainte d'égalité ici aide le vérificateur de type de GHC d'une manière qui nécessite moins d'annotations de type par l'utilisateur.

Answer 2

Pour compléter la réponse de @kosmikus

La même chose s'applique à purescript - vous avez besoin de la contrainte d'égalité pour dériver le type correctement (vous pouvez essayer ici http://try.purescript.org )

module Main where

import Prelude

-- copied from https://github.com/purescript/purescript-type-equality/blob/master/src/Type/Equality.purs
class TypeEquals a b | a -> b, b -> a where
  to :: a -> b
  from :: b -> a

instance refl :: TypeEquals a a where
  to a = a
  from a = a

-----------------

class Twice1 f where
  twice1 :: f -> f

class Twice2 f where
  twice2 :: f -> f

instance mytwice1 :: Twice1 (a -> a) where
  twice1 f = f >>> f

instance mytwice2 :: TypeEquals a b => Twice2 (a -> b) where
  twice2 f = f >>> from >>> f

class Example a where
  transform :: Int -> a

instance exampleInt :: Example Int where
  transform n = n + 1

instance exampleChar :: Example Char where
  transform _ = 'x'

{--
-- will raise error
--   No type class instance was found for Main.Twice1 (Int -> t1)

apply1 x = twice1 transform x

-- to resolve error add type declaration
apply1 :: Int -> Int

--}

-- compiles without error and manual type declaration, has type Int -> Int automatically
apply2 x = twice2 transform x

---

Mais à Idris, vous ne pouvez pas

module Main

import Prelude

interface Twice f where
  twice : f -> f

Twice (a -> a) where
  twice f = f . f

interface Example a where
  transform : Int -> a

Example Int where
  transform n = n + 1

Example Char where
  transform _ = 'x'

-- run in REPL to see that it derives properly:

-- $ idris src/15_EqualityConstraint_Twice_class.idr
-- *src/15_EqualityConstraint_Twice_class> :t twice transform
-- twice transform : Int -> Int

-- Summary:
-- in idris you dont need equality constaint to derive type of such functions properly