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

data Tm = Var Int | Ann Tm Tm | Abs Tm | App Tm Tm | Pi Tm Tm | Uni
  deriving (Show, Eq)
data Clos = Clos Tm Env
  deriving (Show, Eq)
data Dm = DVar Int | DAbs Clos | DApp Dm Dm | DPi Dm Clos | DUni
  deriving (Show, Eq)
type Env = [Dm]

appd :: Clos -> Dm -> Dm
appd (Clos b e) t = eval (t : e) b

brendanzab

fn new_foo(a: &Path) -> Result<~Foo, ~str> {
    read_whole_file(a).chain(|b| frob(b))
                      .chain(|b| baz(b))
                      .map_move(|b| ~Foo { bar: b })
}

brendanzab

use std::{os,str};

fn main() {
    let args = os::args();
    match args.tail() {
        [~"-n",..strs] => print(str::connect(strs, " ")),
        strs => println(str::connect(strs, " ")),
    }
}

brendanzab

The first stage would be to unify the struct and type keywords.

Current syntax

struct Name {
    first: ~str,
    last: ~str
}
 
struct Point(int, int);

brendanzab

RUSTC ?= rustc

#LOG_FLAGS ?= RUST_LOG=rustc::metadata::creader

all: glhex

run: all
	./glhex

glhex: main.rs *.rs

brendanzab

use to_str::ToStr;

macro_rules! map_cast(
    (~[$($elems:expr),+] -> $T:ty) => (~[$($elems as $T),+]);
    (@[$($elems:expr),+] -> $T:ty) => (@[$($elems as $T),+]);
    ($arr:expr -> $T:ty) => ($arr.map(|a| *a as $T));
)

fn main() {
    let arr1 = map_cast!(~[1, 2.5] -> ToStr);

brendanzab

fn main() {
    let stuff = ~[~"one", ~"two", ~"three"];

    stuff
      .map(|s| str::append(~"lol", *s))
      .map(|s| io::println(*s));
}

brendanzab

fn main() {
    swizzle_gen();
}

fn swizzle_gen() {
    swizzle_gen0("x");
    swizzle_gen0("y");
    swizzle_gen0("z");
    swizzle_gen0("w");
}

brendanzab

// user application

loop {
  window.poll_events();
}

// mac/glutin

fn poll_events(&self) {
  nsapp_waitevent();