How to get normal values from fastPack in Idris?

Question

I am confused about the difference between pack and fastPack functions in Idris2 (as of 0.7.0). Both have the same signature:

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

pack works as advertised and converts a list of Chars into a String.

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

renders:

"ab"

But I can't seem to get Strings out of fastPack.

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

renders:

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

I am not sure whether some laziness is going on here. But some of the base code I am testing uses fastPack, so the result expression becomes large very quickly.

Is there a way to get the normal string value out of these fastPack expressions?

(In this example, "ab" from prim__strAppend (fastPack ['a']) (fastPack ['b']). I tried show and force, to no avail.)

Answer 1

I am confused about the difference between pack and fastPack functions in Idris2

pack is implemented in Idris:

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

fastPpack is a foreign function:

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

The ECMAScript implementation just uses Array.prototype.join.

The Scheme implementation looks like this in the Chez backend:

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

And in the Gambit backend:

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

And in the Racket backend:

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

For the C backend, it is implemented like this:

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;
}

Is there a way to get the normal string value out of these fastPack expressions?

That requires far more intimacy with Idris's FFI than I possess.

Interestingly, there is a %transform defined which will automatically replace pack with fastPack:

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