quick ixmonad and examples

[jldodds]

No description provided.

[gmalecha]

I meant to get back to you earlier about this. I think developments like this are great, but I've been wondering if they should be split into separate libraries. What do you think of making coq-el-indexed (we can put it in this organization) and release it as a separate package?

[jldodds]

That makes sense, although this would be a pretty small package, the only instances I'm aware of are state and cont.

It's completely reasonable to close this until someone has time/interest to actually get a complete implementation done.

[gmalecha]

It wouldn't be as small as some node.js packages. :-)

What is left for a "complete implementation"?

[jldodds]

It's certainly usable as is, so maybe nothing needs to be added

[liyishuai]

@gmalecha Should we merge this PR?

[gmalecha]

I don't have any real technical objections to merging this, but I think the question is whether ExtLib should grow and/or shrink. Does it make sense to release separate packages with add-on functionality like indexed monads? What needs to be in the core?

[liyishuai]

It'll make sense to release a separate package if no future code in ExtLib would depend on such add-ons.
I'd prefer having ExtLib as a growing and shrinking library where the community can contribute functionalities they find generically useful and should not redefine everywhere. When some code were adopted by Coq standard library, we should remove them from here.
Some functionalities could come in different styles (e.g. monad notations), and the Coq team might have difficulty deciding which one to include in standard library. In this case, ExtLib can host one or many of them, allowing users to choose.