我刚刚开始学习Idris,我正在阅读" 使用Idris进行类型驱动开发 "一书.第二章的示例练习之一是编写一个函数,给定一个字符串,该函数确定该字符串中单词的平均长度.我的解决方案如下:
average : String -> Double
average phrase =
let werds = words phrase
numWords = length werds
numChars = the Nat (sum (map length werds)) in
cast numChars / cast numWords
但是,由于这numChars条线,我在解决这个问题时遇到了很多麻烦.出于某种原因,除非我明确使用类型,否则不会进行类型检查the Nat.错误说明:
Can't disambiguate since no name has a suitable type:
Prelude.List.length, Prelude.Strings.length
这对我来说并没有多大意义,因为无论使用哪个定义length,返回类型都是Nat.这一点得到了以下事实的支持:在REPL中可以无错误地完成相同的操作序列.这是什么原因？
我一直在努力优化一个有很多内存泄漏问题的程序.泄漏现在已经消失,但主要GC的偶尔运行仍然对PS老一代产生了良好的影响.我知道我可以通过运行时检查基本的整体内存信息,但是可以在程序中检查PS eden,PS幸存者和PS旧的使用情况吗？