András Kovács AndrasKovacs

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

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.

	{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}

	{-\|
	Minimal dependent lambda caluclus with:
	- HOAS-only representation
	- Lossless printing
	- Bidirectional checking
	- Efficient evaluation & conversion checking

	Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196


	{-# 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.

	-- Examples

	data Foo = A \| B \| C

	foo :: Foo -> Int
	foo A = 10
	foo B
	foo C = 20

	foo :: Foo -> Int

	{-
	At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

	"A simple and efficient implementation of strong call by need by an abstract machine"
	https://dl.acm.org/doi/10.1145/3549822

	This is right up my alley since I've implemented strong call-by-need evaluation
	quite a few times (without ever doing more formal analysis of it) and I'm also
	interested in performance improvements. Such evaluation is required in
	conversion checking in dependently typed languages.

	{-# OPTIONS --type-in-type #-}

	open import Relation.Binary.PropositionalEquality
	renaming (cong to ap; sym to infixl 6 _⁻¹; subst to tr; trans to infixr 4 _◾_)
	open import Data.Product
	renaming (proj₁ to ₁; proj₂ to ₂)

	--------------------------------------------------------------------------------

	NatAlg : Set


	Require Import Coq.Unicode.Utf8.

	(*
	As far as I can tell, there is way more literature in Agda on datatype-generic
	programming than in Coq. I think part of the reason is that the Agda literature
	makes liberal use of induction-recursion and fancy termination/positivity
	checking, to define fixpoints of functors. These features are not available in
	Coq.


	{-# language LambdaCase, Strict, OverloadedStrings, DerivingVia #-}
	{-# options_ghc -Wincomplete-patterns #-}

	{-\|
	Simple universe polymorphism. Features:

	- Non-first-class levels: there is a distinct Pi, lambda and application for
	levels. Levels are distinct from terms in syntax/values.
	- The surface language only allows abstraction over finite levels. Internally,

	open import Relation.Binary.PropositionalEquality
	renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
	open import Data.Empty
	open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

	infixr 3 _⇒_
	infix 3 sort⇒_
	infixl 2 _▶_
	infix 2 _$_
	infixr 4 _∷_ _∷'_