Brendan Zabarauskas brendanzab

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.

🚚 The bookmarklet has moved to https://github.com/bramus/mastodon-profile-redirect/

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

	module D = Effect.Deep

	type 'a expr = ..
	type _ Effect.t += Extension : 'a expr -> 'a Effect.t

	(* Base Interpreter *)
	type 'a expr +=
	\| Int : int -> int expr
	\| Add : int expr * int expr -> int expr
	\| Sub : int expr * int expr -> int expr

	module type Form = sig
	type ('env, 'a) meaning

	val vz : ('a * 'env, 'a) meaning
	val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
	val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

	val appl :
	('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
	end

	module type Form = sig
	type 'a meaning

	val lam : ('a meaning -> 'b meaning) -> ('a -> 'b) meaning
	val appl : ('a -> 'b) meaning -> 'a meaning -> 'b meaning
	end

	(* Evaluate a given term. *)
	module Eval = struct
	type 'a meaning = 'a

	let rec eval = function
	\| `Appl (m, n) -> (
	let n' = eval n in
	match eval m with `Lam f -> eval (f n') \| m' -> `Appl (m', n'))
	\| (`Lam _ \| `Var _) as t -> t

	let sprintf = Printf.sprintf

	(* Print a given term using De Bruijn levels. *)
	let rec pp lvl = function

	-- One argument operations with strict evaluation strategy
	inductive UnOp : Type :=
	\| ufst : UnOp -- first element of the pair
	\| usnd : UnOp -- second element of the pair
	\| umkl : UnOp -- left constructor of either type
	\| umkr : UnOp -- right constructor of either type
	deriving DecidableEq

	open UnOp

	{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}

	{-
	(compiled with GHC 9.4.2)
	-}

	{-
	HEADS UP
	this is an example implementation of a non-trivial type system using bidirectional type checking.
	it is...