撰写功能组合:(。)。(。)如何工作? [英] Composing function composition: How does (.).(.) work?

查看:121
本文介绍了撰写功能组合:(。)。(。)如何工作?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

(。)有两个函数,它们带一个一个值并返回一个值:

<。pre> (。)::(b - > c) - > (a - > b) - > a - > c

由于(。)需要两个参数,我觉得(。)。(。)应该是无效的,但它非常好:


$ b (。)。(。)::(b - > c) - >> $ b

  (a→a1→b)→> a  - > a1  - > c 

这是怎么回事?我意识到这个问题措辞严厉......所有功能真的只需要一个参数就可以感谢柯里化。也许更好的方式来说这是类型不匹配。

解决方案

让我们先玩typechecker机械证明。



我想将(。)应用于(。),然后将(。)应用于结果。第一个应用程序可以帮助我们定义变量的一些等价。

 ((。)::(b  - > c) - >(a→b)→a→c)
((。)::(b'→c')→(a'→b') - > a'→c')
((。)::(b - > c) - >(a - > b) - > a' ' - > c'')

让b =(b' - > c')
c =(a' - > b') - > a' - > ((。)(。)::(a - > b) - > a - > c)
((。)::(b'' - > c') - >(a - > b) - > a - > c')

然后我们开始第二次,但很快就卡住了......

  let a =(b'' - > c'')

这是关键:我们希望 let b =(a'' - > b'') - > a - > c'',但我们已经定义了 b ,所以我们必须尝试 unify ---以匹配我们最好的两个定义。幸运的是,他们匹配

  UNIFY b =(b' - > c')=: =(a - > b) - > a - > c''
这意味着
b'= a'' - > b''
c'= a'' - > c''

以及这些定义/统一我们可以继续申请$ b $ ((。)(。)(。)::(b'' - > c') - >(a' - > b ') - >(a' - > c'))

然后展开

((。)(。)(。)::(b'' - > c') - >(a' - (a' - > a'' - > c'))

并将其清除

 替代b'' - > b 
c'' - > c
a' - > a
a'' - > a1

(。)。(。)::(b - > c) - > (a→a1→b)→> (a - > a1 - > c)

说实话,一个违反直觉的结果。




这是直觉。首先看看 fmap

  fmap ::(a  - > ; b) - > (fa  - > fb)

它将函数提升为函子。我们可以反复应用

  fmap.fmap.fmap ::(Functor f,Functor g,Functor h)
=> (a - > b) - > (f(g(ha)) - > f(g(hb)))

允许我们将函数提升到更深层次的 Functors



事实证明,数据类型(r - >)是一个 Functor

  instance Functor(( - >)r)其中
fmap =(。)

这应该看起来很熟悉。这意味着 fmap.fmap 转换为<.c $ c>(。)。(。)。因此,(。)。(。)就是让我们转换(r - >)的深层和深层参数类型 Functor (r - >) Functor 实际上是 Reader Monad ,所以分层 Reader s就像拥有多个独立的全局不变状态。



或者像有多个输入参数不受 fmap ing影响。有点像在(> 1)参数函数的只是结果上组成一个新的继续函数。






最后值得注意的是,如果你认为这些东西很有趣,它就构成了派生Control.Lens镜头


(.) takes two functions that take one value and return a value:

(.) :: (b -> c) -> (a -> b) -> a -> c

Since (.) takes two arguments, I feel like (.).(.) should be invalid, but it's perfectly fine:

(.).(.) :: (b -> c) -> (a -> a1 -> b) -> a -> a1 -> c

What is going on here? I realize this question is badly worded...all functions really just take one argument thanks to currying. Maybe a better way to say it is that the types don't match up.

解决方案

Let's first play typechecker for the mechanical proof. I'll describe an intuitive way of thinking about it afterward.

I want to apply (.) to (.) and then I'll apply (.) to the result. The first application helps us to define some equivalences of variables.

((.) :: (b -> c) -> (a -> b) -> a -> c) 
      ((.) :: (b' -> c') -> (a' -> b') -> a' -> c') 
      ((.) :: (b'' -> c'') -> (a'' -> b'') -> a'' -> c'')

let b = (b' -> c') 
    c = (a' -> b') -> a' -> c'

((.) (.) :: (a -> b) -> a -> c) 
      ((.) :: (b'' -> c'') -> (a'' -> b'') -> a'' -> c'')

Then we begin the second, but get stuck quickly...

let a = (b'' -> c'')

This is key: we want to let b = (a'' -> b'') -> a'' -> c'', but we already defined b, so instead we must try to unify --- to match up our two definitions as best we can. Fortunately, they do match

UNIFY b = (b' -> c') =:= (a'' -> b'') -> a'' -> c''
which implies 
      b' = a'' -> b''
      c' = a'' -> c''

and with those definitions/unifications we can continue the application

((.) (.) (.) :: (b'' -> c'') -> (a' -> b') -> (a' -> c'))

then expand

((.) (.) (.) :: (b'' -> c'') -> (a' -> a'' -> b'') -> (a' -> a'' -> c''))

and clean it up

substitute b'' -> b
           c'' -> c
           a'  -> a
           a'' -> a1

(.).(.) :: (b -> c) -> (a -> a1 -> b) -> (a -> a1 -> c)

which, to be honest, is a bit of a counterintuitive result.


Here's the intuition. First take a look at fmap

fmap :: (a -> b) -> (f a -> f b)

it "lifts" a function up into a Functor. We can apply it repeatedly

fmap.fmap.fmap :: (Functor f, Functor g, Functor h) 
               => (a -> b) -> (f (g (h a)) -> f (g (h b)))

allowing us to lift a function into deeper and deeper layers of Functors.

It turns out that the data type (r ->) is a Functor.

instance Functor ((->) r) where
   fmap = (.)

which should look pretty familiar. This means that fmap.fmap translates to (.).(.). Thus, (.).(.) is just letting us transform the parametric type of deeper and deeper layers of the (r ->) Functor. The (r ->) Functor is actually the Reader Monad, so layered Readers is like having multiple independent kinds of global, immutable state.

Or like having multiple input arguments which aren't being affected by the fmaping. Sort of like composing a new continuation function on "just the result" of a (>1) arity function.


It's finally worth noting that if you think this stuff is interesting, it forms the core intuition behind deriving the Lenses in Control.Lens.

这篇关于撰写功能组合:(。)。(。)如何工作?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆