I gave the entry *logical relation* an Idea-section, blindly stolen from a pdf by Ghani that I found on the web. Please improve, I still don’t know what a “logical relation” in this sense actually is.

Also, I cross-linked with *polymorphism*. I hope its right that “parametricity” may redirect there?

In computer science, a Monad is always an Applicative Functor. It’s regarded as intermediate structure between functors and monads.

And it is the programming equivalent of lax monoidal functors with tensorial strength in category theory. So a Monad in programming is always a lax monoidal functor with tensorial strength.

Exactly how is this possible? What I know about Monad in programming is that they are equivalent to a monad on a ’type category’ which has ’data types’ as objects and ’pure functions’ as morphisms. Since data types can always be seen as a set of values, the type category is like a subcategory of Set. Actually an arbitrary subcategory because languages can support any types as they want.

I got to know that every monad in Set are strong monad, which has tensorial strength by definition. I tried to prove that they eventually form a monoidal functor, but I failed. I could make two different possible candidate for coherence maps from given tensorial strength and costrength, but couldn’t prove that they satisfy the commutation condition for the coherence maps.

The only thing I could find was that strong monads are monoidal monad (and thus monoidal functor) if they are commutative. However, monads are not commmutative in general even in Set. There are many monad which are not commutative in Set, including free monoid monad. (I think they are equivalent to List in programming.)

Just proving that every monad in Set are monoidal functor may not be that hard. I rather want to know more fundamental, or generalizable reason behind that (If exist).

If I’m not wrong, it seems that every monad in Set are indeed monoidal functor even when they are not commutative. What makes this behavior? What makes every monad or strong monad in certain category be always monoidal functor, even when they are not commutative?

I am not a math major and still new to this area. I just got curious about some fundamental things behind tools I have used. I apologize if I said something stupid here.

]]>I created a page for bitcoin, based on the page bitcoin (zoranskoda) in my personal lab.

]]>I created a page (based on the Ethereum (zoranskoda) page in my personal lab) about the blockchain platform Ethereum.

]]>started a bare minimum at *state monad*

This page so far contains mainly links and the definition from the wikipedia. The page is more or less copied from digital identity (zoranskoda) and linked from distributed computing.

]]>A stub created for smart contracts, primarily focus on the blockchain realization of the idea, with link to the wikipedia and smart contract (zoranskoda).

]]>I’ve started writing duploid which generalizes thunk-force category to include negative types as well as positive.

The missing concept for category with runnable monad as a version of thunk-force category for negative types was introduced in the same thesis as duploid but without much explicit definitions since it is immediately subsumed by duploids.

More to come, especially the relationship to adjunctions.

]]>Stub for semantics of a programming language.

]]>started a minimum at *continuation monad*, but not really good yet

created a stub for *completion monad*.

In the course of doing so I found it unfortunate that the link *constructive analysis* simply redirected to *analysis*, a page from which the constructive formulation and the point of it was hardly to be extracted. So I have split off *constructive analysis* right now. But except for a sentence pointing back to the completion monad, it just contains for the moment the list of references that we already had.