Skip to content

bindA is incoherent with the associativity of >>= #164

@garrigue

Description

@garrigue

bindA has type (m >>= f) >>= g = m >>= (fun x => f x >>= g), which means that it moves parentheses from left to right.
However, >>= is left associative, so that bindA augments the number of parentheses.
This is incoherent with usual orientation of associativity lemmas.

Proposed solution: make it non-associative.

Note that from a computational point of view, it might be more natural for >>= to be right-associative, but as discussed for Haskell this is not possible since >>= is heterogeneous. Haskell makes it left-associative too.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions