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

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

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

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

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

brendanzab

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

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