Skip to content

Instantly share code, notes, and snippets.

Pondering type systems…

Brendan Zabarauskas brendanzab

Pondering type systems…
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 / dependent.makam
Last active Dec 3, 2019
Messing with dependent type systems in makam (
View dependent.makam
(* terms *)
term : type.
universe : term.
annotate : term -> term -> term.
unitType : term.
unitTerm : term.
pairType : term -> (term -> term) -> term.
pairTerm : term -> term -> term.
brendanzab /
Last active Nov 29, 2019
Pull-based tree processing for lambda calculi.
//! See [this twitter thread](
//! Traditional syntax trees suffer from lots of pointer indirections and poor data locality!
//! Could we stream things instead, using [pull-based events](
//! as opposed to trees? This should be equivalent to our tree based approaches, but might
//! require us to think carefully about what our core calculus looks like in order to make
//! this kind of thing easier.
use std::sync::Arc;
brendanzab /
Last active Nov 14, 2019
🚧 A graph-based core for a dependently typed language. 🚧

A graph-based core for a dependently typed language


An overly-ambitious attempt to re-think the core calculus of dependent type theory by basing it on graphs as opposed to lambdas, Π-types, Σ-types, etc. The hope is that this might allow us to investigate dependency more closely, and allow us to refine programs to target different environments in an easier way than with traditional programming representations.


View term-graph.json
"record.term": {
"fields": {
"identity": { "node": "$identity" },
"compose": { "node": "$compose" },
"Unit": { "node": "$Unit" },
"Bool": { "node": "$Bool" },
"Option": { "node": "$Option" }
"nodes": {
//! Dependent type system that uses a SAX-style event streams between passes.
//! It would be really neat to have a simple state machine language to describe this.
/// Handler for a state machine that accepts input events.
trait InputHandler {
fn on_bytes(self, bytes: &[u8]>);
fn on_list_start(self);
fn on_list_end(self);
View SExprElaborator.purs
module Core.SExpr where
import Prelude
import Data.List (List(..))
import Data.Maybe (Maybe(..))
import Data.Tuple (Tuple(..))
data SExpr
= Array (Array SExpr)
brendanzab / ast-experiment.yml
Last active Nov 4, 2019
Weid idea for an AST that could form the basis of a structured editor.
View ast-experiment.yml
# Concrete syntax:
# ```
# let
# pi
# : float/64
# = 3.1415
# identity ||< The polymorphic identity function
# : [ A : Type ||< The input type.
# , a : A ||< The input.
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

Communicating type theory and formal systems

Doing a better job of communicating type theory and formal systems

Problems to solve

  • languages should have better specifications
  • our current notation limits our reach
  • puts up barriers between researchers and potential implementers
  • hard to gain an intuition of complicated formal systems from static descriptions

Keybase proof

I hereby claim:

  • I am brendanzab on github.
  • I am brendanzab ( on keybase.
  • I have a public key ASCK-tfcF0xTjkXi6kETLYC-Qdnu4R5Acgz1d70mfmJyfwo

To claim this, I am signing this object:

You can’t perform that action at this time.