brendanzab

NOTE: This was first authored on 26 Feb 2014. Things may have changed since then.

C++'s Templates

C++'s templates could be seen as forming a duck typed, purely functional code generation program that is run at compile time. Types are not checked at the initial invocation stage, rather the template continues to expand until it is either successful, or runs into an operation that is not supported by that specific type – in that case the compiler spits out a 'stack trace' of the state of the template expansion.

To see this in action, lets look at a very simple example:

template 

brendanzab

(** Fractal binary trees

    L-systems are a really wonderful model of plant growth, showing how a set of
    simple grammar rules can result in incredibly life-like and complicated
    organic forms.

    They do however seem a little… stuck in the 80s? In L-systems the state of a
    plant is modelled as a list of instructions, where the branching structure
    emerges from an imperative interpretation of “push” and “pop” symbols. For
    example an L-system that describes a fractal binary tree looks like this:

brendanzab

World building miscellany

Procedural Generation

• Wikipedia: Noctis (Web page)
• Noctis - Official site (Web page)
• Proteus - early prototype screenshots (Blog post)
• Gamasutra: The Making of Elite (Video)
• The Brilliance of Dwarf Fortress
• Interview with Tarn Adams (creator of Dwarf Fortress) (Slides) (Video)

brendanzab

(*
  T ::=
    | Bool
    | T -> T

  t ::=
    | x
    | \(x : T). t
    | t t

brendanzab

// Syntax

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

// Semantics

brendanzab

I think I’ve figured out most parts of the cubical type theory paper(s); I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory? A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then? A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

Q: So what are HIT and UA? A: A HIT is a type equipped with custom equality, as an example, you can write a type similar to the natural numbers but with an equality between all even numbers. Well, it cannot be called natural numbers then.

brendanzab

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

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

//! 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>),
}

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