'behaviour of Isabelle foldl compared to SML

being a beginner of Isabelle I tried to transcribe a simple programming task from rosettacode.org 100 doors based on the Standard ML implementation.

I checked the SML code in this online SML interpreter and especially the call of foldl, which worked fine.

When applying Isabelle's foldl i get an 'Type unification failed' error for function run, which is unexpected, since i tried to transcribe the SML original very closely. Any hints for what the problem is? Thanks a lot!

My code so far:

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 )"

The error message is

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
smlfoldisabelle


Solution 1:[1]

Let's compare the Isabelle version of foldl,

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

with the SML one: foldl f init [x1, x2, ..., xn] returns f(xn,...,f(x2, f(x1, init))...) or init if the list is empty.

They are close, but note that in the SML one, f takes a pair. In Isabelle, the arguments of f are curried. You need to redefine pass accordingly.

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Lawrence Paulson

Related Questions