CODEWITHSUNDEEP
list-comprehensionmonadscoq
user3398169
user3398169

Reputation: 83

List comprehensions in Coq

I want to use Monad comprehensions in Coq. Since I thought it is very difficult for me to implement notations which needs MonadPlus such as [ x | x <- m, x < 4 ], I didn't try to implement such notations. I therefore wrote following code.

Notation "[ e | x <- m1 , .. , y <- m2 ]"
  := (m1 >>= (fun x => .. (m2 >>= (fun y => e)) ..))
  (x closed binder, y closed binder).

However, it didn't work and I got this error.

Error: m1 is expected to occur in binding position in the right-hand side.

I think Coq interpreted "[ m | x <- m1 , .. , y <- m2 ]" (Coq code) as "[ m | x <- ( m1 , .. , y ) <- m2 ]" (pseudo-code). But I don't have solutions for this problem. Any help would be appreciated.

Upvotes: 4

Views: 486

Answers (1)

gallais
gallais

Reputation: 12113

I don't know if such a thing is possible with Notations only. The closest I can get is something where instead of writing [ e | x <- mx , ... , y <- my ] one has to write [ x <- mx , ... , y <- my | e ].

You can do it like so:

Require Import List.

Fixpoint join {a : Type} (xss : list (list a)) : list a :=
match xss with
 | nil           => nil
 | (cons xs xss) => xs ++ join xss
end.

Definition bind {a b : Type} (xs : list a) (f : a -> list b) : list b :=
  join (map f xs).

Notation "[ e" :=  e (at level 3).
Notation "x '<-' mx '|' e ']'" := (bind mx (fun x => cons e nil))
  (at level 2).
Notation "x '<-' mx ',' f"     := (bind mx (fun x => f))
  (right associativity, at level 2).

And you can now write things like this:

Goal forall xs ys, { zs | zs = [ x <- xs, y <- map (plus x) ys | y - x ] }.

However the desugared version looks awful and the goals are pretty hard to read. If it's only for programming though, it's pretty much okay. You can even throw in some extra notations like the one for ranges:

Fixpoint range0 (n : nat) : list nat :=
match n with
 | O   => cons O nil
 | S m => cons n (range0 m)
end.

Definition range (m n : nat) : list nat := map (plus m) (rev (range0 (n - m))).

Notation "m -- n ']'" := (range m n) (at level 2).

Which lets you write things like:

Goal { xs | xs = [ x <- [ 1 -- 3 ]
                 , y <- [ 1 -- x ]
                 | x + y ] }.

Upvotes: 2

Related Questions