Can't write the Free monad in #Agda because it's not strictly positive. If we could, would constraining the functor to be strictly pos help?
Conversation
whoops! No, it wouldn't, because they already have to be...
1
Replying to
What does 'strictly positive' mean? Any reading on this I can look at?
Replying to
wiki.portal.chalmers.se/agda/pmwiki.ph is a start - i.e. negative = on the left, positive = on the right, and strictly as in only