A type-based semantics for user-defined marshalling in polymorphic languages