Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with exported Haskell code

Email Gateway (Aug 22 2022 at 14:55):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

the following Isabelle source demonstrates a problem with the code generator for Haskell.

definition foo :: "bool => bool => bool" where
"foo x y = (let z = x in if z then undefined else y)"

definition bar where "bar = (foo True True = foo True False)"

lemma bar_is_True: "bar = True"
unfolding bar_def foo_def Let_def by simp

export_code bar in Haskell

(* evaluating bar in Haskell yields False! *)

(* the problem is that the generated code for "foo" is

foo :: Bool -> Bool -> Bool;
foo x y = let {
False = x;
} in y;

which is in Haskell identical to

foo x y = y

since the “False = x” pattern match is ignored

*)

Cheers,
René

Email Gateway (Aug 22 2022 at 14:55):

From: Lars Hupel <hupel@in.tum.de>
Hi Rene,

this looks indeed suspicious. Here's the equivalent output for Scala:

def foo(x: Boolean, y: Boolean): Boolean = {
val false: Boolean = x;
y
}

Compiling this yields:

ROOT.scala:4: warning: match may not be exhaustive.
It would fail on the following input: true
val false: Boolean = x;
^

That is, this is a "pattern match" in disguise. So, the problem does not
seem to be isolated to Haskell.

Cheers
Lars

Email Gateway (Aug 22 2022 at 14:55):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Hi Lars,

However, execution of bar in Scala yields a runtime error as desired (which corresponds to invoking Isabelle’s “undefined”).
This is in contrast to Haskell, where bar is executed without error and returns the Boolean False.

Cheers,
René

Email Gateway (Aug 22 2022 at 14:56):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rene,

thanks for investigating this.

The attached theory simplifies the example further and demonstrates that
it affects any case expression with just one clause.

After studying https://wiki.haskell.org/Lazy_pattern_match I came to the
conclusion that when generating code for Haskell let clauses cannot be
used for pattern matching, only local variable definitions. I will dive
into the code…

Cheers,
Florian
Haskell.thy
signature.asc

Email Gateway (Aug 22 2022 at 14:56):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The attached patch is currently in test.

Florian
Haskell.thy
haskell
signature.asc

Email Gateway (Aug 22 2022 at 14:56):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Florian,

thanks for the patch. According to CeTA I can inform you that there the patch
works without problems, i.e., the export_code for CeTA works, compiles and behaves
as expected on examples.

Cheers,
René

Email Gateway (Aug 22 2022 at 15:24):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The problem will be finally resolved in the next Isabelle release.

Cheers,
Florian
signature.asc

Last updated: Apr 16 2024 at 12:28 UTC