Journal of Functional Programming

Table of Contents - 2009 - Volume 19, Issue 02  

Theoretical Pearls

Coherence of subsumption for monadic types

JAN SCHWINGHAMMERa1

a1 Programming Systems Lab, Saarland University, 66041 Saarbrücken, Germany (e-mail: jan@ps.uni-sb.de)

Abstract

One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A ≤ B are interpreted via conversion functions A → B. This paper shows how to extend the method to languages with computational effects, using Moggi's computational metalanguage.