最近試用pure λ Calculus喺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)

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?

我諗你expect我會答not the same thing, 咁咪唔係自相矛盾囉, 但你可能誤會咗我嘅意思, 我只係想講Haskell不能implement a pure Y combinator , as you said咋!

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

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

我諗你expect我會答not the same thing, 咁咪唔係自相矛盾囉, 但你可能誤會咗我嘅意思, 我只係想講Haskell不能implement a pure Y combinator , as you said咋!

If g(x) = f(x) for all x, g and f are the same function. So fix and Y are the same in the sense that they compute the same thing. However, you cannot write a function that compute the same result as Y in Haskell using the formulation of the Y-combinator. You have to write "f y = f (y f)" instead in Haskell.

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

where did you have your higher education? Are you actually a professor?

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

Before talking about [Inst], we need to talk about ⊑. This is a relation between types. Hindley Milner type system can deal with polymorphic types.
σ' ⊑ σ means σ is a more specialized type than σ'. For example,

a -> a ⊑ Int -> Int
[a] -> ⊑ [Char]
a -> b ⊑ a -> [Int->Int]

[Inst] If it is proven that e has type σ' in Γ and σ is a more specialized type than σ', then e has type σ in Γ.

For example is e has type [a] in Γ, then e can have type list of [Int] in Γ. This rule is for instantiation.

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

where did you have your higher education? Are you actually a professor?

MIHK (made in Hong Kong).
Not a professor, though I know many friends who are.

其實學完可以用黎做咩？好似頗多人對haskell有興趣

痴線 咩level既野黎

痴線 咩level既野黎

Principles of programming languages. Final year or graduate level 左右。

痴線 咩level既野黎

Principles of programming languages. Final year or graduate level 左右。

乜原來ug已經要讀呢d野

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

Before talking about [Inst], we need to talk about ⊑. This is a relation between types. Hindley Milner type system can deal with polymorphic types.
σ' ⊑ σ means σ is a more specialized type than σ'. For example,

a -> a ⊑ Int -> Int
[a] -> ⊑ [Char]
a -> b ⊑ a -> [Int->Int]

[Inst] If it is proven that e has type σ' in Γ and σ is a more specialized type than σ', then e has type σ in Γ.

For example is e has type [a] in Γ, then e can have type list of [Int] in Γ. This rule is for instantiation.

Before talking about the last rule for generalization, I need to talk about free variable. In the λ expression λ x . x y. The variable x is a bound variable. It is the argument for the abstraction. The variable y is unbound or free. We do not know what value y has. In λ x . λ y . x y both x and y around bound and there is no free variable.

Similarly we can have free type variable in a polymorphic type. ∀ a . a -> a is a polymorphic function type from any type a to itself. ∀ a . (a, b) is a tuple type where a is any type but b is a free type variable. The meaning of ∀ a . (a, b) depends on some external definition of b. On the other hand, ∀ a . ∀ b . (a, b) has no free type variable. It is a polymorphic tuple type of 2 distinct types.

Here is the last rule

[Gen] If it is proven that e has (a possibly polymorphic) type σ in Γ and α is not a free type variable in Γ, then e has type σ for any α.

α cannot be a free type variable in Γ or we would bind it by mistake.

This rule is the reverse of [Inst]. [Inst] goes from generic to specialized. [Gen] goes from specialized to generic.

痴線 咩level既野黎

Principles of programming languages. Final year or graduate level 左右。

乜原來ug已經要讀呢d野

This is not as abstract or difficult as theory of computation (automata, Turing machines etc) and some school cover those in final year for ug. So I don't think it is hard for a final year CS student.

其實係咁將Haskell尋根究底落去, 我怕終須有日要掂埋近世紀最屈機嘅Category Theory!
(P.S. set theory我就識啫, CT真係完全唔知係乜嘢concept嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

Before talking about [Inst], we need to talk about ⊑. This is a relation between types. Hindley Milner type system can deal with polymorphic types.
σ' ⊑ σ means σ is a more specialized type than σ'. For example,

a -> a ⊑ Int -> Int
[a] -> ⊑ [Char]
a -> b ⊑ a -> [Int->Int]

[Inst] If it is proven that e has type σ' in Γ and σ is a more specialized type than σ', then e has type σ in Γ.

For example is e has type [a] in Γ, then e can have type list of [Int] in Γ. This rule is for instantiation.

Before talking about the last rule for generalization, I need to talk about free variable. In the λ expression λ x . x y. The variable x is a bound variable. It is the argument for the abstraction. The variable y is unbound or free. We do not know what value y has. In λ x . λ y . x y both x and y around bound and there is no free variable.

Similarly we can have free type variable in a polymorphic type. ∀ a . a -> a is a polymorphic function type from any type a to itself. ∀ a . (a, b) is a tuple type where a is any type but b is a free type variable. The meaning of ∀ a . (a, b) depends on some external definition of b. On the other hand, ∀ a . ∀ b . (a, b) has no free type variable. It is a polymorphic tuple type of 2 distinct types.

Here is the last rule

[Gen] If it is proven that e has (a possibly polymorphic) type σ in Γ and α is not a free type variable in Γ, then e has type σ for any α.

α cannot be a free type variable in Γ or we would bind it by mistake.

This rule is the reverse of [Inst]. [Inst] goes from generic to specialized. [Gen] goes from specialized to generic.

A better explanation of [Gen] than mine.

http://akgupta.ca/blog/2013/06/07/so-you-still-dont-understand-hindley-milner-part-3/

留名

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

Before talking about [Inst], we need to talk about ⊑. This is a relation between types. Hindley Milner type system can deal with polymorphic types.
σ' ⊑ σ means σ is a more specialized type than σ'. For example,

a -> a ⊑ Int -> Int
[a] -> ⊑ [Char]
a -> b ⊑ a -> [Int->Int]

[Inst] If it is proven that e has type σ' in Γ and σ is a more specialized type than σ', then e has type σ in Γ.

For example is e has type [a] in Γ, then e can have type list of [Int] in Γ. This rule is for instantiation.

Before talking about the last rule for generalization, I need to talk about free variable. In the λ expression λ x . x y. The variable x is a bound variable. It is the argument for the abstraction. The variable y is unbound or free. We do not know what value y has. In λ x . λ y . x y both x and y around bound and there is no free variable.

Similarly we can have free type variable in a polymorphic type. ∀ a . a -> a is a polymorphic function type from any type a to itself. ∀ a . (a, b) is a tuple type where a is any type but b is a free type variable. The meaning of ∀ a . (a, b) depends on some external definition of b. On the other hand, ∀ a . ∀ b . (a, b) has no free type variable. It is a polymorphic tuple type of 2 distinct types.

Here is the last rule

[Gen] If it is proven that e has (a possibly polymorphic) type σ in Γ and α is not a free type variable in Γ, then e has type σ for any α.

α cannot be a free type variable in Γ or we would bind it by mistake.

This rule is the reverse of [Inst]. [Inst] goes from generic to specialized. [Gen] goes from specialized to generic.

Wow, extremely concise and to the point. And that's what I am looking for! Thanks a lot!

痴線 咩level既野黎

Principles of programming languages. Final year or graduate level 左右。

乜原來ug已經要讀呢d野

This is not as abstract or difficult as theory of computation (automata, Turing machines etc) and some school cover those in final year for ug. So I don't think it is hard for a final year CS student.

吓, 我反而覺得你講得精簡易明過嗰篇So You Still Don't Understand Hindley-Milner?喎! 嗰篇嘢太長太「侵」氣了!

Proof唔Proof到halting problem

Proof唔Proof到halting problem

Google一下都搵到個proof了!

Turing machines make things awkward and complicated. But Lambda Calculus makes things much easier! To illustrate, Y-combinator is already a hint for the undecidability proof of the halting problem!

compare:
Y = λ y . ( λ x . y (x x)) ( λ x . y (x x))

E = Halting(λm.not(Halting(m,m)), λm.not(Halting(m,m)))

Does the above expression E returns True or False? Ans: Cannot be answered( i.e. Undecided)

For details, please see https://yinwang0.wordpress.com/2012/10/25/halting/

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

where did you have your higher education? Are you actually a professor?

MIHK (made in Hong Kong).
Not a professor, though I know many friends who are.

phd?

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

where did you have your higher education? Are you actually a professor?

MIHK (made in Hong Kong).
Not a professor, though I know many friends who are.

phd?

講咁多怕自爆lu。有多過一個同電腦有關學位，都係MIHK，唔係MIT。 。其實呢度講都係皮毛，唔係真係好深。我都係上網睇。有決心嘅undergraduate應該睇得明。睇過有U Hindley Milner係響advanced undergraduate course講，即係expect有部份undergraduate會讀得明，但唔係全部。

...

哈哈, 你啱, 既然用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嚟!)

A
_
B

is just a way to say that A -> B or "If A then B" in plain English.

A B
____
C

is just a way to say that A ^ B -> C or "If A and B then C".

Γ (gamma) is a type environment. You can treat it as something that can answer this question "what is the type of X?". A type environment can be extended like this Γ , x : τ. This means we add a new declaration of some variable x to be the type τ. If x was previously defined in Γ, the old type definition will be ignored. Type environment extension happens when we enter a new scope for example.

The turnstile symbol (⊢) means "proves" or "yields"

Here is what the 6 rules says in English

[Var]: If x:τ in environment Γ, then single variable expression x has type τ in Γ

[App] If it is proven that e0 is a function from τ to τ' in Γ and it is proven that e1 has type τ in Γ, then expression e0 e1 (applying function e0 with argument e1) has type τ' in Γ.

[Abs] If it is proven that e has type τ' in the extended environment Γ , x : τ (adding x : τ to Γ), then expression λ x . e has a function type τ to τ' in Γ.

[Let] If it is proven that e0 has type σ in Γ and e1 has type τ in the extended environment Γ , x : σ, i.e. adding x : σ to Γ. Then expression let x = e0 in e1 has type τ in Γ.

I will talk about the next two rules later. Need to do some work.

where did you have your higher education? Are you actually a professor?

MIHK (made in Hong Kong).
Not a professor, though I know many friends who are.

phd?

講咁多怕自爆lu。有多過一個同電腦有關學位，都係MIHK，唔係MIT。 。其實呢度講都係皮毛，唔係真係好深。我都係上網睇。有決心嘅undergraduate應該睇得明。睇過有U Hindley Milner係響advanced undergraduate course講，即係expect有部份undergraduate會讀得明，但唔係全部。

我學校最後一年如果讀type system 會讀 :p

Oregon Programming Languages Summer School 2012
http://www.youtube.com/playlist?list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf

Oregon Programming Languages Summer School 2012
http://www.youtube.com/playlist?list=PL8Ky8lYL8-Oh7awp0sqa82o7Ggt4AGhyf

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

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

有無 bro 講下 combinators (B, C ... Y), church encodings, category theory 同 lambda calculus 之間既關係？