Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
@brendanzab
brendanzab / CC.hs
Created Sep 7, 2019 — forked from atennapel/CC.hs
Calculus of Constructions, normalization-by-evaluation, semantic typechecking (WIP)
View CC.hs
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
brendanzab / CuTT.md
Last active Jan 27, 2020 — forked from AndyShiue/CuTT.md
Cubical type theory for dummies
View CuTT.md

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
brendanzab / swizzle_gen.rs
Last active Sep 27, 2015 — forked from anonymous/playground.rs
Shared via Rust Playground
View swizzle_gen.rs
fn main() {
swizzle_gen();
}
fn swizzle_gen() {
swizzle_gen0("x");
swizzle_gen0("y");
swizzle_gen0("z");
swizzle_gen0("w");
}
View glutin-ns-events.rs
// user application
loop {
window.poll_events();
}
// mac/glutin
fn poll_events(&self) {
nsapp_waitevent();
View error
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
View map.rs
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
}
View borrow-example.rs
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())
View nest.rs
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 })
}
View echo.rs
use std::{os,str};
fn main() {
let args = os::args();
match args.tail() {
[~"-n",..strs] => print(str::connect(strs, " ")),
strs => println(str::connect(strs, " ")),
}
}
View rust_syntax_proposal_01.md

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

Current syntax

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