Skip to content

Instantly share code, notes, and snippets.

down a type system rabbit hole

Brendan Zabarauskas brendanzab

down a type system rabbit hole
Block or report user

Report or block brendanzab

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
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 /
Last active Jan 27, 2020 — forked from AndyShiue/
Cubical type theory for dummies

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 /
Last active Sep 27, 2015 — forked from anonymous/
Shared via Rust Playground
fn main() {
fn swizzle_gen() {
// user application
loop {
// mac/glutin
fn poll_events(&self) {
View error
rustc src/ -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 {
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)) => {
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, " ")),

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

Current syntax

struct Name {
    first: ~str,
    last: ~str
struct Point(int, int);
You can’t perform that action at this time.