Home » forums » LtU Forum

Typed lambda calculii with type-indexed families of functions instead of polymoprhic functions?

From by basic understanding, in System F, a polymorphic function is a single value that can be directly applied to an argument. I want to know: is there a formalism where a "polymorphic function" is really a declaration of a family of monomorphic functions, indexed by the types used for instantiation. Thus, two calls to the same [nominal] polymorphic function with different types would resolve to two calls to different monomorphic functions. Clearly this model is more towards the C++ idea of function templates than the FP idea of polymorphic functions.

For polymorphic functions with these semantics, it seems that there would be a more clear distinction of what can be resolved at compile-time, using the type information available at instantiation, and what needs run-time dispatch. Perhaps, then, this formalism could also be used as a target language of an optimization that specializes true (System F) polymorphic functions.

So, does anyone know any work in this direction?
Thank you!

By andhow at 2009-01-12 17:13 | LtU Forum | previous forum topic | next forum topic | other blogs | 4059 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Staging would suit your

Staging would suit your purposes: a polymorphic function can be interpreted as a staged function definition, where the type of the parameter is provided by clients. See MetaOCaml.

MLTon and BitC perform specialization of polymorphic functions, so perhaps they have some sort of intermediate language that would also be suitable.

By naasking at Mon, 2009-01-12 17:56 | login or register to post comments

Thanks for the links to

Thanks for the links to MLTon and BitC!

Meta-programming seems to be a big hammer...

By andhow at Mon, 2009-01-12 19:57 | login or register to post comments

See Harper & Morisett 1995

Compiling Polymorphism using Intensional Type Analysis. This spawned a fair amount of follow-up work, and the phrase to google for to find it is "intensional type analysis".

By neelk at Mon, 2009-01-12 22:31 | login or register to post comments

Thanks, I'll need to read

Thanks, I'll need to read more about this.

By andhow at Tue, 2009-01-13 01:10 | login or register to post comments