Skip to content

Instantly share code, notes, and snippets.

@suhailshergill
suhailshergill / update-emacs-ppa.sh
Created June 29, 2012 14:51 — forked from DamienCassou/update-emacs-ppa.sh
Emacs-snapshot build script for Ubuntu PPA
#!/bin/bash
# Author: Damien Cassou
#
# This is the script I use to build https://launchpad.net/~cassou/+archive/emacs/
# from http://emacs.naquadah.org/.
MAIN_VERSION=20120410
SUB_VERSION=1
@suhailshergill
suhailshergill / reverse-proxy.hs
Created August 5, 2012 16:27 — forked from snoyberg/reverse-proxy.hs
A minimalist reverse HTTP proxy using conduit
{-# LANGUAGE OverloadedStrings #-}
import Data.Conduit
import Data.Conduit.List (peek)
import Data.Conduit.Network
import qualified Data.ByteString.Char8 as S8
import Data.Char (toLower, isSpace)
import Network (withSocketsDo)
import Control.Monad.IO.Class
import Control.Concurrent (forkIO)
import Network.Wai
@suhailshergill
suhailshergill / gist:3467113
Created August 25, 2012 15:27 — forked from nicferrier/gist:3466870
converting a bson datetime to an elisp time
(defun bson-datetime-int64-to-time (byte-list)
(let ((calc-num
(concat
"16#"
(mapconcat
(lambda (x) (format "%02X" x))
byte-list ""))))
(list
(calc-eval
"rsh(and(idiv($,1000),16#ffff0000),16)"
@suhailshergill
suhailshergill / MonadImpliesFunctor.scala
Created April 16, 2014 17:04 — forked from jdegoes/MonadImpliesFunctor.scala
scala: monad implies functor
import scala.language.higherKinds
trait Monad[M[_]] {
implicit def `Monad ~> Functor`[M[_]: Monad]: Functor[M] = new Functor[M]{}
}
trait Functor[F[_]] {
}
object Functor {
@suhailshergill
suhailshergill / Deserialization.scala
Last active February 24, 2019 16:08 — forked from ramn/Deserialization.scala
scala: java.io.Serialization
import java.io._
@SerialVersionUID(15L)
class Animal(name: String, age: Int) extends Serializable {
override def toString = s"Animal($name, $age)"
}
case class Person(name: String)
// or fork := true in sbt
@suhailshergill
suhailshergill / emailme.py
Last active February 24, 2019 16:06 — forked from alexalemi/emailme.py
#! /usr/bin/env python
""" Email Me.
Usage:
emailme <message>
emailme [-s] <message>
emailme [-s] <subject> <message>
emailme <toaddr> <subject> <message>
emailme <toaddr> <fromaddr> <subject> <message>
emailme -h | --help
import org.apache.spark.SparkContext
import org.apache.spark.rdd.RDD
/**
* I am trying to narrow down on an Exception thrown by Spark when using "Factories".
* The factories have parameters that are used in the classes' functions.
*
* To run this code: copy-paste this whole content in a Spark-Shell. Execute Test.theMain(sc)
*
*/
#Copyright (c) 2010-2013 Samuel Sutch [samuel.sutch@gmail.com]
#
#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

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

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

Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.