哈斯克尔:这个公式是怎么计算的`(return(+1))(仅10)10`



这是关于由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,因此使用函数monad((->) r),将其简化为

return (1+) (Just 10) 10

因为这是((->) r)monad的>>=的定义(正如您在文章顶部给出的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)monad,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

edit:让我们试着像编译器一样,不假思索地推导Just >>= return (+1)的类型。我们将使用类型推导的主要规则,对应于逻辑中的Modus-Ponens规则:

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

诀窍是从一开始就使用所有不同类型的变量,这样我们甚至没有机会将它们混合在一起:

--Just>>=返回(+1(===(>>=(Just(返回(+1((return::Monad f=>d->f d(+1(::Num n=>n->n----------------return(+1(::(Monad f,Num n(=>f(n->n(---------------------------------------------------------(>>=(::莫纳德m=>m a->(a->m b(->m b只是:(->(c(也许c(----------------m~(->(c,a~也许c--------------------------(>>=(只是::莫纳德((->(c(=>(也许c->(->(cb(->cb~莫纳德((->(c(=>(可能是c->(c->b((->(c->c(----------------------return(+1(::(Monad f,Num n(=>f(n->n(--------------------f~(->((可能是c(,(n->n(~(c->b((>>=(仅(return(1+((:(莫纳德((->(c(,莫纳德(【->】(可能是c((=>c->b~Num n=>n->n

最新更新