Comment pattern match sur une monade libre universellement quantifiée?

Question

Je me demande si je peux écrire une fonction isPure :: Free f () -> Bool, qui vous indique si la monade libre donnée est égale Pure ()ou non. C'est facile à faire pour un cas simple, mais je ne peux pas le comprendre pour un cas plus complexe où il y a des contraintes sur le foncteur f.

import Control.Monad.Free

-- * This one compiles

isPure :: Free Maybe () -> Bool
isPure (Pure ()) = True
isPure _ = False

-- * This one fails to compile with "Ambiguous type variable ‘context0’ arising from a pattern
-- prevents the constraint ‘(Functor context0)’ from being solved."

{-# LANGUAGE RankNTypes #-}
type ComplexFree = forall context. (Functor context) => Free context ()

isPure' :: ComplexFree -> Bool
isPure' (Pure ()) = True
isPure' _ = False

Je peux voir pourquoi spécifier le type exact de context0serait nécessaire en général, mais tout ce que je veux, c'est regarder la structure à gros grains de la monade libre (c'est-à-dire est-ce Pureou non Pure). Je ne veux pas identifier le type parce que mon programme repose sur la transmission de certaines monades libres universellement quantifiées et je veux que cela fonctionne avec l'une d'entre elles. Y a-t-il un moyen de faire cela? Merci!

MODIFIÉ pour changer "quantifié existentiellement" -> "quantifié universellement"

EDIT: puisque mon ComplexFreetype est peut-être trop général, voici une version qui imite plus exactement ce que j'essaie de faire.

--* This one actually triggers GHC's warning about impredicative polymorphism...
{-# LANGUAGE GADTs #-}

data MyFunctor context next where
  MyFunctor :: Int -> MyFunctor context next -- arguments not important

type RealisticFree context a = Free (MyFunctor context) a

class HasFoo context where
  getFoo :: context -> Foo

class HasBar context where
  getBar :: context -> Bar

type ConstrainedRealisticFree = forall context. (HasFoo context, HasBar context) => RealisticFree context ()

processRealisticFree :: ConstrainedRealisticFree -> IO ()
processRealisticFree crf = case isPure'' crf of
  True -> putStrLn "It's pure!"
  False -> putStrLn "Not pure!"

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' = undefined -- ???

(Pour un peu plus de contexte, cette monade gratuite est destinée à modéliser un interprète pour une langue simple, où un «contexte» est présent. Vous pouvez considérer le contexte comme décrivant une monade de lecteur dans laquelle la langue est évaluée, donc HasFoo contextet HasBar contextimposer que a Fooet Barsont disponibles. J'utilise la quantification universelle pour que le type exact du contexte puisse varier. Mon objectif est de pouvoir identifier un "programme vide" dans cet interpréteur de monades gratuit.)

Answer 1

Je vais répondre à votre question remaniée ici. Il s'avère que la réponse est toujours fondamentalement la même que celle de luqui: vous devez instancier l'argument polymorphe avant de pouvoir effectuer une correspondance de motif. Grâce à la contrainte, vous devez utiliser un type de contexte qui est une instance des classes pertinentes. S'il n'est pas pratique d'en utiliser un "vrai", vous pouvez facilement en faire un jetable:

data Gump = Gump Foo Bar

instance HasFoo Gump where
  getFoo (Gump f _) = f

instance HasBar Gump where
  getBar (Gump _ b) = b

Cela devrait convenir à ce cas particulier. Cependant, dans la plupart des situations pratiques similaires, vous souhaiterez instancier votre type réel pour obtenir son comportement spécialisé.

Vous pouvez maintenant instancier le contexte Gumpet vous êtes prêt à partir:

isPure'' :: ConstrainedRealisticFree -> Bool
isPure'' q = case q :: RealisticFree Gump () of
  Pure _ -> True
  Free _ -> False

La raison pour laquelle vous avez cette erreur sur les types imprédicatifs est que vous avez écrit

isPure'' = ...

Les paramètres polymorphes de rang supérieur doivent généralement être des paramètres syntaxiques :

isPure'' q = ...

Answer 2

Tout d'abord, ce n'est pas une quantification existentielle. Cela ressemblerait à ceci:

data ComplexFree = forall context. (Functor context) => ComplexFree (Free context ())

(une syntaxe que je trouve plutôt déroutante, donc je préfère la forme GADT

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree 

, ce qui signifie la même chose)

Vous avez ici un type universellement quantifié , c'est-à-dire que si vous avez une valeur de type ComplexFree(la façon dont vous l'avez écrite), elle peut se transformer en une monade gratuite sur n'importe quel foncteur de votre choix. Ainsi, vous pouvez simplement l'instancier à Identity, par exemple

isPure' :: ComplexFree -> Bool
isPure' m = case m :: Free Identity () of 
                Pure () -> True
                _       -> False

Il doit être instancié à un certain type afin de l'inspecter, et l'erreur que vous voyez est que le compilateur n'a pas pu décider quel foncteur utiliser par lui-même.

Cependant, l'instanciation n'est pas nécessaire pour la définition isPure'. En ignorant les fonds ¹ , l'un des foncteurs avec lesquels vous pouvez instancier ComplexFreeest Const Void, ce qui signifie que le cas récursif de se Freeréduit à

f (m a)
  = Const Void (m a)
 ~= Void

c'est-à-dire que c'est impossible. Par certains arguments de naturalité, nous pouvons montrer que la branche prise par un ComplexFreene peut pas dépendre du choix du foncteur, ce qui signifie que tout élément entièrement défini ComplexFreedoit être un Pure. Nous pouvons donc "simplifier"

isPure' :: ComplexFree -> Bool
isPure' _ = True

Quel ennui.

---

Cependant, je soupçonne que vous avez peut-être commis une erreur de définition ComplexFree, et vous voulez vraiment la version existentielle?

data ComplexFree where
    ComplexFree :: (Functor context) => Free context () -> ComplexFree

Dans ce cas, un ComplexFree"porte" le foncteur avec lui. Cela ne fonctionne que pour un foncteur, et il (et lui seul ) sait de quel foncteur il s'agit. Ce problème est mieux formé et mis en œuvre comme vous vous en doutez

isPure' :: ComplexFree -> Bool
isPure' (ComplexFree (Pure _)) = True
isPure' _ = False

---

¹ Ignorer le fond est une pratique courante et généralement pas problématique. Cette réduction augmente strictement le contenu informationnel du programme - c'est-à-dire que chaque fois que la version originale a donné une réponse définie, la nouvelle version donnera la même réponse. Mais le nouveau pourrait «ne pas entrer dans une boucle infinie» et donner accidentellement une réponse à la place. Dans tous les cas, cette réduction peut être modifiée pour être complètement correcte, et le résultat isPure'est tout aussi inutile.