Email Gateway (Aug 22 2022 at 20:07): Email Gateway (Aug 22 2022 at 20:07):From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users,
I recently discovered the HOL-Library.Monad_Syntax theory with its
(>>=) and do-notation. While defining an inductive predicate using
multiple bind operations, I encountered the following error message.
Unresolved adhoc overloading of constant bind
I minimized the my code until I noticed that the error only occurs with
two or more binds and can be resolved by adding parenthesis on the left
operands.
theory Scratch
imports Main "HOL-Library.Monad_Syntax"
begin
context
fixes f :: "nat ⇒ 'a ⇒ 'a option" and x :: "'a"
begin
declare [[show_variants]]
term "Some x >>= f 0"
(* "Option.bind (Some x) (f 0)" :: "'a option" *)
term "Some x >>= f 0 >>= f 1"
(* Unresolved adhoc overloading of constant bind *)
term "((Some x) >>= f 0) >>= f 1"
(* "Option.bind (Option.bind (Some x) (f 0)) (f 1)" *)
end
end
I checked the source code of Monad_Syntax and noticed that it is
declared as infixr ">>=" 54. I was quite surprised because such a
choice requires one to add extra parenthesis in what seem to be common
cases and the traditional Haskell (>>=) operator itself is left associative.
What is the reasoning for the Isabelle (>>=) to be right and not left
associative? What are situations where it makes more sense?
Best regards,
Martin Desharnais
signature.asc
Email Gateway (Aug 22 2022 at 20:09):From: Christian Sternagel <c.sternagel@gmail.com>
Just as another data point: I also don't remember any specific reasons
for >>= being infixr.
And, like sel4, in IsaFoR we mostly use do-notation (683 occurrences)
over explicit binds (20 occurrences).
cheers
chris
Email Gateway (Aug 22 2022 at 20:10):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Martin,
We have made "bind" left-associative now, which is customary and makes more
sense. Thank you for notifying us.
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC