伊莎貝爾HOLCF不明白fixrec

Question

這是一個非常簡單的理論：

theory Test 
    imports HOLCF 
begin 
    fixrec down :: "'a u → 'a" 
    where "down (up x) = x" 
end 

它提供了以下錯誤：

Type unification failed: Clash of types "_ ⇒ _" and "_ → _" 

Type error in application: operator not of function type 

Operator: up :: ??'a → ??'a⇩⊥ 
Operand: x :: ??'b 

我試圖聲明不同的功能，但我總是得到一個類似錯誤。什麼是問題以及如何解決它？

我試圖用→替換→，但它沒有幫助。

Answer 1

單箭頭→是連續函數的空間，而雙箭頭⇒表示所有總函數的空間。 HOLCF中的所有包僅適用於連續功能。這就是爲什麼⇒不適用於大多數HOLCF。但是，必須使用ASCII中綴運算符$或\<cdot>明確書寫連續函數的函數應用程序。所以下面的工作：

fixrec down :: "'a u → 'a" 
    where "down $ (up $ x) = x" 

同樣，對於連續函數拉姆達抽象使用大寫字母Λ，而不是一個小λ。