Rutvik Patel heyrutvik

A graph-based core for a dependently typed language

Abstract

An overly-ambitious attempt to re-think the core calculus of dependent type theory by basing it on graphs as opposed to lambdas, Π-types, Σ-types, etc. The hope is that this might allow us to investigate dependency more closely, and allow us to refine programs to target different environments in an easier way than with traditional programming representations.

Introduction

The Pledge

One thing that always made me a little sad about transducers was how map lost its ability to iterate multiple collections in parallel. This is actually my favorite feature of map. For example:

(map + (range 5) (range 5 10))
=> (5 7 9 11 13)

One somewhat practical use of this is if you want to compare two sequences, pairwise, using a comparator. Though I wish that every? took multiple collections, this is an adequate substitute:

I try to write code that is "maximally polymorphic" to the extent that I am sufficiently familiar with the concepts involved and that I am confident of being able to efficiently explain my code to co-workers if needed.

I started to use generics in Java to improve reuse of the libraries I wrote at work, but as I was growing a better understanding of types, parametricity and theorems for free, other compelling reasons became prominent:

the free theorems help me reason about code: given parametricity, I know what a function can do and cannot do, based only on its type signature. Eg. given an unconstrained type variable, any value of this type that appears in positive position (output)

Applied Functional Programming with Scala - Notes

1. Mastering Functions

A function is a mapping from one set, called a domain, to another set, called the codomain. A function associates every element in the domain with exactly one element in the codomain. In Scala, both domain and codomain are types.

val square : Int => Int = x => x * x

Explaining Miles's Magic

Miles Sabin recently opened a pull request fixing the infamous SI-2712. First off, this is remarkable and, if merged, will make everyone's life enormously easier. This is a bug that a lot of people hit often without even realizing it, and they just assume that either they did something wrong or the compiler is broken in some weird way. It is especially common for users of scalaz or cats.

But that's not what I wanted to write about. What I want to write about is the exact semantics of Miles's fix, because it does impose some very specific assumptions about the way that type constructors work, and understanding those assumptions is the key to getting the most of it his fix.

For starters, here is the sort of thing that SI-2712 affects:

def foo[F[_], A](fa: F[A]): String = fa.toString

Atom Clojure Setup

This describes how I setup Atom for an ideal Clojure development workflow. This fixes indentation on newlines, handles parentheses, etc. The keybinding settings for enter (in keymap.cson) are important to get proper newlines with indentation at the right level. There are other helpers in init.coffee and keymap.cson that are useful for cutting, copying, pasting, deleting, and indenting Lisp expressions.

Install Atom

Download Atom

The Atom documentation is excellent. It's highly worth reading the flight manual.


	object LambdaCalculus {
	sealed trait Type
	case class Arrow[S <: Type, T <: Type]() extends Type
	case class Base() extends Type

	sealed trait Ctx
	case class Nil() extends Ctx
	case class Cons[X <: Type, XS <: Ctx]() extends Ctx

	(* Inlining for the λ-calculus, implemented in tagless final style. This seems
	* like it _must_ be related to Normalization By Evaluation (see eg [1,2]),
	* since they both amount to β-reduction (plus η-expansion in extensional NBE),
	* and the techniques have a similar "flavor", but I don't immediately see a
	* formal connection.
	*
	* [1] https://gist.github.com/rntz/f2f15f6cb4b8690c3599119225a57d33
	* [2] http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
	*)

	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE TupleSections #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE TypeInType #-}
	{-# LANGUAGE GADTs #-}
	module Data.Optics where


	class Profunctor p where

	-- A port of: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html

	{-# LANGUAGE DeriveFunctor #-}

	module ABT where

	import qualified Data.Foldable as Foldable
	import Data.Foldable (Foldable)
	import Data.Set (Set)
	import qualified Data.Set as Set