如何从Idris中的fastPack获取正常值？

Question

我对 Idris2 中

pack

和

fastPack

函数之间的区别感到困惑（截至 0.7.0）。两者都有相同的签名：

:t pack
Prelude.pack : List Char -> String
:t fastPack
Prelude.fastPack : List Char -> String

pack

按照宣传的方式工作，并将

Char

列表转换为

String

。

pack ['a'] ++ pack ['b']

渲染：

"ab"

但我似乎无法从

String

中得到

fastPack

。

fastPack ['a'] ++ fastPack ['b']

渲染：

prim__strAppend (fastPack ['a']) (fastPack ['b'])

我不确定这里是否存在一些懒惰。但我正在测试的一些基本代码使用了

fastPack

，因此结果表达式很快就会变大。

有没有办法从这些fastPack表达式中获取正常的字符串值？

（在这个例子中，“ab”来自

prim__strAppend (fastPack ['a']) (fastPack ['b'])

。我尝试了

show

和

force

，但没有成功。）

Answer 1

我对 Idris2 中

pack

和

fastPack

函数之间的区别感到困惑

pack

在 Idris 中实现：

||| Turns a list of characters into a string.
public export
pack : List Char -> String
pack [] = ""
pack (x :: xs) = strCons x (pack XS)

fastPpack

是一个外部函数:

%foreign
    "scheme:string-pack"
    "RefC:fastPack"
    "javascript:lambda:(xs)=>__prim_idris2js_array(xs).join('')"
export
fastPack : List Char -> String

ECMAScript 实现仅使用

Array.prototype.join

。

Chez 后端中的

Scheme 实现看起来像这样：

(define (string-pack xs) (list->string xs))

以及 在 Gambit 后端：

(define-macro (string-pack xs)
  `(apply string ,xs))

以及在球拍后端：

(define (string-pack xs) (list->string xs))

对于C后端，是这样实现的：

char *fastPack(Value *charList) {
  Value_Constructor *current;

  int l = 0;
  current = (Value_Constructor *)charList;
  while (current->total == 2) {
    l++;
    current = (Value_Constructor *)current->args[1];
  }

  char *retVal = malloc(l + 1);
  retVal[l] = 0;

  int i = 0;
  current = (Value_Constructor *)charList;
  while (current->total == 2) {
    retVal[i++] = ((Value_Char *)current->args[0])->c;
    current = (Value_Constructor *)current->args[1];
  }

  return retVal;
}

有没有办法从这些fastPack表达式中获取正常的字符串值？

这需要与 Idris 的 FFI 比我更加亲密。

有趣的是，定义了一个

%transform

，它将自动将

pack

替换为

fastPack

：

-- always use 'fastPack' at run time
%transform "fastPack" pack = fastPack