Table of Contents

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

Idris2 Feature Proposal: TypeScript and ECMAScript Interfacing

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
- Some preliminary Outlines and Notes

Disclaimers on Scope

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

My Focus is on NodeJS

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.

This will target the modern Environment

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:

Primary focus will be on the current semver-major of TS and Node
Secondary focus will be supporting [Maintenance-LTS] of NodeJS
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.
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.

No CommonJS modules

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.

Integration of Idris code into a NodeJS project should be smooth

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.

Additional Notes

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.

Some preliminary Outlines and Notes

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

Runtime loading of Idris source code

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.

Output structure

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

Build tools

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

Small Standard Libraries

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).

Strong FFI for calling JS functions in Idris

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.

Clear error handling

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

Look into fully supporting EcmaScript style `IdentifierName`

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

Excerpt from ecma262 11.6

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”*)