Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
[RC Diary] Idris (-29)

[RC Diary] Idris (-29)

Spacemacs integration

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

good

The theory

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:

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment