1. "Covariance" and "contravariance" are properties of a type constructor that follow automatically from the definition of the type constructor. A type constructor is covariant if a `map` function exists and satisfies the functor laws, and contravariant if `contramap` exists and satisfies the contrafunctor laws. If neither `map` nor `contramap` ( Read more... )

Interesting papers:

http://adam.chlipala.net/papers/PhoasICFP08/
https://www.cs.utexas.edu/~wcook/Drafts/2012/graphs.pdf

The first one shows how to construct a representation of a ( Read more... )

Вынесено изъ комментовъ здѣсь https://akuklev.livejournal.com/1306754.html

( Read more... )

I have a new picture of monad transformers (as they are used in functional programming): they are pointed functors in the category of monads ( Read more... )

The usual story of parametricity is given in the paper "Theorems for free" by Wadler. https://ecee.colorado.edu/ecen5533/fall11/reading/free.pdfRead more... )

I'm trying to find a simple proof of parametricity theorems, without using relations. I hoped that I can use dinatural transformations https://en.wikipedia.org/wiki/Dinatural_transformation directly and prove that any purely functional code of type P[A, A] -> Q[A ( Read more... )

(Развернутая версiя комментарiевъ здѣсь https://www.dreamwidth.org/go?redir_type=threadroot&journal=epimorphisms_split&talkid=15546 . Предполагается, что читатель - математикъ.)

1. Разсмотримъ какой-либо языкъ программированiя, гдѣ есть "типы данныхъ" (Int, Float, String, Boolean, Array of String, ...) и они провѣряются при компиляцiи, чтобы функцiи ( Read more... )

So far there seem to exist two classes of monads that have no monad transformers ( Read more... )

Consider the functor M(p) = ∀a. (p → 1 + a) → 1 + a where p is a type parameter. I've been trying to simplify and analyze this deceptively simple expression, with not much success so far ( Read more... )

Looking at the properties of universally quantified types, I found the following transformation ( Read more... )