与 SML 相比，Isabelle foldl 的行为

Question

作为 Isabelle 的初学者，我尝试根据标准 ML 实现从 rosettacode.org 100 doors 中转录一个简单的编程任务。

我检查了这个 online SML interpreter 中的 SML 代码，尤其是 foldl 的调用，它工作正常。

在应用 Isabelle 的 foldl 时，我收到函数 run 的 'Type unification failed' 错误，这是意外的，因为我试图非常仔细地转录 SML 原件。有什么问题的提示吗？非常感谢！

到目前为止我的代码：

theory "100_doors"
  imports Main
begin

datatype Door = Closed | Opened
 
fun toggle :: "Door ⇒ Door" where
"    toggle Closed = Opened" |
"    toggle Opened = Closed"

fun runs :: "nat ⇒ nat list" where
 "runs n = upt 1 (n+1) "
value "(runs 3)"

(* functions using tuples *)
fun initial_doors :: "nat ⇒ (nat * Door) list" where
 "initial_doors m = map (λn. (n, Closed)) (runs m)"
value "(initial_doors 3)"

(* tuple of number_of_doors and a list of index_door tuples *)
fun pass :: "nat * ((nat * Door) list) ⇒ (nat * Door) list" where
" pass (step, doors) = 
   map (λ(index, door). (
    if (index mod step) = 0
    then (index, toggle door)
    else (index, door)
   ))
  doors"
value "pass (2, (initial_doors 2))"

fun run :: "nat ⇒ (nat * Door) list" where
  "run number_of_doors = foldl pass
    ( initial_doors number_of_doors )
    ( runs number_of_doors )"

错误信息是

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

Type error in application: incompatible operand type

Operator:  foldl ::
  (nat × (nat × Door) list ⇒ ??'a ⇒ nat × (nat × Door) list)
  ⇒ nat × (nat × Door) list ⇒ ??'a list ⇒ nat × (nat × Door) list
Operand:   pass :: nat × (nat × Door) list ⇒ (nat × Door) list

Answer 1

我们来比较一下伊莎贝尔版的foldl，

foldl_Nil:  "foldl f a [] = a" |
foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"

使用 SML：foldl f init [x1, x2, ..., xn] returns f(xn,...,f(x2, f(x1, init))...) 或 init 如果列表为空。

它们很接近，但请注意，在 SML 中，f 取一对。在 Isabelle 中，f 的参数是柯里化的。您需要相应地重新定义 pass。

与 SML 相比，Isabelle foldl 的行为

behaviour of Isabelle foldl compared to SML

sml

fold

isabelle