tel

Per Martin-Löf’s (OMLCJLL)

“On the Meanings of the Logical Constants and the Justifications of the Logical Laws”

Intro

I know I tried to write up the Meetup announcement to draw people here with a computer science or programming background. And then I threw at you this dense philosophical paper which assumes you’re familiar with names like Gentzen and languages like German and Greek not Javascript or C#.

So, that was pretty unfair of me, I apologize. In order to amend

tel

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

tel

/* eslint-disable new-cap */

/**
 * Lens types.
 * ===========
 *
 * a * b = {fst: a, snd: b}
 * a + b = {index: Boolean, value: a | b}
 *
 * Iso   s t a b = forall (~>) . Profunctor (~>) => (a ~> b) -> (s ~> t)

tel

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
 

tel

module Sum = struct
  type (+'a, +'b) sum = Inl of 'a | Inr of 'b
  type (+'a, +'b) t = ('a, 'b) sum

  let bimap f g = function
    | Inl a -> Inl (f a)
    | Inr b -> Inr (g b)

  let lmap f = bimap f (fun x -> x)
  let rmap f = bimap (fun x -> x) f

tel

Indentation sensitive parser combinators

An indentation sensitive parser combinator language is one that helps you express ideas like "this parse only succeeds if it's within the current indentation block". The concept is somewhat small and elegant and is implemented in a few libraries. In this writeup, I will use examples from indents.

Background and goal

The direct goal will be to write the sameOrIndented parser combinator with a type

tel

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module ParserCombinators where

{-

We'll build a set of parser combinators from scratch demonstrating how
they arise as a monad transformer stack. Actually, how they arise as a
choice between two different monad transformer stacks!

tel

import scala.language.higherKinds
import scala.language.implicitConversions

trait Pt[C[_[_, _]], S, T, A, B] {
  def apply[~>[_, _]](ex: C[~>])(p: A ~> B): S ~> T
}

trait Profunctor[~>[_, _]] {
  def dimap[X, Y, A, B](f: X => A, g: B => Y)(p: A ~> B): X ~> Y

tel

package jspha.comms

import scala.language.higherKinds

sealed trait Quantity {
  type T[_]
}

object Singular extends Quantity { self =>
  case class T[A](v: A) extends Quantity.Set[A] {

tel

package com.jspha.maia

import scala.language.higherKinds
import shapeless._
import shapeless.ops.hlist.Mapped

trait Maia {

  trait Api {
    type Fields <: HList