Idris2中如何从fastPack获取正常字符串值？

两者核心区别 #

• pack：纯Idris代码实现的字符串构造函数，会把Char列表完全求值，转换成标准String类型，在REPL里直接显示成字符串字面量。
• fastPack：直接调用底层原语prim__strFromList生成字符串，返回的是底层原生字符串表示，REPL默认不会自动展开显示它的字面量，只会保留原语调用的表达式形式。

解决fastPack拼接后无法显示正常字符串的方法 #

你碰到的是REPL的显示机制问题，不是字符串本身无效，试试这两种方式：

1. 用print函数输出
   在REPL里执行：

   print (fastPack ['a'] ++ fastPack ['b'])
   

   就能直接看到输出"ab"。
2. 转成标准String表示
   通过pack . unpack把fastPack生成的原生字符串转成pack那种标准String，之后REPL就会正常显示了：

   pack $ unpack (fastPack ['a'] ++ fastPack ['b'])
   

   执行后会显示"ab"。

额外说明 #

• fastPack是为了性能优化设计的，跳过了Idris层的额外处理直接调用底层实现，所以REPL不会自动美化显示，但字符串本身是有效的，程序运行时完全能正常用。
• 你试的force没用，是因为fastPack返回的不是惰性求值类型，原生字符串不需要force；show无效可能是你直接在REPL里输show (fastPack ...)，REPL显示的是show的返回值表达式，换成print (show (fastPack ...))就能看到正确结果了。

内容的提问来源于stack exchange，提问作者thor