User loginNavigation |
Unifying functions and functorsI recently came across the PML language, which aims to realize "the great unification between records/structures/modules/objects and functions/functors/methods". Sounds great, but it lead me to wonder exactly why there is a distinction between functions and functors in the first place. Is this simply because in all current languages, the module language is separate from the term language? Does anyone have any references on functors that might clarify why functions and functors are currently distinct? Given the explanation of categories in the last link, I might hazard that functions are arrows/morphisms mapping objects within a single category, and functors map objects between different categories, ie. functions operate on objects within a category, functors on entire categories. If that's accurate, then would "the great unification" involve reifying categories/modules at the term level somehow? If not, what does this "great unification" involve? The only reference to "functor" in the PML manual is on page 8: /\id:a -> b : dependent types are allowed in PML. They are useful to write the type of functors: functions that handle structures with type in their fields. Here is an example of such a dependant type with a value of this type: type F = /\s:{ type p = [ A[] | B[] ] val q : p } -> s.p val f:F s = s.q Any clarification is much appreciated. :-) By naasking at 2007-08-07 15:29 | LtU Forum | previous forum topic | next forum topic | other blogs | 6134 reads
|
Browse archives
Active forum topics |
Recent comments
27 weeks 2 days ago
27 weeks 2 days ago
27 weeks 2 days ago
49 weeks 3 days ago
1 year 1 week ago
1 year 3 weeks ago
1 year 3 weeks ago
1 year 5 weeks ago
1 year 10 weeks ago
1 year 10 weeks ago