matthew mcdonald mafm

Simpler, Easier!

Lennart Augustsson, Oct 25, 2007

In a recent paper, Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus), the authors argue that type checking a dependently typed language is easy. I agree whole-heartedly, it doesn't have to be difficult at all. But I don't think the paper presents the easiest way to do it. So here is my take on how to write a simple dependent type checker. (There's nothing new here, and the authors of the paper are undoubtedly familiar with all of it.)

First, the untyped lambda calculus.

I'll start by implementing the untyped lambda calculus. It's a very simple language with just three constructs: variables, applications, and lambda expressions, i.e.,

Cross Entropy Method

How do we solve for the policy optimization problem which is to maximize the total reward given some parametrized policy?

Discounted future reward

To begin with, for an episode the total reward is the sum of all the rewards. If our environment is stochastic, we can never be sure if we will get the same rewards the next time we perform the same actions. Thus the more we go into the future the more the total future reward may diverge. So for that reason it is common to use the discounted future reward where the parameter discount is called the discount factor and is between 0 and 1.

A good strategy for an agent would be to always choose an action that maximizes the (discounted) future reward. In other words we want to maximize the expected reward per episode.

	// This is a quick demonstration of "function inheritance" as described in
	// this paper from Daniel Brown and William Cook.
	// http://www.cs.utexas.edu/users/wcook/Drafts/2009/sblp09-memo-mixins.pdf
	// Expressed in TypeScript (and without the monads).

	// Syntax note: When you write function types in TypeScript, you need to name
	// each parameter. But the names don't actually matter, so I just use _. You
	// can read `(_:A) => B` as `a -> b` in ML or Haskell syntax.

	// In Brown and Cook's Haskell, `type Gen a = a -> a` is a "generator." The