如何从 JavaScript 调用单个 Idris 函数？

Question

假设我在 Idris 中有一个函数可以进行一些计算。为了简单起见，现在将其设置为字符串类型。

f: String -> String

如何将此函数编译为 JavaScript，以便可以从任何普通 JavaScript 代码中调用它？

如果这太简单了，假设f，而不是String，处理Double甚至自定义 Idris 数据类型。

我知道我可以用一个Main.main函数编译整个模块，并且或多或少会输出一些难以理解的 JavaScript 代码。我可以手动从那里提取我的功能吗？我该怎么办？

---

PS尽管我自己回答，但我仍在寻找更好的解决方案，所以欢迎。

Answer 1

是的，您可以手动提取任何函数。

1. 构建模块如下：

   module Main
   
   import Data.String
   
   f: Double -> Double
   f x = x + 1
   
   interact: String -> String
   interact s = let x = parseDouble s in
       case x of
            Nothing => "NaN"
            Just x => show (f x)
   
   main: IO ()
   main = do
       s <- getLine
       putStrLn (interact s)
   

2. 编译如下：

   module Main
   
   import Data.String
   
   f: Double -> Double
   f x = x + 1
   
   interact: String -> String
   interact s = let x = parseDouble s in
       case x of
            Nothing => "NaN"
            Just x => show (f x)
   
   main: IO ()
   main = do
       s <- getLine
       putStrLn (interact s)
   

   Main.js将创建一个名为的文件。正如您所说，将会有几兆字节或多或少难以理解的 JavaScript 代码。

3. 手动编辑此文件并进行与此类似的编辑：

   --- Resistors.js
   +++ Resistors-default.js
   @@ -1,7 +1,5 @@
    "use strict";
   
   -(function(){
   -
    const $JSRTS = {
        throw: function (x) {
            throw x;
   @@ -36130,7 +36128,3 @@
            }
        }
    }
   -
   -
   -$_0_runMain();
   -}.call(this))
   

4. 现在请注意，这个 JS 文件中有注释，用 Idris 名称标记了 JS 函数。例如，与我们的interact函数相对应的是这个 JS 函数：

   // Main.interact
   
   function Main__interact($_0_arg){
       const $_1_in = Data__String__parseDouble($_0_arg);
   
       if(($_1_in.type === 1)) {
           const $cg$3 = Main__bestMatch_39_($_1_in.$1, Main__manyResistors_39_());
           let $cg$2 = null;
           $cg$2 = $cg$3.$1;
           return Prelude__Show__Main___64_Prelude__Show__Show_36_Schema_58__33_show_58_0($cg$2);
       } else {
           return "NaN";
       }
   }
   

5. 如果您将此 JS 文件作为脚本附加到网页，则可以在浏览器中打开 JS 控制台并与 Idris 函数交互，如下所示：

   Main__interact("10")
   "11"
   

希望这可以帮助！