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

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

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

brendanzab

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

brendanzab

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
}

brendanzab

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

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