# in Code

## Justin Le

Welcome! My name is Justin Le. I’m a PhD student at Chapman University in California, studying Computational Science & Applied Maths; I studied Physics and Computer Science at University of California, San Diego :)

This is just my weblog covering my various adventures in programming and explorations in the vast worlds of computation, physics, engineering, mathematics, and knowledge. Expect a healthy curiosity and an only slightly unhealthy obsession for finding new ways to marvel, wonder, and create. Join me if you wish!

Check out my most popular articles: Inside My World (Ode to Functor and Monad) and “IO Monad” Considered Harmful!

## Recent Entries

• ### Advent of Code 2017! Ongoing solutions and explanations

Just a short post to share that I started a github repository of my Advent of Code 2017 Solutions, as I write them!

I also am including my reflections and explanations on my solutions, explaining my thought processes and how the solutions work.

Yes I definitely spent a bit too much time writing the executable, which is an automated (cached) downloader, test suite runner (on sample inputs), and benchmark suite.

I originally was only going to casually try the problems (like I did last year), but I hit a decent global rank by accident on Day 4 (which was very suited for Haskell!), and since then I’ve been taking things seriously to try to aim for the global leaderboard (top 100). This is a struggle for me because I’m not really the fastest algorithm person, but I think it’s a fun goal for me to try to hit this year.

Wish me luck! And if you haven’t started yet, it’s not too late to join in the fun! glguy has been maintaining the semi-official Haskell Leaderboard (join code 43100-84040706) – come join us!

• ### Hamiltonian Dynamics in Haskell

As promised in my hamilton introduction post (published almost exactly one year ago!), I’m going to go over implementing of the hamilton library using

1. DataKinds (with TypeLits) to enforce sizes of vectors and matrices and help guide us write our code
2. Statically-sized linear algebra with hmatrix
4. Statically-sized vectors with vector-sized

This post will be a bit heavy in some mathematics and Haskell concepts. The expected audience is intermediate Haskell programmers. Note that this is not a post on dependent types, because dependent types (types that depend on runtime values) are not explicitly used.

The mathematics and physics are “extra” flavor text and could potentially be skipped, but you’ll get the most out of this article if you have basic familiarity with:

1. Basic concepts of multivariable calculus (like partial and total derivatives).
2. Concepts of linear algebra (like dot products, matrix multiplication, and matrix inverses)

No physics knowledge is assumed, but knowing a little bit of first semester physics would help you gain a bit more of an appreciation for the end result!

• ### Fixed-Length Vector Types in Haskell (an Update for 2017)

This post is a follow-up to my fixed-length vectors in haskell in 2015 post! When I was writing the post originally, I was new to the whole type-level game in Haskell; I didn’t know what I was talking about, and that post was a way for me to push myself to learn more. Immediately after it was posted, of course, people taught me where I went wrong in the idioms I explained, and better and more idiomatic ways to do things. And that’s great! Learning is awesome!

Unfortunately, however, to my horror, I began noticing people referring to the post in a canonical/authoritative way…so the post became an immediate source of guilt to me. I tried correcting things with my practical dependent types in haskell series the next year. But I still saw my 2015 post being used as a reference even after that post, so I figured that writing a direct replacement/follow-up as the only way I would ever fix this!

So here we are in 2017. GHC 8.2 is here, and base is in version 4.10. What’s the “right” way to do fixed-length vectors in Haskell?

This post doesn’t attempt to present anything groundbreaking or new, but is meant to be a sort of reference/introduction to fixed-length vectors in Haskell, as of GHC 8.2 and the 2017 Haskell ecosystem.

We’ll be looking at two methods here: The first one we will be looking at is a performant fixed-length vector that you will probably be using for any code that requires a fixed-length container — especially for tight numeric code and situations where performance matters. We’ll see how to implement them using the universal native KnownNat mechanisms, and also how we can implement them using singletons to help us make things a bit smoother and more well-integrated. For most people, this is all they actually need. (I claim the canonical haskell ecosystem source to be the vector-sized library)

The second method is a structural fixed-length inductive vector. It’s…actually more like a fixed-length (lazily linked) list than a vector. The length of the list is enforced by the very structure of the data type. This type is more useful as a streaming data type, and also in situations where you want take advantage of the structural characteristics of lengths in the context of a dependently typed program. (I claim the canonical haskell ecosystem source to be the type-combinators library)

One of the most common gripes people have when learning Haskell is the fact that typeclass “laws” are only laws by convention, and aren’t enforced by the language and compiler. When asked why, the typical response is “Haskell can’t do that”, followed by a well-intentioned redirection to quickcheck or some other fuzzing library.

But, to any experienced Haskeller, “Haskell’s type system can’t express X” is always interpreted as a (personal) challenge.

GHC Haskell’s type system has been advanced enough to provide verified typeclasses for a long time, since the introduction of data kinds and associated types. And with the singletons library, it’s now as easy as ever.

(The code for this post is available here if you want to follow along! Some of the examples here involving Demote and relying on its injectivity will only work with singletons HEAD, even though the necessary patches were made seven months ago1)

1. Not sure why it’s not on hackage yet, but I will update when it gets there!

• ### Introducing the Hamilton library

Hamilton: README / hackage / github

The hamilton library is on hackage! It was mostly a proof-of-concept toy experiment to simulate motion on bezier curves, but it became usable enough and accurate enough (to my surprise, admittedly) that I finished up some final touches to make it complete and put it on hackage as a general-purpose physics simulator.

The library is, in short, a way to simulate a physical system by stating nothing more than an arbitrary parameterization of a system (a “generalized coordinate”) and a potential energy function.

I was going to write a Haskell post on the implementation, which was what interested me at first. I wanted to go over –

1. Using automatic differentiation to automatically compute momentum and the hamilton equations, which are solutions of differential equations.

2. Using type-indexed vectors and dependent types in a seamless way to encode the dimensionality of the generalized coordinate systems and to encode invariants the types of functions.

• ### Practical Dependent Types in Haskell 2: Existential Neural Networks and Types at Runtime

We’re back to continue on our journey in using dependent types to write type-safe neural networks! In Part 1, we wrote things out in normal, untyped Haskell, and looked at red flags and general design principles that nudged us in the direction of adding dependent types to our program. We learned to appreciate what dependent types offered in terms of guiding us in writing our code, helping the compiler check our correctness, providing a better interface for users, and more.

We also learned how to use singletons to work around some of Haskell’s fundamental limitations to let us “pattern match” on the structure of types, and how to use typeclasses to generate singletons reflecting the structure of types we are dealing with.

(If you read Part 1 before the singletons section was re-written to use the singletons library, here’s a link to the section in specific. This tutorial will assume familiarity with what is discussed there!)

All of what we’ve dealt with so far has essentially been with types that are fixed at compile-time. All the networks we’ve made have had “static” types, with their sizes in their types indicated directly in the source code. In this post, we’re going to dive into the world of types that depend on factors unknown until runtime, and see how dependent types in a strongly typed language like Haskell helps us write safer, more correct, and more maintainable code.

This post was written for GHC 8 on stackage snapshot nightly-2016-06-28, but should work with GHC 7.10 for the most part. All of the set-up instructions and caveats (like the singletons-2.0.1 bug affecting GHC 7.10 users and the unreleased hmatrix version) are the same as for part 1’s setup.

All of the code in this post is downloadable as a standalone source file so you can follow along!

• ### Practical Dependent Types in Haskell: Type-Safe Neural Networks (Part 1)

It seems these days like programming with dependent types in Haskell (and its advantages) is moving slowly but steadily to the mainstream of Haskell programming. In the current state of Haskell education, dependent types are often considered topics for “advanced” Haskell users. However, I can foresee a day where the ease of use of modern Haskell libraries relying on dependent types forces programming with dependent types to be an integral part of normal intermediate (or even beginner) Haskell education.

The first project in this series will build up to a type-safe artificial neural network implementation with back-propagation training.

• ### Automatic Propagation of Uncertainty with AD

This post and series is a walk-through of the implementation of my uncertain library, now on hackage!

Some of my favorite Haskell “tricks” involve working with exotic numeric types with custom “overloaded” numeric functions and literals that let us work with data in surprisingly elegant and expressive ways.

Here is one example — from my work in experimental physics and statistics, we often deal with experimental/sampled values with inherent uncertainty. If you ever measure something to be $12.3\,\mathrm{cm}$, that doesn’t mean it’s $12.300000\,\mathrm{cm}$ — it means that it’s somewhere between $12.2\,\mathrm{cm}$ and $12.4\,\mathrm{cm}$…and we don’t know exactly. We can write it as $12.3 \pm 0.1\,\mathrm{cm}$. The interesting thing happens when we try to add, multiply, divide numbers with uncertainty. What happens when you “add” $12 \pm 3$ and $19 \pm 6$?

The initial guess might be $31 \pm 9$, because one is $\pm 3$ and the other is $\pm 6$. But! If you actually do experiments like this several times, you’ll see that this isn’t the case. If you tried this out experimentally and simulate several hundred trials, you’ll see that the answer is actually something like $31 \pm 7$. (We’ll explain why later, but feel free to stop reading this article now and try this out yourself!1)

Let’s write ourselves a Haskell data type that lets us work with “numbers with inherent uncertainty”:

ghci> let x = 14.6 +/- 0.8
ghci> let y = 31   +/- 2
ghci> x + y
46 +/- 2
ghci> x * y
450 +/- 40
ghci> sqrt (x + y)
6.8 +/- 0.2
ghci> logBase y x
0.78 +/- 0.02
ghci> log (x**y)
85.9 +/- 0.3

1. You can simulate noisy data by using uniform noise distributions, Gaussian distributions, or however manner you like that has a given expected value (mean) and “spread”. Verify by checking the standard deviation of the sums!