Higher-order functors

[nilern]

Higher-order functors are an old and obvious extension.

I think the only problem is whether defunctorizers like MLton can support them. I suspect that the module language would still be normalizing (since it can be reduced to a subset of System F(omega)) so the defunctorizer would still terminate instead of infinite expansion. Extending the actual algorithms would surely be nontrivial.

[RobertHarper]

I don't think these create any difficulties for implementation. An old paper by H, Mitchell, and Moggi shows how to reduce higher-order modules to structures in a systematic way. (c) Robert Harper. All rights reserved.

…

On Wed, Jul 10, 2019 at 4:17 AM Pauli Jaakkola ***@***.***> wrote: Higher-order functors are an old and obvious extension. I think the only problem is whether defunctorizers like MLton can support them. I suspect that the module language would still be normalizing (since it can be reduced to a subset of System F(omega)) so the defunctorizer would still terminate instead of infinite expansion. Extending the actual algorithms would surely be nontrivial. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#41?email_source=notifications&email_token=AALWY5K3GDJNKH3EDTWKFUDP6WLLBA5CNFSM4H7MW562YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4G6JE55A>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AALWY5PYM3I342ZIBGXEBZLP6WLLBANCNFSM4H7MW56Q> .

[JohnReppy]

I've been lobbying for adding defunctorization to SML/NJ. Since we have separate compilation, we will need to pickle the abstract syntax (absyn) that is produced by the type checker and beta-reduce functors when they are applied. For higher-order functors, we may have to pickle the result, since we will only generate code once the functor has been reduced to a structure.

[MatthewFluet]

Also, a recent paper by Elsman et al. (Static interpretation of higher-order modules in Futhark: functional GPU programming in the large, https://dl.acm.org/citation.cfm?doid=3243631.3236792) shows the defunctorization of higher-order modules works as one would expect.

[nilern]

I've been lobbying for adding defunctorization to SML/NJ. Since we have separate compilation, we will need to pickle the abstract syntax (absyn) that is produced by the type checker and beta-reduce functors when they are applied. For higher-order functors, we may have to pickle the result, since we will only generate code once the functor has been reduced to a structure.

Sounds similar to Elsman's thesis?

Also, a recent paper by Elsman et al. (Static interpretation of higher-order modules in Futhark: functional GPU programming in the large, https://dl.acm.org/citation.cfm?doid=3243631.3236792) shows the defunctorization of higher-order modules works as one would expect.

So all the details have already been worked out. Nice!