Brendan Zabarauskas brendanzab

Basic setup for formalizing elaboration

First attempts

Elaboration is, broadly speaking, taking user-written syntax and converting it to "core" syntax by filling in missing information and at the same time validating that the input is well-formed.

I haven't been fully happy with formalizations that I previously used, so I make a new attempt here. I focus on a minimal dependently typed case.

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.

	-- Polarized lambda calculus to A-normal form
	-- With eta-expansion and call-saturation

	type Ix = Int
	type Lvl = Int

	data Ty = TInt
	deriving (Show)
	data TFun = TFun [Ty] Ty
	deriving (Show)

	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

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