Intension and Extension?

I wrote the following code.

foreach(var e1 in
  from table_1
  where table_1.field_1 == 3
  select table_1) {

  foreach(var e2 in
    from table_2
    where table_2.field_2 == e1.field_1a
    select table_2) {

    foreach(var e3 in
      from table_3
      where table_3.field_3 == e2.field_2b
      select table_3) {
      ...
    }
  }
}

But the query of that code can be written in SQL as following:

SELECT *
FROM TABLE_3,
  (SELECT *
  FROM TABLE_2,
    (SELECT *
    FROM TABLE_1
    WHERE TABLE_1.FIELD_1 = 3
    ) X
  WHERE TABLE_2.FIELD_2 = X.FIELD_1A
  ) Y
WHERE TABLE_3.FIELD_3 = Y.FIELD_2B

In the former code, the loop is expanded inside. But the SQL is expanded outside.
It is interesting but I do not know that it is significant.

Using Xaml for design document

I got an idea that we use Xaml for design document.

For example, view/state transition diagrams, ER diagrams and flow charts etc.

I want tools to create design documents in Xaml formats.

Have such tools been yet?

I am learning Coq.

But my learning speed is slow...

I want to apply Coq for describing application specifications.
But I do not think that I use Coq directly to describe application specifications.
I convert specifictions in natural language(but formal to some extent) to Coq language and process them by Coq.

Does it work good ?

Comonad in Coq

I am interested in Coq.
We can use Coq for proving the satisfaction for the monad laws when we define the Monad-type structure.

I want to prove the comonad laws for stream comonad using Coq.
But it's so difficult for me... .

Monad and Comonad

Monad is famous for the sake of Haskell.
But I think that comonad is not famous.
This site describe the Store Comonad.
I write this Store Comonad in F#.

type Store<'b, 'a> = ('b -> 'a) * 'b

let Store v b : Store<'b, 'a> = (v, b)

let extract ((v, b) : Store<'b, 'a>) = v b
let fmap (f : 'a -> 'c) ((v, b) : Store<'b, 'a>) = Store (f << v) b let duplicate ((v, b) : Store<'b, 'a>) = Store (Store v) b
let extend (f : Store<'b, 'a> -> 'c) (x : Store<'b, 'a>) = fmap f (duplicate x)