2017-05-27 52 views
2

在最近的工作表上,我被要求解釋爲什麼函數f,在:f g x = g (g x) x中沒有類型。對Haskell函數類型參數的說明

對於Haskell,我很新,我很困惑於如何在不知道任何有關函數的細節的情況下計算出左右表達式的關聯順序。好像是g應該被定義爲:

g :: a -> b,假設的x類型爲a - 然而,這似乎立即導致麻煩的,因爲在RHS,g (g x) x似乎暗示g需要兩個參數,類型之一ba之一。此外,我也堅持如何閱讀LHS,也就是說f有兩個參數:函數g和變量x,或者它只需要1個參數,(g x)

我想知道是否有人可以指導我如何閱讀這些表達式?

+0

我無法理解所問的問題。你能否準確地向我們提出與工作表中出現的問題一樣的問題?我可以說'g(g x)'將'g'應用於'x'的結果是'g'。如果你對使用括號的應用程序的語言更熟悉,那麼這些語言就是'g(g(x))'。 –

+0

@ReinHenrichs問題如下:「解釋爲什麼下面定義的函數f沒有類型: f g x = g(g x)x」 我有點好奇你怎麼能解決這個問題?一旦我們評估g(g x),將g應用於g x的結果,我們將如何處理x(g(g x)x? – CowNorris

+0

啊,我錯過了最後的'x'並且感到困惑,因爲'f g x = g(g x)'顯然是一個類型。 –

回答

6

相關的規則是:

  1. 應用寫成並置,即f x適用fx

  2. 括號用於界定表達式,不適用於功能應用,即f (g x)適用fg x。 (其中g x是本身的g應用到x。)

  3. 應用相關聯的左側,即,f x y = (f x) y

把這些在一起,我們可以看到,g (g x) x = (g (g x)) x,即,g (g x)應用到x,其中g (g x)是本身的gg x到該應用程序。

我還應該提到,Haskell中的所有函數都只有一個參數。似乎一個函數具有多個參數在哪裏,實在是譁衆取寵:

f x y z = ((f x) y) z 

換句話說,f是一個函數,參數,返回一個函數,參數,返回一個函數,參數並返回一個值。你可能會明白爲什麼我們有時更喜歡撒謊,並說一個函數需要多個參數,但這在技術上並不正確。 「接受多個參數」的函數實際上是一個返回函數的函數,該函數可能會返回一個函數,依此類推。

7

爲了能夠回答這樣的問題,您需要像Haskell編譯器一樣思考。我們有一個功能。

f g x = g (g x) x 

爲了使這是很好類型的,我們需要找到的類型fgx。現在,f需要兩個參數,所以

f :: a -> b -> c 
g :: a 
x :: b 

我們也知道,g x必須合理的表達(我們會說g x是「中規中矩」),所以g必須到x可以是函數應用。所以它也是這樣的情況,

g :: b -> t0 

其中t0是一個類型變量,現在。我們不知道g x的結果;我們只知道它「有意義」。現在,外部g (g x) x也必須有意義。因此,g必須是我們可以應用g x(其類型爲t0,正如我們前面所述)和x(其類型爲b)以便能夠獲得c(函數的返回類型)的結果。所以

g :: t0 -> b -> c 

現在,這裏是問題發生的地方。我們看到g有三個聲明:ab -> t0t0 -> b -> c。爲了使g擁有所有這三種類型,他們必須將統一爲。也就是說,通過插入某些變量的值,他們必須能夠變得相同。 a沒有任何問題,因爲它是一個自由變量,不依賴於其他任何東西,所以我們可以將它「設置」爲任何我們想要的。因此b -> t0t0 -> b -> c必須相同。在Haskell中,我們寫的

(b -> t0) ~ (t0 -> b -> c) 

括號(中種)都是右結合的,所以這相當於

(b -> t0) ~ (t0 -> (b -> c)) 

爲了兩個函數類型是一樣的,他們的論據必須是一樣的,所以

b ~ t0 
t0 ~ (b -> c) 

通過的傳遞特性,這意味着

b ~ (b -> c) 

所以b是一種以自己爲論點的類型。這就是Haskell所說的無限類型,不符合現行標準。所以爲了讓你寫的這個函數可以接受,b必須是Haskell中不存在的類型。因此,f不是有效的Haskell函數。

+0

最好不要給作業問題的答案。學生應該回答它,而不是我們。 –

+3

我認爲問題和答案在https://meta.stackoverflow.com/q/334822/625403的作業政策指導方針中都是合理的。這當然不是「不利於學生學習的答案」。當然,它比OP可能更理想,但Stack Overflow是爲那些從Google來到這裏的人創造持久價值的答案,而不僅僅是提出問題的人。 – amalloy

5
  1. 功能應用程序是左結合:a b c解析作爲(a b) c
  2. 函數定義對於lambda表達式語法糖:f x y = ...裝置f = \x y -> ...
  3. lambda表達式使用多個參數自動咖喱:\x y -> ...裝置\x -> (\y -> ...)

因此

f g x = g (g x) x 

意味着

f = \g -> (\x -> (g (g x)) x) 

現在,讓我們試着得出的f類型。讓我們給它一個名字:

f :: ta 

但究竟什麼是taf被定義爲的λ,所以它的類型涉及->(它是一個函數):

\g -> (\x -> (g (g x)) x) :: tb -> tc 
g :: tb 
\x -> (g (g x)) x :: tc 

即對於某些類型tbtc,並且g(參數)的類型是tb,並且結果(函數體)的類型是tc\g -> ...的類型是tb -> tc

而且因爲整個事情是必然f,我們有

ta = tb -> tc 

我們不tc做,雖然:

\x -> (g (g x)) x :: td -> te 
x :: td 
(g (g x)) x :: te 

tc = td -> te 

功能正文(其類型我們稱爲te)由一個應用程序組成(必須是)變量x的函數。由此可以得出:

g (g x) :: td -> te 

因爲

x :: td 
(g (g x)) x :: te 

再次向下鑽取,我們有

g :: tf -> (td -> te) 
g x :: tf 

因爲應用gg x必須有類型td -> te。最後,

g :: td -> tf 

因爲

x :: td 
g x :: tf 

現在我們有g兩個等式:

g :: tf -> (td -> te) 
g :: td -> tf 

因此

tf  = td 
td -> te = tf 

tf -> te = tf 

在這裏,我們碰到一個問題:tf定義在之中ms本身,給出類似於

tf = (((((... -> te) -> te) -> te) -> te) -> te) -> te 

即無限大的類型。這是不允許的,這就是爲什麼f沒有有效的類型。