Suhail Shergill suhailshergill

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.,

Mo kobrosli 1:41 PM

Sent from Toronto Apache Spark

Hi Suhail. Sorry. Yesterday was nuts. Answers below! Didn't fit inline on the comments. over the max :( Didn't feel like breaking it all up.

	#Copyright (c) 2010-2013 Samuel Sutch [[email protected]]
	#
	#Permission is hereby granted, free of charge, to any person obtaining a copy
	#of this software and associated documentation files (the "Software"), to deal
	#in the Software without restriction, including without limitation the rights
	#to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
	#copies of the Software, and to permit persons to whom the Software is
	#furnished to do so, subject to the following conditions:
	#
	#The above copyright notice and this permission notice shall be included in

	object RDDasMonadPlus {
	import org.apache.spark.{ SparkContext }
	import org.apache.spark.rdd.RDD
	import scalaz._
	import Scalaz._
	import scala.reflect.ClassTag

	// RDDMPlus is the type for which we will define the Monad instance. it can be
	// constructed from an RDD using the RDDClassTag constructor. this
	// implementation is based on insights from

	(define (take-sample)
	(rejection-query

	(define A (if (flip) 1 0))
	(define B (if (flip) 1 0))
	(define C (if (flip) 1 0))
	(define D (+ A B C))

	A

	;; by conditioning on A, note that we could also condition on B first if desired
	(define (ab)
	(define a (flip 0.8))
	(define b (if a (flip 0.5) (flip 0.3)))
	(list a b)
	)
	(hist (repeat 1000 ab) "joint AB by conditioning on A")

	;; alternative solution
	(define (joint-ab)

	[ 5 of 25] Compiling Control.Eff1 ( src/Control/Eff1.hs, dist/build/Control/Eff1.o )

	src/Control/Eff1.hs:492:10:
	Could not deduce (Data.OpenUnion51.FindElem Choose r)
	arising from the superclasses of an instance declaration
	from the context (Member NdetEff r)
	bound by the instance declaration at src/Control/Eff1.hs:492:10-46
	In the instance declaration for ‘MonadPlus (Eff r)’

	src/Control/Eff1.hs:527:34:

	(dolist (pkg '(s))
	(message "%s" pkg) ;; this will print "s"
	(eval `(use-package ,pkg)))

	#!/bin/bash
	export GDK_NATIVE_WINDOWS=1
	exec emacsclient --alternate-editor="" -s ~/.emacs.d/server/socket -c "$@"

Suhail Shergill suhailshergill

Simpler, Easier!

First, the untyped lambda calculus.

Sessions/Users