Brendan Zabarauskas brendanzab

Pi-Sigma-Self

The following is a set of syntax-directed rules to typing a dependently type system with self types. This is hopefully decidable given decidable conversion checking.

The main innovation is that all introduction rules propagate the self due to the new type of checking rule. This allows the fixpoint to be transparent to introductions, when combined with pairs, this leads to mutual recursion and the inductive types.

This doesn't define any universe or restriction to fixpoints, as those are more or less orthogonal to the typing issues here.

Syntax

using some templates with some hacky macros to allow matching on the contents of a std::variant, and getting the underlying value immediately.


	{-# language Strict, LambdaCase #-}

	module ReasonableLC where

	type Ix = Int
	type Lvl = Int

	-- environment trimming, drops some entries
	data Trim = Empty \| Keep Trim \| Drop Trim

	#lang racket

	;; CIS531 -- Fall 2025
	;; Kristopher Micinski
	;;
	;; Notes on CPS Conversion

	#;(+ (* (read) 3) (+ 4 5))

	;; When we translate constructs like +, *, and other

	(* this whole thing is a sketch *)
	type var = int [@@deriving show { with_path = false }]

	type term =
	\| T_var of var
	\| T_let of var * term * term
	\| T_lambda of var * term
	\| T_apply of term * term
	\| T_reify of thunk

	module Syntax = struct
	type var = string

	type term =
	\| T_var of var
	\| T_let of var * term * term
	\| T_annot of term * term
	\| T_with_self of term * term
	(* pi *)
	\| T_forall of var * term * term

	import bisect
	from dataclasses import dataclass

	class Bound:
	def to_bound(self): return self
	def __lt__(self, other):
	return self <= other and self != other
	def __le__(self, other):
	if isinstance(self, Init) or isinstance(other, Done): return True
	if isinstance(self, Done) or isinstance(other, Init): return False

	-- A lower bound in a totally ordered key-space k; corresponds to some part of an
	-- ordered sequence we can seek forward to.
	data Bound k = Init \| Atleast !k \| Greater !k \| Done deriving (Show, Eq)
	instance Ord k => Ord (Bound k) where
	Init <= _ = True
	_ <= Done = True
	_ <= Init = False
	Done <= _ = False
	Atleast x <= Atleast y = x <= y
	Atleast x <= Greater y = x <= y

	{- cabal:
	build-depends: base, random, containers
	-}
	{-# LANGUAGE GADTs, ViewPatterns, GHC2021 #-}
	import Text.Printf
	import Control.Monad (liftM, ap)
	import Data.Function (on)
	import Data.List (sort, minimumBy)
	import System.Random
	import qualified Data.Map as M

	open import Data.Nat
	open import Data.Nat.Properties
	open import Relation.Binary.PropositionalEquality
	open import Data.Product
	open import Data.Sum
	open import Relation.Nullary

	module MonoidNat3 where

	data Expr : Set where