suhailshergill

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

suhailshergill

#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

suhailshergill

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)
 *
 */

suhailshergill

#! /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

suhailshergill

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

import scala.language.higherKinds

trait Monad[M[_]] {
  implicit def `Monad ~> Functor`[M[_]: Monad]: Functor[M] = new Functor[M]{}
}

trait Functor[F[_]] {
}
object Functor {

suhailshergill

(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

{-# 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

#!/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