Brendan Zabarauskas brendanzab

September 2022:

This has spread to a far wider audience than I had anticipated - probably my fault for using a title that is in hindsight catnip for link aggregators. I wrote this back in 2021 just as a bunch of personal thoughts of my experiences using Rust over the years (not always well thought through), and don't intend on trying to push them further, outside of personal experiments and projects.

Managing a living language is challenging and difficult work, and I am grateful for all the hard work that the Rust community and contributors put in given the difficult constraints they work within. Many of the things I listed below are not new, and there's been plenty of difficult discussions about many of them over the years, and some are being worked on or postponed, or rejected for various good reasons. For more thoughts, please see my comment below.

My personal list of Rust gr

	// Syntax

	pub enum Expr {
	Int(i32),
	Neg(Box<Expr>),
	Add(Box<Expr>, Box<Expr>),
	Mul(Box<Expr>, Box<Expr>),
	}

	// Semantics

	(** Phrase generator based on an example from the Grammatical Framework tutorial.

	- {{:https://okmij.org/ftp/gengo/NASSLLI10/}
	Lambda: the ultimate syntax-semantics interface}
	- {{:https://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html#toc16}
	Grammatical Framework Tutorial: Lesson 2}

	Todo:

	- generate languages (orthographies, vacabularies, grammars)

	(** An elaborator for a simply typed lambda calculus with mutable metavars.

	This implementation is based on Arad Arbel’s gist:
	https://gist.github.com/aradarbel10/837aa65d2f06ac6710c6fbe479909b4c
	*)

	module Core = struct

	(** {1 Types} *)

	//! Bidirectional type checker for a simple functional language

	use std::rc::Rc;

	#[derive(Clone, PartialEq, Eq)]
	enum Type {
	Bool,
	Int,
	Fun(Rc<Type>, Rc<Type>),
	}

	module IndexedMonad = struct

	module type S = sig

	type ('i, 'a) t

	val pure : 'a -> (_, 'a) t
	val bind : ('i, 'a) t -> ('a -> ('i, 'b) t) -> ('i, 'b) t

	end

	(** {0 An implementation of a small dependently typed language}

	This is an implementation simple dependently typed language where types are
	first-class and where the output types of functions may depend on the inputs
	supplied to them.

	Type checking is is implemented in terms of an {i elaborator}, which checks
	and tanslates a user-friendly {i surface language} into a simpler and more
	explicit {i core language} that is more closely connected to type theory.
	Because we need to simplify types during elaboration we also implement an

	(** {0 Elaboration with Record Patching and Singleton Types}

	This is a small implementation of a dependently typed language with
	dependent record types, with some additional features intended to make it
	more convenient to use records as first-class modules. It was originally
	ported from {{: https://gist.github.com/mb64/04315edd1a8b1b2c2e5bd38071ff66b5}
	a gist by mb64}.

	The type system is implemented in terms of an ‘elaborator’, which type
	checks and tanslates a user-friendly surface language into a simpler and

	:- module(core,
	[ % Operational semantics

	eval/2, % +Expr, -VExpr
	quote/2, % +VExpr, -Expr
	normalise/2, % +Term, -Term

	eval/3, % +Env, +Expr, -VExpr
	quote/3, % +Len, +VExpr, -Expr
	normalise/3, % +Env, +Term, -Term