Блог

Речь идет об объединении двух простых арифметических операторов (двух частичных функций) с помощью Applicative и Monad . Я примерно понял это до сих пор.

 -- ┌──────────────────────────────────────┐  
-- | instance Applicative ((->) r) where  |                                           
-- |   pure = const                       |                                           
-- |   (<*>) f g x = f x (g x)            |  (1)                                          
-- |   liftA2 q f g x = q (f x) (g x)     |                                         
-- |                                      |       
-- | instance Monad ((->) r) where        |                                           
-- |   f >>= k = r -> k (f r) r          |  (2)                                                                         
-- └──────────────────────────────────────┘

λ> ( ) <*> (*2) $ 10  
  -- Type check: 
  (<*>) ::  f     (a -> b) -> f      a  -> f      b
           (-> r) (a -> b) -> (-> r) a  -> (-> r) b
           (r ->   a -> b) -> (r ->  a) -> (r ->  b)
           ---------------    ---------
           ( ) ~ f            (*2) ~ g      r ~ x (10)

  -- Actual calcuation: by (1)
  f x (g x) = ( ) 10 ((*2) 10) = ( ) 10 20 = 30 

λ> (*2) >>= ( ) $ 10  -- 30
  -- Type check: 
  (>>=) ::  m     a    ->  a  -> m     b  ->  m     b
           (-> r) a    -> (-> r) a  -> b  -> (-> r) b
           (r  -> a)   -> (a  -> r  -> b) -> (r ->  b)
           ---------      ---------------
           (*2) ~ f       ( ) ~ k             r ~ 10

  -- Actual calculation: by (2)
  k (f r) r = ( ) ((*2) 10) 10 = ( ) 20 10 = 30 
  

Но когда я попытался применить эти вещи к некоторой структуре (возможно), я застрял на этом. (Я пометил «ЗДЕСЬ» в конце строк, где я застрял.)

 -- ┌────────────────────────────────────────────────┐   
-- | instance Applicative Maybe where               |                                     
-- |     pure = Just                                |                    
-- |     Just f  <*> m       = fmap f m             |                                       
-- |     Nothing <*> _m      = Nothing              |                                      
-- |     liftA2 f (Just x) (Just y) = Just (f x y)  |                                                  
-- |     liftA2 _ _ _ = Nothing                     |                               
-- |     Just _m1 *> m2      = m2                   |                                 
-- |     Nothing  *> _m2     = Nothing              |                                      
-- |                                                |     
-- | instance  Monad Maybe  where                   |                                 
-- |     (Just x) >>= k      = k x                  |                                  
-- |     Nothing  >>= _      = Nothing              |                                      
-- |     (>>) = (*>)                                |                                                            
-- └────────────────────────────────────────────────┘

λ> Just 10 >>= return . ( 1)   -- Just 11
  -- Type check:
  (>>=) ::  m     a    ->  a  -> m     b  ->  m     b
            ----------     --------------
            Just 10        return . ( 1) :: a -> m b  
        so, m ~ Maybe, a ~ Int
  Just 10 >>= return . ( 1) :: m     b 
                               Maybe Int 
  
  -- Actual calculation:
  Just 10 >>= return . ( 1) = return . ( 1) $ 10
                            = Just   . ( 1) $ 10
                            = Just 11

λ> Just >>= return ( 1) $ 10   -- 11
  -- This is point-free style
     I don't get it.
  -- Type check:
  (>>=) ::  m     a    ->     a  -> m     b  ->  m     b
            ----------        --------------
            (-> a) (Maybe a)  m (a -> a)   <==== HERE! 
                                           I can't derive the correct type. 

  -- Actual calculation:                   <==== and HERE!
  m >>= f   = x -> f (m x) x              <==== How can this formula be derived?
            = (return ( 1)) (Just 10) 10   <==== How can this be calculated?
  

В выражении монады нет стиля без точек. Я не понял. Как я могу вывести тип и получить результат, как в предыдущих случаях простых арифметических выражений?

Большое спасибо.

Спасибо за ваш отличный ответ, Нилл. С вашей помощью я мог бы найти, что было не так в моих мыслях и коде. Но я все еще не могу правильно получить окончательный тип Just >>= return ( 1) . Я обновил свой вопрос и попытался определить его тип. Я знаю, что ошибаюсь в выводе типов. Могу ли я получить дополнительную помощь, чтобы найти неправильную часть и исправить это?

 -- Type check: Incorrect
(>>=) ::  m     a    ->     a  ->  m    b  ->  m     b
         (-> r) a    ->    (-> r)  a -> b  -> (-> r) b
         --------          --------------
         f                 k                  r -> k (f r) r
         m                 f                  r -> m (f r) r          
         (-> d) (Maybe d)  (-> r) (n -> n)
     so, a ~ Maybe d
         a ~ n, b ~ n  -- This means a, b, n are all the same type.
                       -- Character a, b can be interchangeable. 
Just >>= return ( 1) :: (-> r) b  
                      = (-> r) a          -- by `a ~ b`
                      = (-> r) (Maybe d)  -- by `a ~ Maybe d` 
                                          -- HERE: Is this right?  
                                             Should this be `(-> r) n`?
                      = a -> Maybe b      -- by changing characters
               HERE: WRONG RESULT TYPE??? It must be `a -> a` not `a -> Maybe a` 

-- Actual calcuation:
Moand instance for function (`(-> r)`) type here (I got)
m >>= f = x -> f (m x) x
        = return ( 1) (Just 10) 10
        = return ( 1) (Just 10) $ 10
        = const  ( 1) (Just 10) $ 10  -- by (1), pure = const
        = ( 1) $ 10                   -- 'Just 10' was ignored by 'const (pure)' function.
        = ( ) 10 = 11
  

Большое спасибо.

В

 Just >>= return ( 1) $ 10
  

Just является функцией r -> Maybe r , поэтому используется функциональная монада ((->) r) , дающая сокращение как

 return (1 ) (Just 10) 10
  

потому что это определение >>= для ((->) r) монады (так же, как вы дали его в верхней части вашего поста, f >>= k = r -> k (f r) r ).

Теперь return (1 ) применяется к Just 10 , так что это тоже функция,

 return :: Monad m => a          -> m        a
(1 ) :: Num m =>   n -> n
return (1 ) :: (Monad m, Num n) => m     (n -> n)
                         Num n  => (r -> (n -> n))
Just 10 :: (Num i => Maybe i) ~     r
  

Для функций, return == const , таким образом, мы имеем

 const (1 ) (Just 10) 10
===
(1 ) 10
===
11
  

Ваш другой вопрос: как получилось, что для ((->) r) монады m >>= f = x -> f (m x) x ? (вы заметили, что это то же самое, что и определение вверху f >>= k = r -> k (f r) r , вплоть до переименования некоторых переменных, верно?)

И ответ таков: потому что типы подходят:

 (>>=)    ::  m     a  -> (a -> m     b ) -> m     b
         ~   (r -> a) -> (a -> (r -> b)) -> (r -> b)
(>>=)        m           f                   x  = b
    where
        mx = m x       :: a
        f_mx = f mx    ::       r -> b
        b = f_mx x     ::            b
  

редактировать: давайте попробуем вывести тип Just >>= return ( 1) без каких-либо размышлений, просто чисто механическим способом, как это сделал бы компилятор. Мы будем использовать основное правило вывода типов, соответствующее правилу Modus Ponens в логике:

         A     :: a
     F        :: t -> b
    --------------------
     F  A     ::      b       ,  t ~ a
  

Хитрость заключается в том, чтобы использовать все переменные разных типов с самого начала, поэтому у нас даже не будет возможности их перепутать:

 -- Просто >> = возврат ( 1) === (>>=) Просто (возврат ( 1))

return :: Monad f => d -> f d 
( 1) :: Num n => n -> n
 ----------------
return ( 1) :: (Монада f, число n) => f (n -> n)
---------------------------------------------------------
(>> =) :: Monad m => m a -> (a -> m b ) -> m b 
Просто :: (->) c (Возможно, c)
 ----------------
 m ~ (->) c , a ~ Может быть c
 --------------------------
(>> =) Просто :: Monad ((->) c) => (Возможно, c -> (->) c b ) -> (->) c b
 ~ Monad ((->) c) => (Возможно, c -> (c -> b)) -> (c -> b)
 ---------------------- 
return ( 1) :: (Монада f, число n) => f (n -> n)
 ----------------------
f ~ (->) (Возможно, c) , (n -> n) ~
 (c -> b)
(>> =) Просто (возврат (1 )) ::
 (Монада ((->) c), Монада ((->) (Возможно, c)) => c -> b
 ~ Num n => n -> n