A library for polymorphic dynamic typing

摘要

This paper presents a library for programming with polymorphic dynamic types in the dependency typed programming language Agda. The resulting library allows dynamically typed values with a polymorphic type to be instantiated to a less general (possibly monomorphic) type without compromising type soundness.