Introduction

Last year, I learned of the Idris language and wrote a blog post after reading a book on it. Coincidentally, I joined a company that worked on blockchain technology almost immediately after publishing that post. So when I came across a paper titled “Safer smart contracts through type-driven development: Using dependent and polymorphic types for safer development of smart contracts”, which combined two topics of my interest, I just had to read it.

This post is a collection of the thoughts that came across my mind while I was reading the paper. There won’t be any new idea that builds on the contents of the paper. I assume basic understanding of functional programming paradigm, in particular the distinction between pure functions and side effects.

Summary

Once we get through the introduction to Elm, we start to encounter some odd-looking operators in Elm codes. I’m talking about the ones like >>, <<, |>, and <|, which modify how functions are composed and applied. I will give more details about how and when I use them in this post, but here’s my rule of thumb:

1. Use |> and <| to visually describe the flow of data. It’s their main advantage over nested parantheses, which provide equivalent functionalities.

2. Use >> and << to describe function compositions independent of the data flow. In practice, I usually define a new function through composition and use it with |> and <|.

3. Use either the pair of |> and >> or <| and << without mixing them. The shapes of these operators hold inherent directional meanings, so mixing different directions taxes our cognitive resources.

Preface

This interview with Rich Hickey, the creator of Clojure language, was conducted by Michael Fogus on CodeQuarterly. All credit should be given to him. I’m posting it here for two reasons:

1. Preservation

CodeQuarterly is gone, so I wanted to create another copy of this interesting and insightful interview to preserve it.

2. Original Text for Korean Translation

I wanted to provide the original English text for readers of my Korean translation in case they wanted to reference the primary source.

Summary

Type-Driven Development with Idris introduces a software development approach that uses types as the primary tool for building softwares. In this paradigm, types are given much more responsibilities than their traditional role of checking data validity. For example, types can be used to represent the input and output states of functions or various contracts that functions and datas must fulfill. Such descriptions and contracts are enforced at compile time, providing much stronger guarantee of software correctness at compile time than other approaches can.

Idris programming language is used in the book to teach type-driven development (TDD). Idris is a general purpose pure functional programming language created by Edwin Brady, who is also the author of this book. Idris is inspired by Haskell and ML and sports a state of the art type system suited for TDD. You will learn basics of Idris language alongside TDD in this book.

Summary

How to Bake Pi: an Edible Exploration of the Mathematics of Mathematics explores what mathematics is about by explaining the purpose and building blocks of mathematics in an easy-to-read language, drawing examples from everyday life, including baking.

I recommend it to you if you have never learned abstract mathematics but would like an introduction to it written in a way that even normal human beings can understand.

I do not recommend this book if you want to learn category theory or its application to software development. This book will give you an overview of what category theory is about, but will not teach you anything in depth about category theory. In terms of category theory textbook, the contents of this book would fit in as an extended introduction chapter.

Summary

If you are a software developer without formal computer science background who want a friendly introduction to computer science, I highly recommend this book.

This book explores some of core concepts of computer science, specifically syntax and semantics of programming languages and basic abstract machines that can execute programs. The author writes in a concise, easy-to-read, and lighthearted style, providing codes that you would write at your daily job as examples. It’s much easier to read than a typical academic writing that’s full of bizarre mathematical symbols.

Overview

I wanted to build an Elixir application that can run Elixir code provided by users and return the results. Maintaining security is critical for an application like this, since I could be running some evil codes written by diabolical mastermind residing in the scary trench of Internet. I’ve never done something like this before, so I had to research extensively for a good solution.

Unfortunately there does not seem to be a perfect solution, as always. After considering tradeoffs, I chose to settle for Docker container with some security options. I think it’s a reasonably secure and reasonably performant option for my use case. This blog post is a journal of what I’ve learned while building the application.

I am by no means an expert in this matter, so read this as not as a survey of technology but as a personal journal. I do welcome correction and additional resources to better my understanding. And if you want an overview of sandboxing technology landscape, I recommend Sandboxing landscape by Marek (@majek04). It’s a broad, up-to-date, and also well-written article as much as I can tell.

This post assumes understanding of how GenServer.cast/2 and GenServer.call/2 work.

TL;DR

Call a GenServer.call/2 function after GenServer.cast/2. This prevents your caller process from executing any more code until it receives a reply to the call/2 function from the receiver process. The receiver process handles and sends the reply to call/2 only after it has handled the message from cast/2. This can ensure sequential execution of code. If you need a generic function, :sys.get_state/1 can be used for this purpose.

Nowadays many features of Haskell can be found in other languages, too. But such features often feel like an awkward addition to languages that are designed for different goals in mind. In contrast, functional programming elements are given the highest accommodation in Haskell. I think this is what makes Haskell special - it is purely dedicated to functional programming. So even though Haskell and other languages might be providing theoretically identical features, the experience of using them is so vastly different. I think I could learn the following lessons because of this special atmosphere that Haskell has.

The Scary, Scary Land of Haskell

I think few other programming languages evoked as much trepidation in me as did Haskell. After all, it is a language known for being arcane and unusual. Still, everyone said that learning Haskell would dramatically broaden my understanding of programming, so I’ve been eyeing for an opportunity to venture into the land of Haskell for a while.