Inklings: a tumblelog

I must admit, I don’t fully grasp Agda as a language, nor do I quite grasp dependent types, but it does seem interesting, and it seems as if it might be more straightforward conceptually when it clicks with me than Haskell’s type system was.