Poprawność niejawna podnoszenia

Question

Wyobraź sobie, że mam wartość, która jest nazwą rodzajową nad monady:

m :: (Monad m) => m A -- 'A' is some concrete type 

Teraz powiedzmy, że specjalizuję się tę wartość do konkretnego transformatora monada stosie w dwóch odrębnych sposobów:

m1 :: T M A 
m1 = m 

m2 :: T M A 
m2 = lift m 

... gdzie M i T M są monady i T jest transformator monada:

instance Monad M where ... 
instance (Monad m) => Monad (T m) where ... 
instance MonadTrans T where ... 

... a te przykłady są zgodne z prawami monad i monadowymi prawami transformatora.

możemy wywnioskować, że:

m1 = m2 

... nie wiedząc nic o m innego niż tego typu?

To tylko długotrwały sposób na pytanie, czy lift m jest prawidłowym zamiennikiem dla m, zakładając, że oba typy kontroli. Jest trochę trudniej sformułować pytanie, ponieważ wymaga ono sprawdzenia typu jako dwie oddzielne monady przed i po podstawieniu. O ile mogę powiedzieć, jedynym sposobem takiego sprawdzenia typu byłoby sprawdzenie, czy m jest generyczne nad monadą.

Moja mglista intuicja jest taka, że ​​podstawienie powinno być zawsze poprawne, ale nie jestem pewien, czy moja intuicja jest poprawna, ani jak to udowodnić, jeśli jest prawidłowa.

Answer 1

Jeśli m :: Monad m => m A, następnie m musi być równoważna return x jakiegoś x :: A, ponieważ jedynymi sposobami trzeba dostać nic :: m x są return i (>>=). Ale aby użyć (>>=), musisz być w stanie wyprodukować jakieś m y, które możesz zrobić z return lub z inną aplikacją (>>=). Tak czy inaczej, musisz ostatecznie użyć return, a prawa Monady gwarantują, że całe wyrażenie będzie równoznaczne z return x.

(Jeśli m jest całkowicie polimorficzny nad monady, to musi w stanie wykorzystać go w m ~ Identity, więc nie można używać żadnych fantazyjnych sztuczek monady, chyba że przejdzie mu argument. Tego rodzaju trik stosowany jest np here i here.)

Biorąc pod uwagę, że m = return x, wiemy przez monad transformatory prawa (lift . return = return), że lift m = m.

Oczywiście dotyczy to tylko tego konkretnego typu. Jeśli masz, powiedzmy, m :: MonadState S m => m A, wtedy m może z łatwością różnić się od lift m - na przykład z typem takim jak StateT A (State A) A, get i lift get będzie inny.

(i oczywiście to wszystko jest ignorowanie ⊥. Potem znowu, jeśli nie większość monady nie przestrzegać prawa w każdym razie).

Answer 2

Wierzę, że to jest niechlujny inductive proof że jest m odpowiednik lift m.

Myślę, że musimy spróbować dowieść czegoś o m (lub raczej o wszystkich możliwych wartościach typu (Monad m) => m A). Jeśli weźmiemy pod uwagę Monad jako składające się z wiązania i wrócić tylko i ignorować dno i fail wówczas koniecznością na najwyższym poziomie m być jednym z:

mA = return (x) 
mB = (mX >>= f) 

Dla mA dwie formy m są równoważne prawu transformatora monada :

lift (return (x)) = return (x) 

To jest podstawowy przypadek. Wtedy jesteśmy w lewo z drugiego prawa transformatora rozumować o mB:

lift (mX >>= f) = lift mX >>= (lift . f) 

i gdzie chcielibyśmy udowodnić, że nasza mB jest równa tej ekspansji:

mX >>= f = lift mX >>= (lift . f) 

Zakładamy, że lewa strona wiązania jest równoważna (mX = lift mX), ponieważ jest to nasza hipoteza indukcyjna (prawda?).

Więc jesteśmy w lewo, aby udowodnić f = lift . f przez zastanawianie się, co f musi wyglądać następująco:

f :: a -> m b 
f = \a -> (one of our forms mA or mB) 

i lift . f wygląda następująco:

f = \a -> lift (one of our forms mA or mB) 

Który pozostawia nas z powrotem z naszej hipotezy:

m = lift m