Verity Scheel MonoidMusician

Nick Scheel
what's the weakest type theory we can define arbitrary finite aleph numbers in? (arbitrary finite beth numbers are easy – just need natural numbers and functions)

Reed Mullanix
Be warned, the cardinals are not very well behaved in constructive math
Pretty much every direction you look, weird stuff starts to happen

Nick Scheel
yeah 🙂
I just find it weird that, with choice, all cardinals are aleph numbers, but beth numbers are the ones that are easy to construct in type theory

My research ideas

Implement a better typechecker for Dhall. Hopefully still straightforward to implement and with good errors.

I think it will essentially be a reification of the typechecker into data structures such that data still only flows one way, but acts like it flows both ways via substitution. Very tricky.

If I get it implemented, then I can look at performance.

Threads

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.

	# Syntax for a metalanguage for writing programming language standards/specifications with an eye towards codegen

	# The data format is very simple: data is either a string or a tuple of data.
	# The idea is that we'll impose some simple types on top of this:
	# Obviously strings, and arrays, possibly associative lists, and then mixed ADTs/enums, which are either plain strings or arrays where the first item is the tag denoting the constructor.
	# I don't have the types figured out yet.

	# Variable names
	variable-name = [_A-Za-z][-_A-Za-z0-9]*
	# A variable can have periods, but they don't mean anything

	module Main where

	import Prelude

	import Effect (Effect)
	import Effect.Aff (Aff)
	import Data.Maybe (Maybe(..))
	import Halogen as H
	import Halogen.Aff as HA
	import Halogen.HTML as HH

	module Main where

	import Prelude

	import Effect (Effect)
	import Effect.Aff (Aff)
	import Data.Maybe (Maybe(..))
	import Halogen as H
	import Halogen.Aff as HA
	import Halogen.HTML as HH

	module TestKindMatch where

	import Prelude
	import Data.Maybe (Maybe)

	class Functor1 :: ((Type -> Type) -> Type) -> Constraint
	class Functor1 t where
	map1 :: forall f g. (f ~> g) -> t f -> t g

	data Proxy :: forall k. k -> Type

	<html>
	<head>
	<meta charset="utf-8"/>
	<meta name="viewport" content="width=device-width, initial-scale=1.0">
	<title>Control my mac</title>
	<style>
	/* From https://css-tricks.com/styling-cross-browser-compatible-range-inputs-css/ */
	input[type=range] {
	-webkit-appearance: none;
	margin: 10px 0;

	#!/usr/bin/env python3

	import sys
	import os
	import mmap

	filename = sys.argv[1]

	tag = b"RIFF"