Istanza MonadFix per Put

Question

Una semplice domanda, spero: il pacchetto binary definisce due tipi, Get and Put. Il primo è essenzialmente una monade di stato, e il secondo è essenzialmente uno scrittore. Sia lo stato che lo scrittore hanno istanze ragionevoli MonadFix, quindi mi aspetterei che lo sarebbero anche Get e Put.

Get fa. Put no. Quindi, è possibile definire un'istanza appropriata MonadFix per Put (in realtà per PutM)?

Una domanda più generica è: come si verifica normalmente che un'istanza di classe tipo soddisfi effettivamente le leggi di tale classe?

Answer 1

Come si può vedere nell'origine del pacchetto binario (Data.Binary.Put:71), la struttura dati utilizzata per i valori monadici è rigorosa nel builder. Poiché l'estrazione del valore dalla monade deve forzare la struttura in cui viene trovato il valore, ciò causerà un ciclo infinito se il builder dipende dall'input.

data PairS a = PairS a !Builder 
newtype PutM a = Put { unPut :: PairS a } 

Così si potrebbe scrivere un esempio MonadFix, ma non sarebbe in grado di fare qualcosa di utile con esso. Ma non penso che tu possa fare qualcosa di utile con lo MonadFix qui, almeno niente che non potresti fare con il semplice vecchio fix, dal momento che la monade PutM è fondamentalmente Writer Builder (ma con un'implementazione specializzata).

Per quanto riguarda la seconda domanda, non è correlata alla prima, quindi è necessario porsi come una domanda separata.

Answer 2

Ecco una risposta alla tua seconda domanda e un seguito al commento di Daniel. Di verificare le leggi a mano e userò l'esempio dei Functor leggi per Maybe:

-- First law 
fmap id = id 

-- Proof 
fmap id 
= \x -> case x of 
    Nothing -> Nothing 
    Just a -> Just (id a) 
= \x -> case x of 
    Nothing -> Nothing 
    Just a -> Just a 
= \x -> case x of 
    Nothing -> x 
    Just a -> x 
= \x -> case x of 
    _ -> x 
= \x -> x 
= id 

-- Second law 
fmap f . fmap g = fmap (f . g) 

-- Proof 
fmap f . fmap g 
= \x -> fmap f (fmap g x) 
= \x -> fmap f (case x of 
    Nothing -> Nothing 
    Just a -> Just (f a)) 
= \x -> case x of 
    Nothing -> fmap f Nothing 
    Just a -> fmap f (Just (g a)) 
= \x -> case x of 
    Nothing -> Nothing 
    Just a -> Just (f (g a)) 
= \x -> case x of 
    Nothing -> Nothing 
    Just a -> Just ((f . g) a) 
= \x -> case x of 
    Nothing -> fmap (f . g) Nothing 
    Just a -> fmap (f . g) (Just a) 
= \x -> fmap (f . g) (case x of 
    Nothing -> Nothing 
    Just a -> Just a) 
= \x -> fmap (f . g) (case x of 
    Nothing -> x 
    Just a -> x) 
= \x -> fmap (f . g) (case x of 
    _ -> x) 
= \x -> fmap (f . g) x 
= fmap (f . g) 

Ovviamente ho potuto saltato un sacco di quei passi, ma volevo solo precisare la prova completa. Provare questo tipo di leggi è difficile all'inizio finché non ne prendi il controllo, quindi è una buona idea iniziare lento e pedante e poi, una volta migliorato, puoi iniziare a combinare passaggi e persino a fare un po 'in testa dopo un po' per semplificare quelli.