Brendan Zabarauskas 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.

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

Current syntax

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

	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

	fn main() {
	swizzle_gen();
	}

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

	// user application

	loop {
	window.poll_events();
	}

	// mac/glutin

	fn poll_events(&self) {
	nsapp_waitevent();

	rustc src/lib.rs -o idris/idrisfs.o --crate-type=lib --emit=obj

	Undefined symbols for architecture x86_64:
	"___morestack", referenced from:
	_sizeof_int in idrisfs.o
	sizeof_int::__rust_abi in idrisfs.o
	mem::size_of::h1f2d9faff57bec09oaa::v0.0 in idrisfs.o
	ld: symbol(s) not found for architecture x86_64
	clang: error: linker command failed with exit code 1 (use -v to see invocation)
	FAILURE: gcc -O2 -fwrapv -fno-strict-overflow -I. ./idrisfs.o -x c /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/idris5178 -L/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/rts -lidris_rts -lgmp -lpthread -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/rts -I. -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/prelude -I/Users/sven/Library/Haskell/ghc-7.6.3/lib/idris-0.9.12/share/base -o /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/idris5176

	use std::iter::Iterator;

	fn map<T, U, I: Iterator<T>>(fun: \|T\| -> U, mut iter: I) -> Vec<U> {
	let mut acc = vec![];
	for elt in iter {
	acc.push(fun(elt));
	}
	acc
	}

	extern crate serialize;

	use serialize::json;

	fn get_string<'a>(data: &'a json::Json, key: &~str) -> Option<&'a str> {
	match *data {
	json::Object(ref map) => {
	match map.find(key) {
	Some(&json::String(ref s)) => {
	Some(s.as_slice())

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

	use std::{os,str};

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