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
use std::fmt;
use std::fmt::parse::FlagAlternate;
use std::fmt::parse::FlagSignAwareZeroPad;
use std::fmt::parse::FlagSignPlus;
use std::fmt::parse::{AlignLeft, AlignRight, AlignUnknown};
use std::num::{cast, zero};
use std::uint;
/// Sets that form a boolean algebra.
/// These must contain exactly two elements, top and bottom: `{⊤, ⊥}`, and be
/// equipped with three basic operators: `¬`, `∧`, and `∨`, the definitions of
/// which are outlined below.
pub trait Boolean: Eq {
/// The bottom value, `⊥`.
fn bottom() -> Self;
/// The top value, `⊤`.
struct Checked<T>(T);
impl<T: CheckedAdd> Add<Checked<T>, Option<Checked<T>>> for Checked<T> {
fn add(&self, other: &Checked<T>) -> Option<Checked<T>> {
let (&Checked(ref x), &Checked(ref y)) = (self, other);
x.checked_add(y).map(|z| Checked(z))
impl<T: CheckedSub> Sub<Checked<T>, Option<Checked<T>>> for Checked<T> {
macro_rules! bitset(
($BitSet:ident: $T:ty {
$($VALUE:ident = $value:expr),+
}) => (
pub struct $BitSet {
priv bits: $T,
//! Leveraging tuples to make a statically typed, concatenative EDSL in Rust.
//! I'm not sure how practical it really is – Rust's syntax can make it a little
//! hard to read, but it's fun to play around with it. The neat thing is how
//! little copying occurs. Everything is moved in and out by-value in a pipeline.
//! Thanks goes to [Tekmo on reddit](
//! comments/1zzom4/using_functionlength_to_implement_a_stack_language/cfyibsr)
//! for the idea.
extern crate collections;
use std::fmt;
use std::io;
use collections::HashMap;
fn main() {
let mut stdin = io::stdin();
let mut env = (~[], words::default());
loop {
View arith.hs
evalBigStep :: Tm -> Maybe Tm
evalBigStep (TmIf t1 t2 t3) =
evalBigStep t1 >>= \b1 -> case b1 of
TmTrue -> evalBigStep t2 -- (B-IfTrue)
TmFalse -> evalBigStep t3 -- (B-IfFalse)
_ -> Nothing
evalBigStep (TmSucc t1) =
evalBigStep t1 >>= \t1' -> case t1' of
nv1 | isNumerical nv1 -> Just (TmSucc nv1) -- (B-Succ)
_ -> Nothing

Introducing the lambda calculus

The following function:

fn(x) { t }

can be written using this weird notation devised by Church in the 40s:

λx. t
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)) => {

Introducing the lambda calculus

λx. t

This could be expressed in a 'hypothetical conventional language' as:

fn(x) { t }
You can’t perform that action at this time.