So I've added the Idris layer into my Spacemacs config and everything is working perfectly, aaaah. Colors are ok, indentation
too, and the REPL works as expected, the only thing that got me thinking was the (Not loaded) message under the buffer in
which I have Idris code, but now it makes perfect sense, it says that when you have changes that haven't been loaded in
the REPL, I just need to ,r to load it
I wasn't really getting the purpose behind the function, so :doc the to the rescue:
Prelude.Basics.the : (a : Type) -> (value : a) -> a
Manually assign a type to an expression.
Arguments:
a : Type -- the type to assign
value : a -- the element to get the type
The function is Total
A Total function is one that "is defined for all possible inputs and is guaranteed to terminate".
Going through Type Driven Development with Idris one shocking thing I've discovered is that the compiler and the type checker are two different things, the first runs before the second.
At some point the author is talking about Functors, so I had a look around to find some information about those, and
basically I asked for troubles:
I will leave these concepts for a later moment, as of now I feel like I don't have enough mental power / experience to grasp them, hopefully the concepts will grow in my mind while reading through the chapters.