Ads
:^(
你睇下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一定容易啲
有加有乘,減數點做? :^(
睇完呢篇嘢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, 好似仲易明過呢篇嘢喎, 正! :^( :^(
有加有乘,減數點做? :^(
睇完呢篇嘢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.
:^(
你睇下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囉! :^(
唔又數學角度開始,可以又實物角度學各類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應該係讀過晒上面堆嘢。
Ads
順便求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! :^(
順便求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?
順便求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.
順便求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)
:^(
順便求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)
Ads
Code4food係major computer engineering?
In CE we trust :^(
可唔可以透露係邊間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嗰啲)介紹下?! :^(
Code4food係major computer engineering?
In CE we trust :^(
可唔可以透露係邊間u :^(
我懷疑佢係MIT(or 接近MIT級數嘅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呢? 直頭係自相矛盾啦! :^(
你睇下C4F個會員number大成咁, 都知佢過咗嚟連登冇耐啦!
BTW, 通過functional programming, 可以明白深一層其他programming paradigms嘅真諦, 而各大functional languages或者其他languages裏面注入嘅functional features其實都源自lambda calculus, 明白佢嘅運作有一理通百理明之效.
但你(同C4F兄)可能會問, 咁你不如直接用Maths嘅角度學各類computer languages咪仲好? 唉, 弊在我唔係數底呢? Mission impossible囉!