Depuis que j'ai posté mon réponse précédente vous avez indiqué que cela ne vous dérangeait pas de changer votre définition de PT . Je suis heureux de vous annoncer qu'en assouplissant cette restriction, la réponse à votre question passe de pas de à oui ! J'ai déjà fait valoir que vous devez indexer votre monade par l'ensemble des types dans votre support de stockage, alors voici un code fonctionnel montrant comment le faire. (A l'origine, j'avais prévu de modifier ma réponse précédente, mais elle est devenue trop longue, alors nous y voilà).
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}
import Prelude
Nous allons avoir besoin d'une plus intelligente Monad classe que celle du prélude : celle des des choses indexées de type monade décrivant les chemins à travers un graphe dirigé. Pour des raisons qui devraient devenir évidentes, je vais également définir des foncteurs indexés.
class FunctorIx f where
imap :: (a -> b) -> f i j a -> f i j b
class FunctorIx m => MonadIx m where
ireturn :: a -> m i i a
(>>>=) :: m i j a -> (a -> m j k b) -> m i k b
(>>>) :: MonadIx m => m i j a -> m j k b -> m i k b
ma >>> mb = ma >>>= \_ -> mb
replicateM_ :: MonadIx m => Int -> m i i a -> m i i ()
replicateM_ 0 _ = ireturn ()
replicateM_ n m = m >>> replicateM_ (n - 1) m
Une monade indexée utilise le système de types pour suivre la progression d'un calcul avec état. m i j a est un calcul monadique qui nécessite un état d'entrée de i change l'état en j et produit une valeur de type a . Séquençage des monades indexées avec >>>= c'est comme jouer aux dominos. Vous pouvez alimenter un calcul qui prend l'état de i à j dans un calcul qui va de j à k et obtenir un calcul plus important de i à k . (Il existe une version plus riche de cette monade indexée décrite dans le document Flèches Kleisli de la fortune outrageante ( et ailleurs ) mais celui-ci est bien suffisant pour nos besoins).
Une possibilité avec MonadIx est un File qui suit l'état d'un handle de fichier, vous assurant ainsi de ne pas oublier de libérer des ressources. fOpen :: File Closed Open () part d'un fichier fermé et l'ouvre, fRead :: File Open Open String renvoie le contenu d'un fichier ouvert, et fClose :: File Open Closed () fait passer un fichier d'ouvert à fermé. Le site run L'opération prend un calcul de type File Closed Closed a ce qui garantit que vos poignées de fichiers sont toujours nettoyées.
Mais je m'égare : ici, nous ne sommes pas concernés par un identifiant de fichier mais par un ensemble d'"emplacements mémoire" typés ; les types des éléments de la banque mémoire de la machine virtuelle sont ceux que nous utiliserons pour les indices de la monade. J'aime que mes monades "programme/interprète" soient de type gratuitement parce qu'il exprime le fait que les résultats se trouvent à la fin d'un calcul, et favorise la composabilité et la réutilisation du code, donc voici le foncteur qui produira PT quand on le branche sur FreeIx ci-dessous :
data PTF ref as bs r where
MkRef_ :: a -> (ref (a ': as) a -> r) -> PTF ref as (a ': as) r
GetRef_ :: ref as a -> (a -> r) -> PTF ref as as r
PutRef_ :: a -> ref as a -> r -> PTF ref as as r
instance FunctorIx (PTF ref) where
imap f (MkRef_ x next) = MkRef_ x (f . next)
imap f (GetRef_ ref next) = GetRef_ ref (f . next)
imap f (PutRef_ x ref next) = PutRef_ x ref (f next)
PTF est paramétrée par le type de référence ref :: [*] -> * -> * - Les références sont autorisées à connaître les types présents dans le système - et indexés par la liste des types stockés dans la "mémoire" de l'interpréteur. Le cas intéressant est MkRef_ : faire une nouvelle référence ajoute une valeur de type a à la mémoire, en prenant as à a ': as ; la suite attend un ref dans l'environnement étendu. Les autres opérations ne modifient pas la liste des types dans le système.
Lorsque je crée des références de manière séquentielle ( x <- mkRef 1; y <- mkRef 2 ), ils seront de différents types : le premier sera une ref (a ': as) a et le second sera un ref (b ': a ': as) b . Pour que les types s'alignent, j'ai besoin d'un moyen d'utiliser une référence dans un environnement plus grand que celui dans lequel elle a été créée. En général, cette opération dépend du type de référence, donc je vais la mettre dans une classe.
class Expand ref where
expand :: ref as a -> ref (b ': as) a
Une généralisation possible de cette classe engloberait le modèle d'applications répétées de expand avec un type comme inflate :: ref as a -> ref (bs :++: as) a .
Voici un autre élément réutilisable de l'infrastructure, le monade libre indexée Je l'ai déjà mentionné. FreeIx transforme un foncteur indexé en une monade indexée en fournissant une opération de jonction alignée sur le type. Free qui noue le nœud récursif dans le paramètre du foncteur, ainsi qu'une opération sans effet. Pure .
data FreeIx f i j a where
Pure :: a -> FreeIx f i i a
Free :: f i j (FreeIx f j k a) -> FreeIx f i k a
lift :: FunctorIx f => f i j a -> FreeIx f i j a
lift f = Free (imap Pure f)
instance FunctorIx f => MonadIx (FreeIx f) where
ireturn = Pure
Pure x >>>= f = f x
Free love {- , man -} >>>= f = Free $ imap (>>>= f) love
instance FunctorIx f => FunctorIx (FreeIx f) where
imap f x = x >>>= (ireturn . f)
L'un des inconvénients des monades libres réside dans le langage standard que vous devez écrire pour faire de la monade un outil de gestion de la qualité. Free et Pure plus facile à travailler. Voici quelques armes à simple action PT qui constituent la base de l'API de la monade, et quelques synonymes de modèle pour cacher le Free lorsque nous déballons PT valeurs.
type PT ref = FreeIx (PTF ref)
mkRef :: a -> PT ref as (a ': as) (ref (a ': as) a)
mkRef x = lift $ MkRef_ x id
getRef :: ref as a -> PT ref as as a
getRef ref = lift $ GetRef_ ref id
putRef :: a -> ref as a -> PT ref as as ()
putRef x ref = lift $ PutRef_ x ref ()
pattern MkRef x next = Free (MkRef_ x next)
pattern GetRef ref next = Free (GetRef_ ref next)
pattern PutRef x ref next = Free (PutRef_ x ref next)
C'est tout ce dont nous avons besoin pour être en mesure d'écrire PT les calculs. Voici votre fib exemple. J'utilise RebindableSyntax et en redéfinissant localement les opérateurs de la monade (en leurs équivalents indexés) de façon à ce que je puisse utiliser do sur ma monade indexée.
-- fib adds two Ints to an arbitrary environment
fib :: Expand ref => Int -> PT ref as (Int ': Int ': as) Int
fib n = do
rold' <- mkRef 0
rnew <- mkRef 1
let rold = expand rold'
replicateM_ n $ do
old <- getRef rold
new <- getRef rnew
putRef new rold
putRef (old+new) rnew
getRef rold
where (>>=) = (>>>=)
(>>) = (>>>)
return :: MonadIx m => a -> m i i a
return = ireturn
fail :: MonadIx m => String -> m i j a
fail = error
Cette version de fib ressemble exactement à celui que vous vouliez écrire dans la question originale. La seule différence (à part les liaisons locales de >>= et ainsi de suite) est l'appel à expand . Chaque fois que vous créez une nouvelle référence, vous devez expand tous les anciens, ce qui est un peu fastidieux.
Enfin, nous pouvons terminer le travail que nous avons entrepris et construire un PT -machine qui utilise un Tuple comme support de stockage et Elem comme type de référence.
infixr 5 :>
data Tuple as where
E :: Tuple '[]
(:>) :: a -> Tuple as -> Tuple (a ': as)
data Elem as a where
Here :: Elem (a ': as) a
There :: Elem as a -> Elem (b ': as) a
(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! There ix = xs ! ix
updateT :: Elem as a -> a -> Tuple as -> Tuple as
updateT Here x (y :> ys) = x :> ys
updateT (There ix) x (y :> ys) = y :> updateT ix x ys
Pour utiliser un Elem dans un tuple plus grand que celui pour lequel vous l'avez construit, vous devez juste le faire regarder plus bas dans la liste.
instance Expand Elem where
expand = There
Notez que ce déploiement de Elem est un peu comme un indice de Bruijn : les variables les plus récemment liées ont des indices plus petits.
interp :: PT Elem as bs a -> Tuple as -> a
interp (MkRef x next) tup = let newTup = x :> tup
in interp (next $ Here) newTup
interp (GetRef ix next) tup = let x = tup ! ix
in interp (next x) tup
interp (PutRef x ix next) tup = let newTup = updateT ix x tup
in interp next newTup
interp (Pure x) tup = x
Lorsque l'interprète rencontre un MkRef demande, il augmente la taille de sa mémoire en ajoutant x à l'avant. Le vérificateur de caractères vous rappellera que toute ref d'avant le MkRef doivent être correctement expand ed, de sorte que les références existantes ne soient pas déréglées lorsque le tuple change de taille. Nous avons payé pour un interprète sans casts non sécurisés, mais nous avons obtenu l'intégrité référentielle pour démarrer.
Pour fonctionner à partir d'un départ arrêté, il faut que le PT Le calcul s'attend à commencer avec une banque de mémoire vide, mais nous lui permettons de se terminer dans n'importe quel état.
run :: (forall ref. Expand ref => PT ref '[] bs a) -> a
run x = interp x E
Il vérifie les caractères, mais est-ce que ça marche ?
ghci> run (fib 5)
5
ghci> run (fib 3)
2
