Verity Scheel MonoidMusician

Commentary on Parametricity

copied from Slack thread, let me know if you have questions!

Background on parametricity

This was mostly based on Reynold’s original paper on parametricity, if I recall correctly …

In most proof assistants, you can’t prove that all functions are parametric, even if you can’t intuitionistically write a function that violates it (in particular, in the absence of LEM).

So you can’t prove that the type ∀ A → (A → (A → A) → A) is equivalent to the natural numbers, you actually have to define a sigma type of functions that are parametric (and you also have to quotient this by proofs of parametricity, I think), and then you can obtain your result.

The problem

Information is lost when going from concrete syntax to AST, and information also gets lost when doing operations on that AST.

So I have a novel approach to compiler source spans that’s been on my mind for years. I haven’t exactly implemented it, though code for it does appear in my mess of dhall-purescript, which is my project to create an interactive structural editor plus dhall implementation. But it isn’t exactly integrated into producing useful output yet.

Anyways.

The Solution

My opinion on compiler source spans is that:

Every AST node should be associated with at least one source span.

MonoidMusicianʼs Type Theory Musings

Welcome to my (un)scrambled thoughts on all things from the intersection of homotopy type theory, functional programming, and set theory! Thereʼs going to be a lot of terminology being thrown around, but donʼt be intimidated: hopefully Iʼll either describe the term, link to a definition/explanation, or youʼll be able to figure it out from context (or just skip it!). I do believe the best way to be clear is to be precise with language and to use established terminology, but because I am synthesizing pretty disparate areas of knowledge, most people wonʼt know all the terms.

My goal with these are to raise some new perspectives on common themes, and cross-pollinate these fields with each other.

	#!/usr/bin/env python3

	import sys
	import os
	import mmap

	filename = sys.argv[1]

	tag = b"RIFF"

	{-# OPTIONS --cubical --safe #-}
	module Cubical.Parametricity where

	open import Cubical.Core.Everything

	open import Cubical.Foundations.Prelude
	open import Cubical.Data.Sigma.Properties
	open import Cubical.Foundations.Everything
	open import Cubical.Data.Everything hiding (Iso ; compIso)

	module Test.AppendOverlap where

	import Data.Semigroup (class Semigroup, (<>))
	import Data.Tuple (Tuple(..))
	import Prim.Row (class Nub, class Union)
	import Record (union)
	import Unsafe.Coerce (unsafeCoerce)

	unsafeSplit ::
	forall left right nubbed.

	import algebra.module

	open list

	-- The binomial coefficient, defined recursively on the natural numbers
	def B : ℕ → ℕ → ℕ
	\| _ 0 := 1
	\| 0 _ := 0
	\| (n+1) (k+1) := B n (k+1) + B n k

	-- This work by Nick Scheel is licensed under CC0 1.0
	-- https://creativecommons.org/publicdomain/zero/1.0/

	-- A basic framework for graph theory on multidigraphs in Lean
	-- and a proof that no_watershed_condition is sufficient to
	-- establish that a graph has a unique sink for each vertex
	--
	-- I hope to give some introduction to the syntax of how Lean works here,
	-- but I assume some familiarity with functions, pattern matching,
	-- type theory, and proofs.

	module LeibnizGADT where

	import Prelude

	import Control.Monad.Eff.Exception.Unsafe (unsafeThrow)
	import Data.Leibniz (type (~), coerce, coerceSymm, liftLeibniz, liftLeibniz1of2, liftLeibniz2of2, lowerLeibniz1of2, lowerLeibniz2of2, symm)
	import Data.Tuple (Tuple(..))

	-- Solution to https://www.reddit.com/r/purescript/comments/4x1jq3/approximating_gadts_in_purescript/d6bzlez/
	data T a

	-- \| A change for a single key is an addition, removal, or update.
	data MapChange v dv
	= Add v
	\| Remove
	\| Update dv

	-- \| A change for each possible key.
	newtype MapChanges k v dv = MapChanges (Map k (MapChange v dv))

	prune :: forall k v. Array (Tuple k (Maybe v)) -> Array (Tuple k v)