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.

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

	type never = \|
	type ('a, 'b) equal = Refl : ('x, 'x) equal

	type ('l, 'r) dec_equal =
	\| D_refl : ('l, 'l) dec_equal
	\| D_neq : (('l, 'r) equal -> never) -> ('l, 'r) dec_equal

	let ( let* ) v f = Option.bind v f

	module Nat = struct

	Set Implicit Arguments.
	Require Import List Program FunctionalExtensionality.

	(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

	(** Names/Variables will be identified with a natural number.
	λx.λy.y x is represented as λλ0 1 *)
	Definition var : Type := nat.

	(** There is a need for partial maps, e.g., to keep track of what variable

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