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 [[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

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

from itertools import imap                                                                                                       
def foo(x): return iter(x) # function which returns an iter                                                                      
bar = ["bar", "baz"]                                                                                                             
list(foo("bar"))                                                                                                                 
#[Out]# ['b', 'a', 'r']                                                                                                          
baz = iter(bar) # iterator of inputs                                                                                             
qu = (item for sublist in imap(foo, baz) for item in sublist)                                                                    
list(qu) # demonstration of chaining things together                                                              

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

-- The illustration of the Boehm-Berarducci encoding

-- This file is the baseline: using ordinary algebraic
-- data type and operations of constructions, deconstructions
-- and transformation.
-- We use the running example of the Exp data type from
-- tagless-final lectures

module BB_ADT where

suhailshergill

object TTFI {

  object Initial {
    // {{{ OOP

    object OOP {
      // extending language is easy, adding more functions is hard since it
      // involves having to modify each case class
      trait Exp[A] {
        def eval: A

suhailshergill

(defun su/monkeypatch/nil-fun (&rest args))
(defvar su/monkeypatch/nil-var nil)

(defun su/monkeypatch/mangle-name (symbol prefix)
  (concat "su/monkeypatches/" prefix (symbol-name symbol))
  )
(defun su/monkeypatch/copy-values (source-symbol dest-symbol)
  "This function copies values from source to dest. It does not keep any
  backups. I f you want that you want to use 'su/monkeypatch' instead"
  (ignore-errors

suhailshergill

-- [[file:~/Dropbox/Public/papers/pl/haskell/free/free-applicative-functors_capriotti-kaposi.org::*%5B%5Bhttp://hackage.haskell.org/package/free-4.7.1/docs/Control-Monad-Free.html%5D%5BFree%20monad%5D%5D][su/haskell/free/FreeAL/modulo]]

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS -fno-warn-orphans #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}