search

SMLFamily / Successor-ML

A version of the 1997 SML definition with corrections and some proposed Successor ML features added.
190 stars 10 forks source link

Higher-order functors #41

Open nilern opened 4 years ago

nilern commented 4 years ago

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 commented 4 years ago

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 notifications@github.com 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 https://github.com/SMLFamily/Successor-ML/issues/41?email_source=notifications&email_token=AALWY5K3GDJNKH3EDTWKFUDP6WLLBA5CNFSM4H7MW562YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4G6JE55A, or mute the thread https://github.com/notifications/unsubscribe-auth/AALWY5PYM3I342ZIBGXEBZLP6WLLBANCNFSM4H7MW56Q .

JohnReppy commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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!