Utrecht University and

This paper presents a library for programming with polymorphic dynamic types in the dependently 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 compro-mising type soundness. There are situations where the types of the values that a program manipulates are not known during compilation. This is typically the case when data, or even parts of the program itself, are obtained by interacting with the ‘outside ’ world: when values are ex-changed between applications by deserialization from disk, input is provided by a user, or part of a program is obtained over a network connection. Modern statically typed functional languages, such as Clean (van Eekelen et al., 1990), Haskell (Peyton Jones, 2003), and OCaml (Leroy et al., 2011), all support some form of dynamic typing, that allows programmers to defer type checking until runtime. These languages define a special type for dynamically typed values. We will abbreviate such dynamically typed values to dynamic value or just dynamic. A dynamically typed valu