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

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

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

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

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

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

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

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

屌lm 先

你睇下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喎!

有加有乘，減數點做？

睇完呢篇嘢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). 就係咁簡單。

有加有乘，減數點做？

睇完呢篇嘢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 -

有加有乘，減數點做？

睇完呢篇嘢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.

有加有乘，減數點做？

睇完呢篇嘢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啲:

你睇下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應該係讀過晒上面堆嘢。

lm

你睇下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應該係讀過晒上面堆嘢。

汝有片言，愚當記取。竊知生有涯而學無涯，冀於未殆之時成之!

Code4food係major computer engineering?

順便求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?

順便求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係major computer engineering?

In CE we trust

順便求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.

Code4food係major computer engineering?

我覺得佢至少phd level

順便求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

順便求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)

Code4food係major computer engineering?

In CE we trust

可唔可以透露係邊間u

順便求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嗰啲)介紹下?!

Code4food係major computer engineering?

In CE we trust

可唔可以透露係邊間u

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

...

哈哈, 你啱, 既然用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係major computer engineering?

In CE we trust

可唔可以透露係邊間u

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

三大ja。

順便求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?