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

MCHK

95 回覆
8 Like 0 Dislike
MCHK 2017-04-22 17:49:36


你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!

BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.

但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!
7e2a73d0043b3f98 2017-04-22 17:57:41


你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!

BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.

但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!

你要玩lambda calculus 用coq一定容易啲
R1R_MYJJ 2017-04-22 18:03:04
屌lm 先
MCHK 2017-04-22 18:12:51


你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!

BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.

但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!

你要玩lambda calculus 用coq一定容易啲


吓, 咁又唔駛去到用Coq咁專業! 畢竟I just treat lambda calculus as a means to dive into Haskell or the functional features of other languages! I'm of no interest to prove all kinds of Church encodings or learn lambda calculus in depth喎!
Code4Food 2017-04-22 23:08:21
有加有乘,減數點做?


睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!


哈,呢篇野嘅方法基本上同我嘅係一樣。


但我lap一lap你整pred嗰啲steps, 好似仲易明過呢篇嘢喎, 正!


個trick係一路做function composition時記住之前個value,咁做完f^n時就就會有f^(n-1). 就係咁簡單。
MCHK 2017-04-23 01:51:42
有加有乘,減數點做?


睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!


哈,呢篇野嘅方法基本上同我嘅係一樣。


但我lap一lap你整pred嗰啲steps, 好似仲易明過呢篇嘢喎, 正!


個trick係一路做function composition時記住之前個value,咁做完f^n時就就會有f^(n-1). 就係咁簡單。


明白了, 但我先玩下你steps中提及嘅Church pairs先:
pair = λ x y z . z x y
first = λ p . p (λ x y . x)
second = λ p . p (λ x y . y)

first (pair a b) = a
second (pair a b) = b

咁e.g. first (pair a b) 係點變成a嘅呢? 個steps是咁的:
first (pair a b)
= (λ p . p (λ x y . x)) ((λ x y z . z x y) a b) // application of first on pair on a & b
= (λ p . p (λ x y . x)) (λ z . z a b) // β-reduction
= (λ z . z a b)(λ x y . x) // - ditto -
= (λ x y . x) a b // - ditto -
= a // - ditto -

Code4Food 2017-04-23 02:26:36
有加有乘,減數點做?


睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!


哈,呢篇野嘅方法基本上同我嘅係一樣。


但我lap一lap你整pred嗰啲steps, 好似仲易明過呢篇嘢喎, 正!


個trick係一路做function composition時記住之前個value,咁做完f^n時就就會有f^(n-1). 就係咁簡單。


明白了, 但我先玩下你steps中提及嘅Church pairs先:
pair = λ x y z . z x y
first = λ p . p (λ x y . x)
second = λ p . p (λ x y . y)

first (pair a b) = a
second (pair a b) = b

咁e.g. first (pair a b) 係點變成a嘅呢? 個steps是咁的:
first (pair a b)
= (λ p . p (λ x y . x)) ((λ x y z . z x y) a b) // application of first on pair on a & b
= (λ p . p (λ x y . x)) (λ z . z a b) // β-reduction
= (λ z . z a b)(λ x y . x) // - ditto -
= (λ x y . x) a b // - ditto -
= a // - ditto -


Yes.
MCHK 2017-04-23 02:47:12
有加有乘,減數點做?


睇完呢篇嘢http://gettingsharper.de/2012/08/30/lambda-calculus-subtraction-is-hard/放棄咗! 雖然Church encoding話subtraction只是咁樣: sub = λ x y . y pred x , 但我唔太理解個pred點整出嚟, 就算整到個pred出嚟, 個sub都唔係真subtraction嚟, 篇嘢有講原因!

In short, it's not too meaningful to implement a subtraction operator in terms of plain λ calculus, 好似係!


哈,呢篇野嘅方法基本上同我嘅係一樣。


但我lap一lap你整pred嗰啲steps, 好似仲易明過呢篇嘢喎, 正!


個trick係一路做function composition時記住之前個value,咁做完f^n時就就會有f^(n-1). 就係咁簡單。


明白了, 但我先玩下你steps中提及嘅Church pairs先:
pair = λ x y z . z x y
first = λ p . p (λ x y . x)
second = λ p . p (λ x y . y)

first (pair a b) = a
second (pair a b) = b

咁e.g. first (pair a b) 係點變成a嘅呢? 個steps是咁的:
first (pair a b)
= (λ p . p (λ x y . x)) ((λ x y z . z x y) a b) // application of first on pair on a & b
= (λ p . p (λ x y . x)) (λ z . z a b) // β-reduction
= (λ z . z a b)(λ x y . x) // - ditto -
= (λ x y . x) a b // - ditto -
= a // - ditto -


Yes.


上面個implementation of Church pairs in Haskell唔太純潔, 下面嗰個就比較pure and true啲:

Code4Food 2017-04-23 07:59:14


你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!

BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.

但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!

唔又數學角度開始,可以又實物角度學各類computer languages。先讀solid state electronics,學transistor,再學logic gates,再學adder/mux/buffer,再學ALU/Cache,跟著學CPU,跟手學成部電腦computer architecture。知到部電腦點行就學assembly programming,學完後就學compilers。

呢個bottom up學法,學完要明白C pointer無難度(memory address嚟,好似係,除非唔係)。

利申:我bachelor's degree應該係讀過晒上面堆嘢。
suffix 2017-04-23 08:10:24
lm
MCHK 2017-04-23 17:36:10


你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!

BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.

但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!

唔又數學角度開始,可以又實物角度學各類computer languages。先讀solid state electronics,學transistor,再學logic gates,再學adder/mux/buffer,再學ALU/Cache,跟著學CPU,跟手學成部電腦computer architecture。知到部電腦點行就學assembly programming,學完後就學compilers。

呢個bottom up學法,學完要明白C pointer無難度(memory address嚟,好似係,除非唔係)。

利申:我bachelor's degree應該係讀過晒上面堆嘢。


汝有片言,愚當記取。竊知生有涯而學無涯,冀於未殆之時成之!
underpants 2017-04-24 18:14:29
Code4food係major computer engineering?
kekekejjjj 2017-04-24 18:19:08
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?
MCHK 2017-04-24 20:02:26
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?


係呀, Haskell個built-in Y combinator叫fixed-point combinator(i.e. fix), import個Data.Function 或者 Control.Monad.Fix就用得, 唔駛自己嚟, 不過自己當然都嚟唔到, define唔到個又pure又true嘅Y combinator, 最多打下茅波, 整個超殘廢版 :
let fixedPoint fun = let {x = fun x} in x
or simply
let y f = f (y f)

Code4Food 2017-04-24 23:03:47
Code4food係major computer engineering?

In CE we trust
Code4Food 2017-04-24 23:05:33
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?

It is not possible due to limitation of the Hindley Milner type system but you can write the fixed-point operator trivially in Haskell due to lazy evaluation.
kekekejjjj 2017-04-25 01:54:27
Code4food係major computer engineering?

我覺得佢至少phd level
kekekejjjj 2017-04-25 01:56:31
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?

It is not possible due to limitation of the Hindley Milner type system but you can write the fixed-point operator trivially in Haskell due to lazy evaluation.

yaa i guess that's what I meant.
because when you try to type with milner system it got stuck somewhere due to the recursive property? i remember trying to derive a proof before but failed
Code4Food 2017-04-25 03:17:48
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?


係呀, Haskell個built-in Y combinator叫fixed-point combinator(i.e. fix), import個Data.Function 或者 Control.Monad.Fix就用得, 唔駛自己嚟, 不過自己當然都嚟唔到, define唔到個又pure又true嘅Y combinator, 最多打下茅波, 整個超殘廢版 :
let fixedPoint fun = let {x = fun x} in x
or simply
let y f = f (y f)



No. They are the same thing only expressed differently. It is not possible to express the fixed-point combinator using lambda calculus in Haskell "fix" is the same thing. The only difference is that:

y f = f (y f)

is not a normal definition in the mathematical sense. It is a equation. Essentially we want to solve this equation:

x = f x

We want to find a value x such that f x equals to x itself. Hence it is called a fixed point. The thing with an equation is that it may not be solvable or has multiple or infinite solution. In Haskell, if you write

y f = f (y f)

you get

f (f (f (f (f .......))

so y is indeed the fixed point combinator. However, you can only do it in a language with lazy evaluation. You can do the same in scheme of lisp but you will get a stack overflow if you write something like:

(define fix (lambda (f) (f (y f))))

(define fact-0
(lambda (next)
(lambda (n) (if (= 0 n) 1 (* n (next (- n 1)))))))

;; stack overflow
(fix fact-0)
underpants 2017-04-25 18:49:30
Code4food係major computer engineering?

In CE we trust

可唔可以透露係邊間u
MCHK 2017-04-25 18:53:56
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?


係呀, Haskell個built-in Y combinator叫fixed-point combinator(i.e. fix), import個Data.Function 或者 Control.Monad.Fix就用得, 唔駛自己嚟, 不過自己當然都嚟唔到, define唔到個又pure又true嘅Y combinator, 最多打下茅波, 整個超殘廢版 :
let fixedPoint fun = let {x = fun x} in x
or simply
let y f = f (y f)



No. They are the same thing only expressed differently. It is not possible to express the fixed-point combinator using lambda calculus in Haskell "fix" is the same thing. The only difference is that:

y f = f (y f)

is not a normal definition in the mathematical sense. It is a equation. Essentially we want to solve this equation:

x = f x

We want to find a value x such that f x equals to x itself. Hence it is called a fixed point. The thing with an equation is that it may not be solvable or has multiple or infinite solution. In Haskell, if you write

y f = f (y f)

you get

f (f (f (f (f .......))

so y is indeed the fixed point combinator. However, you can only do it in a language with lazy evaluation. You can do the same in scheme of lisp but you will get a stack overflow if you write something like:

(define fix (lambda (f) (f (y f))))

(define fact-0
(lambda (next)
(lambda (n) (if (= 0 n) 1 (* n (next (- n 1)))))))

;; stack overflow
(fix fact-0)


哈哈, 你啱, 既然用Haskell都implement唔都個純Y combinator (i.e. Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))), 咁Haskell個fix (imported from Data.Function or Control.Monad.Fix)又點可能係個純Y combinator呢? 直頭係自相矛盾啦!

BTW, 其實依你所見, 如果要深入認識Haskell, 駛唔駛學埋佢個type inference system (i.e. 你提及過嘅Hindley–Milner type system). 但我google過個HM algorithm, 即刻O晒嘴(乜L嘢嚟 ):


如果要學埋, 有冇啲淺入淺出嘅articles(唔太多maths jargons嗰啲)介紹下?!
MCHK 2017-04-25 22:14:08
Code4food係major computer engineering?

In CE we trust

可唔可以透露係邊間u


我懷疑佢係MIT(or 接近MIT級數嘅U)出嚟嘅!
MCHK 2017-04-25 22:23:38


...

哈哈, 你啱, 既然用Haskell都implement唔都個純Y combinator (i.e. Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))), 咁Haskell個fix (imported from Data.Function or Control.Monad.Fix)又點可能係個純Y combinator呢? 直頭係自相矛盾啦!

BTW, 其實依你所見, 如果要深入認識Haskell, 駛唔駛學埋佢個type inference system (i.e. 你提及過嘅Hindley–Milner type system). 但我google過個HM algorithm, 即刻O晒嘴(乜L嘢嚟 ):


如果要學埋, 有冇啲淺入淺出嘅articles(唔太多maths jargons嗰啲)介紹下?!


其實係咁將Haskell尋根究底落去, 我怕終須有日要掂埋近世紀最屈機嘅Category Theory!
(P.S. set theory我就識啫, CT真係完全唔知係乜嘢concept嚟!)
Code4Food 2017-04-26 01:49:12
Code4food係major computer engineering?

In CE we trust

可唔可以透露係邊間u


我懷疑佢係MIT(or 接近MIT級數嘅U)出嚟嘅!

三大ja。
Code4Food 2017-04-26 01:55:50
順便求C4F指點下點樣係Haskell度implement Y/fix combinator?
i.e.呢舊嘢:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))
or
Y = λ f . ( λ x . f (x x)) ( λ x . f (x x))
or
Yf

Yf produces fYf produces f(fYf) produces f(f(fYf)) ... as recursion

我見stackoverflow話Y唔屬於Haskell built-in 嘅任何一個type, 就咁define Y 去 implement會出error, 咁應該點做呢? 可否用factorial做example教下點implement Y combinator?

Thanks in advance!

according to what I am aware of, it is not possible. But I think Y combinator is implemented internally in haskell?


係呀, Haskell個built-in Y combinator叫fixed-point combinator(i.e. fix), import個Data.Function 或者 Control.Monad.Fix就用得, 唔駛自己嚟, 不過自己當然都嚟唔到, define唔到個又pure又true嘅Y combinator, 最多打下茅波, 整個超殘廢版 :
let fixedPoint fun = let {x = fun x} in x
or simply
let y f = f (y f)



No. They are the same thing only expressed differently. It is not possible to express the fixed-point combinator using lambda calculus in Haskell "fix" is the same thing. The only difference is that:

y f = f (y f)

is not a normal definition in the mathematical sense. It is a equation. Essentially we want to solve this equation:

x = f x

We want to find a value x such that f x equals to x itself. Hence it is called a fixed point. The thing with an equation is that it may not be solvable or has multiple or infinite solution. In Haskell, if you write

y f = f (y f)

you get

f (f (f (f (f .......))

so y is indeed the fixed point combinator. However, you can only do it in a language with lazy evaluation. You can do the same in scheme of lisp but you will get a stack overflow if you write something like:

(define fix (lambda (f) (f (y f))))

(define fact-0
(lambda (next)
(lambda (n) (if (= 0 n) 1 (* n (next (- n 1)))))))

;; stack overflow
(fix fact-0)


哈哈, 你啱, 既然用Haskell都implement唔都個純Y combinator (i.e. Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))), 咁Haskell個fix (imported from Data.Function or Control.Monad.Fix)又點可能係個純Y combinator呢? 直頭係自相矛盾啦!


If g(x) = f(x) for all x, then are g and f the same thing?
吹水台自選台熱 門最 新手機台時事台政事台World體育台娛樂台動漫台Apps台遊戲台影視台講故台健康台感情台家庭台潮流台美容台上班台財經台房屋台飲食台旅遊台學術台校園台汽車台音樂台創意台硬件台電器台攝影台玩具台寵物台軟件台活動台電訊台直播台站務台黑 洞