Orestis Melkonian omelkonian

Lightweight region memory management in a two-stage language

Intro
Basics
- Stage inference
Regions
- Bit-stealing
- Using regions
Eager regions

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

	module GenerateYourNeighbors
	open FsCheck

	type BST<'a> =
	\| Empty
	\| Node of BST<'a> * 'a * BST<'a>

	[<StructuralEquality;StructuralComparison>]
	type Extended<'a when 'a: comparison> =
	\| NegInfty

	{-
	Weak excluded middle states that for every propostiion P, either ¬¬P or ¬P holds.

	We give a proof of weak excluded middle, relying just on basic facts about real numbers,
	which we carefully state, in order to make the dependence on them transparent.

	Some people might doubt the formalization. To convince yourself that there is no cheating, you should:

	* Carefully read the facts listed in the RealFacts below to see that these are all
	just familiar facts about the real numbers.


	{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

	{-
	Challenge:
	- Define a deeply embedded faithfully represented syntax of a dependently typed
	TT in Agda.
	- Use an Agda fragment which has canonicity. This means that the combination of
	indexed inductive types & cubical equality is not allowed!
	- Prove consistency.

	(* A relatively straightforward formalization of HA^2 *)

	Require Import Coq.Lists.List.
	Require Import Coq.Strings.String.

	Inductive tm :=
	\| v(name : string)
	\| Succ(a : tm)
	\| Z
	\| Plus(a b : tm)

	{-# LANGUAGE DeriveFunctor #-}
	{-# LANGUAGE DeriveGeneric #-}
	{-# LANGUAGE DerivingStrategies #-}
	{-# LANGUAGE DerivingVia #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE NoStarIsType #-}
	{-# LANGUAGE PatternSynonyms #-}