最近試用pure λ Calculus喺Haskell度砌啲基本嘢...

95 回覆
8 Like 0 Dislike
2017-04-26 23:36:10
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!

2017-04-26 23:50:15
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!



BTW, 我開呢個post嘅目的/初衷就係要嘗試用上面講嘅圖則建造起樓嘅部件囉! 發展商呢我就揀咗Haskell!
2017-04-27 00:19:36
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?

category主要同type有關

https://ncatlab.org/nlab/show/lambda-calculus
Simply typed lambda calculus is the natural internal languge of Cartesian closed category. This means that:

1. Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while

2. Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.
2017-04-27 00:22:30
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!


I don't think lambda calculus need set theory. In fact, we don't the concept of domain in pure lambda caculus.(好似係?)
2017-04-27 00:26:20
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!



BTW, 我開呢個post嘅目的/初衷就係要嘗試用上面講嘅圖則建造起樓嘅部件囉! 發展商呢我就揀咗Haskell!

thanks bro
btw 你想用 fp 去做 oop 做到既野?
2017-04-27 00:30:39
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?

category主要同type有關

https://ncatlab.org/nlab/show/lambda-calculus
Simply typed lambda calculus is the natural internal languge of Cartesian closed category. This means that:

1. Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while

2. Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.


對我嚟講, 上面都唔知up乜7, 麻煩叔叔你可唔可以好似C4F神咁, 淺入淺出咁講解下呢?!
2017-04-27 00:30:41
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?

category主要同type有關

https://ncatlab.org/nlab/show/lambda-calculus
Simply typed lambda calculus is the natural internal languge of Cartesian closed category. This means that:

1. Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while

2. Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.

thanks bro
好深奧
2017-04-27 00:35:37
見識過linguists 用 lamba calculus 去做 analysis, 好多nlp 都係以呢啲為根基
2017-04-27 00:38:37
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?

category主要同type有關

https://ncatlab.org/nlab/show/lambda-calculus
Simply typed lambda calculus is the natural internal languge of Cartesian closed category. This means that:

1. Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while

2. Every simply typed lambda calculus “generates” a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.

thanks bro
好深奧

其實再深d既我都唔識
2017-04-27 00:40:45
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!


I don't think lambda calculus need set theory. In fact, we don't the concept of domain in pure lambda caculus.(好似係?)


其實我都唔係太清楚Lambda Calculus同Set Theory係咪有關係, 但我記憶所及, 以前初初接觸Haskell時, 好多articles (especially those written by CS professors)講解function時都會用到set theory嘅domain concept(大概係咁: Given an input, a function will always return the same output; and input and output are just closely related domains.)
2017-04-27 00:52:06
有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係?


如果Lambda Calculus建築理論, Church encoding就係以Lambda Calculus造出嚟嘅圖則: Church numerals are the blueprints for building natural numbers; Church booleans, logic operators such as true/false, and, or, not; Church pairs, a function that takes a function argument; B, C, K, W, Y combinators, a series of higher-ordered functions to help build more complex user-defined functions.

至於Category Theory(CT)同上面呢堆嘢有乜關係, 我就唔曉喇, 只知CT係an alternative to set theory, 而function under Lambda Calculus係借用咗set theory (domain concept)去define嘅!



BTW, 我開呢個post嘅目的/初衷就係要嘗試用上面講嘅圖則建造起樓嘅部件囉! 發展商呢我就揀咗Haskell!

thanks bro
btw 你想用 fp 去做 oop 做到既野?


唔係! BTW, 記得Quora度有人提過, 其實GoF有一半左右嘅OOP design patterns 係取材自FP features的, 熟習FP對學OOP都有莫大好處囉!
2017-04-27 01:08:29
見識過linguists 用 lamba calculus 去做 analysis, 好多nlp 都係以呢啲為根基


Yeah, this is also the direction I'd like to go so that I can use Haskell or other FLs to do nlp-like tasks such as syntax or semantic analysis!
2017-04-27 01:35:07
見識過linguists 用 lamba calculus 去做 analysis, 好多nlp 都係以呢啲為根基


Yeah, this is also the direction I'd like to go so that I can use Haskell or other FLs to do nlp-like tasks such as syntax or semantic analysis!


[member]
I've started a project to build a library to adapt declarative programming. For example:

[code]

a("man").is(a("person")).whose("gender").is("male")

// defines

class Man extends Person {
constructor(name) {
super(name, "male");
}
// the rest of the class
}

// then

whatIs(a("man"))
// => "a man is a person whose gender is male

[/code]
[\member]

do you find that there is a certain degree of similarity in what we are interested in doing ?
2017-04-27 01:35:09
Oregon Programming Languages Summer School 2012
http://www.youtube.com/playlist?list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf


居然有4堂Category Theory (foundations level), 好似唔錯!

BTW, 呢間U個Summer School logo好正:
λ, 全部都係λ !

https://www.cs.uoregon.edu/research/summerschool/summer17/_images/oplssLogo.svg


Category Theory for programmers:

https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

This is a good series of video lecture. I watched it all but did not quite fully understand the last bit on Monads. You have to be patient though. It is 20 video for about 15-20 hours.
2017-04-27 02:23:25
見識過linguists 用 lamba calculus 去做 analysis, 好多nlp 都係以呢啲為根基


Yeah, this is also the direction I'd like to go so that I can use Haskell or other FLs to do nlp-like tasks such as syntax or semantic analysis!


[member]
I've started a project to build a library to adapt declarative programming. For example:

[code]

a("man").is(a("person")).whose("gender").is("male")

// defines

class Man extends Person {
constructor(name) {
super(name, "male");
}
// the rest of the class
}

// then

whatIs(a("man"))
// => "a man is a person whose gender is male

[/code]
[\member]

do you find that there is a certain degree of similarity in what we are interested in doing ?


我剩係見到好多grammatical units變成higher-order/call-back functions, 同ES6個typical class inheritance. BTW, 用JS咁玩法, 都係第一次見!
2017-04-27 02:35:32
Oregon Programming Languages Summer School 2012
http://www.youtube.com/playlist?list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf


居然有4堂Category Theory (foundations level), 好似唔錯!

BTW, 呢間U個Summer School logo好正:
λ, 全部都係λ !

https://www.cs.uoregon.edu/research/summerschool/summer17/_images/oplssLogo.svg


Category Theory for programmers:

https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

This is a good series of video lecture. I watched it all but did not quite fully understand the last bit on Monads. You have to be patient though. It is 20 video for about 15-20 hours.


時間唔算好長(正常一篇academic article隨時都要花8/9個鐘嚟睇計), 問題係唔知我個background knowledge suf唔sufficient enough去聽明佢講乜嘢 ! Anyway, 又多個好source去學CT了, 正!
2017-04-27 02:47:58
You can skip the first lecture because it is mostly about philosophy behind category theory.
2017-04-27 19:02:58
You can skip the first lecture because it is mostly about philosophy behind category theory.


Roger! 不過等我睇晒嗰4條CT foundations片, 補補個底先開佢齋, 哈!
2017-04-28 00:49:38
順便玩下B, C, K, W呢幾個primitive combinators 嘅 implementation in Haskell.
B, C, K, W are defined as follows:
B x y z = x (y z)
C x y z = x z y
K x y = x
W x y = x y y




BTW, 用上面啲combinators再加多個S combinator已經玩到好基本嘅combinatory logic了, i.e.

B = S (K S) K
C = S (S (K (S (K S) K)) S) (K K)
K = K
W = S S (S K)


不過combinatory logic又係個大topic嚟, 遲啲先再深入研究一下!
2017-04-29 00:50:38
諗住開坑玩下idris
吹水台自選台熱 門最 新手機台時事台政事台World體育台娛樂台動漫台Apps台遊戲台影視台講故台健康台感情台家庭台潮流台美容台上班台財經台房屋台飲食台旅遊台學術台校園台汽車台音樂台創意台硬件台電器台攝影台玩具台寵物台軟件台活動台電訊台直播台站務台黑 洞