Haskell：这个公式是怎么计算出来的？ `(return (+1)) (刚好 10) 10`
Haskell: How is this formula calculated? `(return (+1)) (Just 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
但是当我试图将这些东西应用到某些结构（也许）时，我卡住了。 （我在卡住的行末标记了 'HERE'。）
-- ┌────────────────────────────────────────────────┐
-- | 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?
Monad表达式中有point-free风格。我不明白。如何像前面的简单算术表达式一样推导类型并得到结果？
非常感谢。
感谢您的精彩回答，尼尔。在您的帮助下，我可以找到我的思想和代码中的错误。但是我仍然无法正确获得 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 的 >>= 的定义（正如您在 post、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 >>= return (+1) === (>>=) Just (return (+1))
return :: Monad f => d -> f d
(+1) :: Num n => n -> n
----------------
return (+1) :: (Monad f, Num n) => f (n -> n)
---------------------------------------------------------
(>>=) :: Monad m => m a -> (a -> m b ) -> m b
Just :: (->) c (Maybe c)
----------------
m ~ (->) c , a ~ Maybe c
--------------------------
(>>=) Just :: Monad ((->) c) => (Maybe c -> (->) c b ) -> (->) c b
~ Monad ((->) c) => (Maybe c -> (c -> b)) -> (c -> b)
----------------------
return (+1) :: (Monad f, Num n) => f (n -> n)
----------------------
f ~ (->) (Maybe c) , (n -> n) ~
(c -> b)
(>>=) Just (return (1+)) ::
(Monad ((->) c), Monad ((->) (Maybe c)) => c -> b
~ Num n => n -> n
这是关于通过 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
但是当我试图将这些东西应用到某些结构（也许）时，我卡住了。 （我在卡住的行末标记了 'HERE'。）
-- ┌────────────────────────────────────────────────┐
-- | 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?
Monad表达式中有point-free风格。我不明白。如何像前面的简单算术表达式一样推导类型并得到结果？
非常感谢。
感谢您的精彩回答，尼尔。在您的帮助下，我可以找到我的思想和代码中的错误。但是我仍然无法正确获得 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 的 >>= 的定义（正如您在 post、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 >>= return (+1) === (>>=) Just (return (+1))
return :: Monad f => d -> f d
(+1) :: Num n => n -> n
----------------
return (+1) :: (Monad f, Num n) => f (n -> n)
---------------------------------------------------------
(>>=) :: Monad m => m a -> (a -> m b ) -> m b
Just :: (->) c (Maybe c)
----------------
m ~ (->) c , a ~ Maybe c
--------------------------
(>>=) Just :: Monad ((->) c) => (Maybe c -> (->) c b ) -> (->) c b
~ Monad ((->) c) => (Maybe c -> (c -> b)) -> (c -> b)
----------------------
return (+1) :: (Monad f, Num n) => f (n -> n)
----------------------
f ~ (->) (Maybe c) , (n -> n) ~
(c -> b)
(>>=) Just (return (1+)) ::
(Monad ((->) c), Monad ((->) (Maybe c)) => c -> b
~ Num n => n -> n