I realize this is a pretty big feature, but having the ability to interact back and forth between the two in a "natural" way would vastly increase the accessibility of Idris. I only just started out with Idris2 but by having snooped through its workings bit, it seems very possible to accomplish this task. I will be exploring this idea and try to figure out specifics etc.

• Idris2 Feature Proposal: TypeScript and ECMAScript Interfacing
  • Disclaimers on Scope
    • My Focus is on NodeJS
    • This will target the modern Environment
    • No CommonJS modules
    • Integration of Idris code into a NodeJS project should be smooth
    • Additional Notes
  • Some preliminary Outlines and Notes
    • Runtime loading of Idris source code
    • Output structure
    • Build tools
    • Small Standard Libraries
    • Strong FFI for calling JS functions in Idris
    • Clear error handling
    • Look into fully supporting EcmaScript style IdentifierName
      • Excerpt from ecma262 11.6

Some notes on what aren't thing I'm planning to focus on.

I'm not very experienced with JS/ES in the browser, and won't be focusing on browser-specific functionality. This could always be implemented at a later stage.

A Lot of headaches and potential problems can be avoided if the powers of the modern ecosystem can be leveraged. And everything will be a lot easier if no considerations have to be made for supporting older versions of TypeScript, NodeJS and ECMAScript. Secondary transpiling should be able to provide most if not all of the support for older/legacy versions and variations and thus are not a focus. More specifically this means:

1. Primary focus will be on the current semver-major of TS and Node
2. Secondary focus will be supporting [Maintenance-LTS] of NodeJS
3. No particular focus should be given to any older parts of the environment as this will vastly increase the necessary workload and probability of issues arising from accommodating legacy-compatibility.
4. For the time being, if any specific work for browser-interop is in the works, it should be prepared handle interoperability issues arising from modern TC39 specification and syntax fully implemented in the V8 engine (Chrome/NodeJS), but without --or with dubious-- implementation in other engines (eg. FireFox/Spidermonkey, Safari/JavaScriptCore) outside of the main code.

ECMAScript modules have been implemented in a stable fashion in NodeJS and across browsers for quite a while now. They make many things a lot easier and since they can seamlessly use CJS modules --but not the other way around--, it would be a major hassle to support them.

The main goal is to make Idris accessible to the NodeJS ecosystem, not the other way around. Anything that makes it smoother for TypeScript/ECMAScript to be integrated into an Idris project is very much desired, but a secondary focus.

• It's possible that it will end up making sense to use a dialect for better integration. It should not be a major deviation if possible.
• This doesn't necessarily have to end up being a replacement for the current JS transpiler.
• This doesn't necessarily have to be based on or extend the current JS transpiler.

This is very much a WIP section, feel free to extend it and add questions.

NodeJS has an esm_loaders api (still experimental), which could be used for loading Idris modules directly from source. Now this doesn't make much sense for production code, but it would make a nice developer tool and would make work on this project easier as well.

I've been using the ts-node/esm loader to load TypeScript at runtime since it dropped and it has been a very nice addition to the toolbox. It does make for a good reference.

The current output structure isn't very friendly to typical JS projects. It might make sense to align it more.

Look at options for build tools so they make integration as easy as possible. I'm thinking focus should be on a limited feature set but easy to use and reliable

There should be a small (optional) standard library in both languages for doing basic evaluation and analysis of the other language. Particularly for type preservation and optimization (eg. an Int32 in JS).

Using typescript style TypeGuards, Idris would not need to know or understand the nature of a function input and return value. TS TypeGuards can tell Idris whether a value is acceptable or not as an absolute truth, making it possible to leverage the full power of TypeScript type checking inside Idris.

Idris needs to be able to throw precise and useful errors resulting from interop issues.

NOTE: look out for ResrvedWord and related things

Would it be feasible to support the full range of ecma262 IdentifierName?

• U+0024 and U+005f anywhere in identifier
  • allow for $ and _ to be used as common chars in identifiers
• U+200C and U+200D anywhere after firs code point (ZERO WIDTH NON-JOINER, ZERO WIDTH JOINER)
• look into using escape sequences in identifiers

NOTE: rewritten in Extended Backus-Naur Form

IdentifierName =
  | IdentifierStart
  | IdentifierName, IdentifierPart ;

IdentifierStart =
  | UnicodeIDStart
  | '$'
  | '_'
  | '\\' , UnicodeEscapeSequence ;
  
IdentifierPart =
  | UnicodeIDContinue
  | '$'
  | '\\' UnicodeEscapeSequence
  | <ZWNJ>
  | <ZWJ> ;
  
UnicodeIDStart = 
  ; (*any Unicode code point with Unicode property “ID_Start"*)
  
UnicodeIDContinue =
  ; (*any Unicode code point with Unicode property “ID_Continue”*)