Idris 2: Quantitative Type Theory in Practice
This sounds very neat in principle, but it doesn’t seem very easy to understand the code in practice. In particular:<p>In the run length encoding example, I don’t understand how the runtime data structure is defined. There is a Runlength data type, but its definition looks more like a Haskell-style curried function definition than a data definition. It seems to call the ‘rep’ function and the list concatenation operator, but how do you get a datatype out of that? If you drew a boxes and arrows diagram showing how the data is stored, what would it look like?<p>I’m wondering if this is like how you can use a closure to store data in captured local variables? Or perhaps like lazy evaluation in Haskell?