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

	{-
	At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

	"A simple and efficient implementation of strong call by need by an abstract machine"
	https://dl.acm.org/doi/10.1145/3549822

	This is right up my alley since I've implemented strong call-by-need evaluation
	quite a few times (without ever doing more formal analysis of it) and I'm also
	interested in performance improvements. Such evaluation is required in
	conversion checking in dependently typed languages.

	%{
	(** the [Surface] module contains our AST. *)
	open Surface

	(** exception raised when a [nonempty_list] returns an empty list. *)
	exception EmptyUnfolding

	(** desugars `(x y z : a) -> b` into `(x : a) -> (y : a) -> (z : a) -> b`. *)
	let rec unfoldPi (xs : string list) (dom : expr) (cod : expr) : expr =
	match xs with

	(** Core Types *)
	module Syntax =
	struct
	type t =
	\| Local of int
	\| Hole of string
	\| Let of string * t * t
	\| Lam of string * t
	\| Ap of t * t
	\| Pair of t * t

	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	;;
	;; Solo freelancer's S-Corp tax optimization
	;;
	;; Assumes an unmarried single-shareholder and tons of other stuff.
	;; I'm not a tax professional, no guarantees here, probably typos, etc. Come on!
	;; Run with https://github.com/Z3Prover/z3
	;;
	;; See also my notes at https://kevinlynagh.com/financial-plan/

	package amyc.ast

	import amyc.utils.Positioned

	/* A polymorphic module containing definitions of Amy trees.
	*
	* This trait represents either nominal trees (where names have not been resolved)
	* or symbolic trees (where names/qualified names) have been resolved to unique identifiers.
	* This is done by having two type fields within the module,
	* which will be instantiated differently by the two different modules.

	module Hints exposing (..)

	import List
	import Html exposing (..)
	import Html.Attributes as A

	{-----------------------------------------------------------

	SYNTAX HINTS (OCaml -> Elm)

	(* Itty bitty SMT solver: DPLL(T) where T = equality *)
	(*
	# let x, y = 0, 1 (* integer variable IDs *) ;;
	# let prob = SMT.new_problem 2 (* 2 for two variables *) ;;
	# let b = SMT.new_bool prob;;
	# SMT.add_clause prob [b; SMT.eq prob x y];
	SMT.add_clause prob [SMT.not b];
	SMT.solve prob;;
	- : SMT.response = SMT.SAT
	# SMT.add_clause prob [SMT.not (SMT.eq prob x y)];