Brendan Zabarauskas brendanzab

A somewhat brief overview of typechecking System F

This document comprises an example of typechecking a type system based on System F, in a small ML-like language.

You can skip the below section if you already understand System F itself.

A brief overview of System F

System F is the name given to an extension of the simply typed lambda calclus.

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

	{-# OPTIONS --without-K #-}

	-- version 1, conversion is indexed over conversion
	module IndexedConv where

	data Con : Set
	data Ty : Con → Set
	data Sub : Con → Con → Set
	data Tm : ∀ Γ → Ty Γ → Set
	data Con~ : Con → Con → Set

	{-# OPTIONS --guarded #-}


	open import Agda.Primitive
	open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
	open import Data.Unit using (⊤; tt)
	open import Data.Nat -- using (ℕ; _+_; suc; _<_)
	open import Data.Nat.Properties
	open import Data.Fin using (Fin; fromℕ; fromℕ<)
	open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)

	{-# OPTIONS --cubical #-}

	open import Agda.Builtin.Cubical.Path
	open import Agda.Primitive.Cubical

	cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y)
	→ PathP (λ i → B (p i)) (f x) (f y)
	cong f p i = f (p i)

	open import Data.Nat

	{-# LANGUAGE GADTs #-}

	import Control.Monad

	-- Note that Cmd values are perfectly "pure" values. There's nothing here that
	-- makes them impure.
	data Cmd a where
	PutStr :: String -> Cmd ()
	PutStrLn :: String -> Cmd ()
	ReadLn :: Cmd Int

	{-# language
	BlockArguments
	, ConstraintKinds
	, ImplicitParams
	, LambdaCase
	, OverloadedStrings
	, PatternSynonyms
	, Strict
	, UnicodeSyntax
	#-}

	module C : sig
	type t
	val empty : t
	val one : char -> t
	val union : t -> t -> t
	val inter : t -> t -> t
	val top : t
	val mem : char -> t -> bool
	val make : (char -> bool) -> t
	val equal : t -> t -> bool