為什麼函數式語言里有recursive data type但沒有recursive function type？

01-31

比如(define (fix) (lambda () (fix)))，定義了一個無參數的fix函數。調一下fix返回一個無參數的函數，這函數的作用就是調用之後返回自己。
在Haskell里寫fix () = ()-&>(fix ())會報錯「cannot construct the infinite type」。實際上在強類型的函數式語言里，似乎都無法處理這種recursive function type。
這是否與類型系統的性質有關係？比如「要求type checker必定停機」之類。放鬆這個性質的話，是否能夠處理recursive function type？有無必要？
補充：
(define (fix) fix)或者f () = f（會報錯）是更簡單的寫法。

補充：
Types and Programming Languages 21.8 μ-Types。。書讀少

（先佔坑。。）

Equirecursive Types和Isorecursive Types的問題。 Haskell, SML, Ocaml， C等語言默認用的是Isorecursive。Java, Scala貌似是Equirecursive Types。但是Ocaml有一個可選的「開關」-rectypes。

$ ocaml -rectypes # let rec f = fun x -&> f;; val f : b -&> a as a = &

而默認情況下

$ ocaml # let rec f = fun x -&> f;; Error: This expression has type a -&> b but an expression was expected of type b The type variable b occurs inside a -&> b

Equirecursive的好處是表達力強、方便，但是類型推導困難，且使用時容易發生錯誤（或者說類型檢查演算法不能及早發現錯誤）。

$ ocaml -rectypes # let rec map f = function | [] -&> [] | x :: xs -&> map f x :: map f xs;; val map : a -&> (b list as b) -&> (c list as c) = & # map (fun x -&> x + 1) [1; 2];; This expression has type int but is used with type a list.

Haskell/SML的List的元素不能是List也是同樣的道理。

在定義遞歸數據類型時也一樣。如Haskell中

-- Wrong type Bad = (Int, Bad) type Evil = Bool -&> Evil

-- Right data Good = Pair Int Good data Fine = Fun (Bool-&>Fine)

如何區分Equirecursive Types和Isorecursive Types，直觀來說，Iso-recursive types類型的遞歸，在語法上顯式就「告訴」編譯器我要用遞歸結構，Haskell/Ocaml在定義遞歸函數時，是在模式匹配時區分並做相應處理的（Ocaml更絕直接rec),而遞歸數據類型，Haskell要用data或者newdata等關鍵字說明。前面那種實現，遞歸結構的出現更「自由」而不可控，比如Scheme，List可以套List，define可以像題目描述中那樣(define (fix) (lambda () (fix)))。（當然這種區分並不嚴謹）

具體原理以及實現要講清楚可能要敲type rule，畫圖什麼的。待續。。

fdsfd

@Jks Liu 我「精心構造」了一個y combinator。

【如果你知道這個可以的話，不要噴我，我只是覺得你的答案有點誤解人，讓人覺得haskell要遞歸必須用自帶的，不能不用它而自己寫一個像Y combinator那樣的】

其實你可以用recursive data type模擬recursive function type

-- Y.hs module Y where

newtype F a = F { unF :: F a -&> a } y = f -&> (x -&> x (F x)) (x -&> f (unF x x))

在GHCi中測試

*Main&> :t y y :: (a -&> a) -&> a *Main&> take 5 (y (1:)) [1,1,1,1,1]

說明確實沒什麼問題

newtype其實只是在編譯期有效，編譯完了就沒了，所以以上的F和unF都可視作id

（台下：不對呀，這是解釋執行的，不是編譯的！）

好吧我們試一試

===【警告！前方高能，非戰鬥人員迅速撤離！】===

（是的我把提示符改了，你管不著）

bash$ cat Y.hs module Y where


newtype F a = F { unF :: F a -&> a }
y = f -&> (x -&> x (F x)) (x -&> f (unF x x))
bash$ ghc --version

The Glorious Glasgow Haskell Compilation System, version 7.6.3

bash$ ghc -c Y.hs

ghc: panic! (the impossible happened)

  (GHC version 7.6.3 for x86_64-unknown-linux):

	Simplifier ticks exhausted

    When trying UnfoldingDone x{v aeL} [lid]

    To increase the limit, use -fsimpl-tick-factor=N (default 100)

    If you need to do this, let GHC HQ know, and what factor you needed

    To see detailed counts use -ddump-simpl-stats

    Total ticks: 4762

Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug

好吧Jks Liu你贏了。。。

【這是個已知的bug】

有。

以下是Haxe源碼，Main.hx

typedef RecursiveFunction = Int-&>RecursiveFunction;

class Main { static function main() { function f(i):RecursiveFunction { trace(i); return f; } f(1)(2)(3)(4)(5)(6); } }

執行一下試試：

$ haxe --run Main Main.hx:6: 1 Main.hx:6: 2 Main.hx:6: 3 Main.hx:6: 4 Main.hx:6: 5 Main.hx:6: 6

能支持遞歸函數類型。

再換Scala試試，Main.scala

import scala.language.existentials object Main { def main(arguments:Array[String]) { type RecursiveFunction = T forSome { type T &<: Int =&> T } def f:RecursiveFunction = { i:Int =&> println(i) f } f(1)(2)(3)(4)(5)(6) } }

執行：

$ scala Main.scala 1 2 3 4 5 6

也沒問題啊。

@vczh 說遞歸函數類型沒有用，簡直蠢到死。下面是我去年寫的CSV解析器，就用了遞歸函數類型來定義狀態機：

https://github.com/qifun/haxe-import-csv/blob/master/src/haxe/com/qifun/importCsv/CsvParser.hx#L39

Haskell 類型推導需要得到一個確定的類型。fix () = ()-&>(fix ()) 無法為 fix 推導出一個確定的類型。

首先，對應 (define (fix) (lambda () (fix))) 的不是是 fix () = ()-&>(fix ()) ，因為這個函數是接受 () 作為參數的，例如 cc () = 1, cc :: Num a =&> () -&> a

其次， (define (fix) (lambda () (fix))) 定義下，對 fix 求值是不會終結的，在這個意義下：

fixPointer :: (s -&> s) -&> s fixPointer f = f (fixPointer f) id :: a -&> a id x = x fix :: s fix = fixPointer id

這樣定義的 fix 不知是否和 (define (fix) (lambda () (fix))) 更加類似。

你是說 $phi = lambda a. phi$ 這種？它類型確實可以居留成 $mu au.alpha ightarrow au$ ，至於 Haskell 之類為啥不加入它，估計——就是懶……OCaml 貌似是能支持這種類型的。

golang可以定義recursive type，function type和其他的也沒什麼不同，所以可以定義recursive function type。例如

type Bar func() Bar // 返回類型和函數類型一致

一個自己返回自己的函數

var bar Bar bar = function() Bar { return bar }

上面這樣的函數，可以用來做visitor，例如 generrorcheck/generrorcheck.go at master · reusee/generrorcheck · GitHub，用來匹配符合特定條件的序列，十分靈活。

還有的常見用法是做狀態機，例如

package main


func main() {

	type State int

	type Machine func(*State) Machine
	var start, run, stop Machine

	start = func(s *State) Machine {

		*s = 1

		return run

	}

	run = func(s *State) Machine {

		if *s == 10 {

			return stop

		}

		*s++

		return run

	}

	stop = func(s *State) Machine {

		print(*s)

		return nil

	}

m := start var s State for m != nil { m = m(s) } }

Go Playground

將int狀態累加到10。更複雜的狀態機也是同樣的結構。例如text/template/parse/lex.go里的

type stateFn func(*lexer) stateFn

go/lex.go at master · golang/go · GitHub

Rob Pike有個talk解說了這個lexer

http://www.youtube.com/watch?v=HxaD_trXwRE

我從Engineering的角度說吧。如果你說的是Fuck = Shit -&> IO Fuck，那這種肯定不是你說的recursive function，你說的recursive function我認為是Fuck = Shit -&> Fuck這樣子的東西。

你說這種函數有什麼用？沒有用的。你無論寫出一個什麼樣的代碼，它的類型滿足這個條件，你都會發現你這個函數——沒有用。

Go函數作為值與類型

化簡（思路類似於 $lambda$ -calculus中的 $eta$ relation）

(define (fix) (lambda () (fix)))

得：

(define (fix) fix)

相當於Haskell中的

let fix = fix

引用這個fix會導致無限循環。

至於

(define (f x) f)

在Haskell中就無法表示了，但我們確定它是下面這個函數的Fixed Points：

let g t x = t

但在Haskell中很難直接地寫出Y Combinator，即使你精心構造出來了，計算Y(g)的時候，同樣會得到infinite type的錯誤。

我覺得，這裡用Y Combinator是不行的，需要一個Yv Combinator，可是我沒找到如何在Haskell中實現Yv的方法，也許根本就無法實現，或者即使實現出來了也是和Y同樣的命運。

Quiz：

為什麼Scheme就可以呢？

覺得不僅僅需要放鬆「類型推導必須停機」這條規則，可能還得引入類似於解方程的手段。

隱約覺得約定一個函數的類型和數字的對應關係，就能拿它做計算了（逃