@edwinbrady asking because I couldn’t find a decent answer online... is there a canonical way to cache (memoize) functions in Idris? In Haskell, it seems to be a PhD-sized problem 
I haven't really thought about it. I'd expect it's similar to the problem in Haskell.
-
-
In Haskell, for pure functions, you can often rely on laziness, famous fibs = 0:1:zipWith (+) fibs (tail fibs) fib n = fibs !! n (MemoTrie e.g. uses trie to avoid linear cost of lookup) More real-world example is calculating edit-distance...
-
... but it’s probably isn’t as convinient in Idris, and you’ll experience similar problems as when writing recursion schemes library (i.e. termination checker is not smart enough)
- 4 more replies
New conversation -
-
-
Tangent: in the scheme backend for Idris2 I recently noticed that zero-arity bindings, being encoded as zero-arity scheme lambdas, cause reevaluation at every occurrence. Considering experimenting with emitting thunks there if I can figure out more of the codegen.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.