brendanzab

(** {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

brendanzab

[{"tag":"Heading","contents":[0,"Martin-Löf Type Theory"]},{"tag":"Paragraph","contents":"A description of Martin-Löf Type Theory in Holbert, by Brendan Zabarauskas."},{"tag":"Paragraph","contents":"Original gist: ~https://gist.github.com/brendanzab/1b4732179b15201bf33fed6dbca02458~"},{"tag":"Heading","contents":[2,"Introduction"]},{"tag":"Paragraph","contents":"/Martin-Löf Type Theory/ (MLTT), also known as /Intuitionistic Type Theory/, is a type theory proposed by Per Martin-Löf in the mid 70s. It forms the basis of many popular dependently typed programming languages and theorem provers, for example Agda, Coq, Idris, Epigram, and more. The influence of MLTT also extends to other languages, for example partly inspiring the module systems of Standard ML and OCaml, and in the work on adding dependent types to Haskell."},{"tag":"Paragraph","contents":"The main forms of judgement in this presentation of Martin-Löf Type theory are:\n\n- $A:_type A$\n    which can be read as “$A:A$ is a type”\n\n- $A a:_:_ a A$\n

brendanzab

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

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

brendanzab

Weird field/param language 2

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

This is a more succinct syntax than the previous gist, this time using in and out in place of param and record, and making introductions and eliminations more succinct.

Grammar

brendanzab

Weird field/param language

Further messing around on top of some ideas in the previous gist.

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

Grammar

term, type ::=\

brendanzab

Weird binder language thingy

Playing around with a uniform notation for binders (eg. Π, Σ, λ, let). This is probably not the greatest language to program in directly, but I think it's fun to see if a more consistent syntax can help to expose some of the differences between dependent functions, dependent pairs, and let expressions...

Syntax

brendanzab

Weird type theory diagrams

I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these :sparkles: very informal :sparkles: Venn diagram thingies.

Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!

Syntax

brendanzab

Implementing Inference Rules

When first reading programming language papers, it can be challenging to figure out how to translate the notation into working implementations. The following post is intended to help show how these rules correspond to working implementations in Prolog, OCaml, and Lean, for a very simple language of arithmetic expressions.

Natural deduction

T ::=
  | Int
 | Bool

brendanzab

Quantifiers

Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.

Examples

{
 out id : {