Recently, I heard that quotient types are dual to subclassing. What do you mean with “non-termination of infinitary rewrite systems”? And, strategy is just a way to deal with non-confluence. Monads are the continuation-passing style translation that (formulas-as-types) corresponds to Gödels double negation translation of classical logics into constructivist logics, that is, embedding the computational interpretation of Turing machines into models of simulating interaction machines.
I think I’m missing the joke here
Monad tutorials come in many different forms:
This is just pointing out how silly and not useful they are to most people.
Recently, I heard that quotient types are dual to subclassing. What do you mean with “non-termination of infinitary rewrite systems”? And, strategy is just a way to deal with non-confluence. Monads are the continuation-passing style translation that (formulas-as-types) corresponds to Gödels double negation translation of classical logics into constructivist logics, that is, embedding the computational interpretation of Turing machines into models of simulating interaction machines.