Skip to content

Instantly share code, notes, and snippets.


Brendan Zabarauskas brendanzab

View GitHub Profile

Weird type theory diagrams

I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these very informal Venn diagram thingies.

Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!



Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=


Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.


  out id : {
brendanzab / Monoids.lean
Last active Mar 5, 2021
Playing with monoids in Lean 4
View Monoids.lean
Playing with monoids in Lean 4
$ lean -v
Lean (version 4.0.0-nightly-2021-02-28, commit 6a6f68f6ccc8, Release)
namespace Monoids
brendanzab / ArithExprs.lean
Last active May 10, 2021
A proof of the correctness of an arithmetic expression compiler and decompiler in Lean 4.
View ArithExprs.lean
A proof of the correctness of an arithmetic expression compiler in Lean 4.
Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's
[course material].
[course material]:
brendanzab / maps.lean
Last active Feb 10, 2021
Total and partial maps in Lean 4 (inspired by Software Foundations)
View maps.lean
Total and partial maps
This is inspired by [the relevant chapter in Software Foundations]. Unlike
Software Foundations, these maps are also parameterised over a `Key`
type, which must supply an implementation of `DecidableEq`.
[Software Foundations]:
namespace Maps
brendanzab /
Last active Oct 18, 2020
Updates on the Pikelet Programming Language
marp theme

Pikelet status update

Brendan Zabarauskas


brendanzab /
Last active Aug 24, 2020
A weird dependent graph language thing?
Notation Meaning
l ? T abstract node in T
l : T concrete node in T
l = t node equal to t
default = t reduce to this node if all nodes are concrete
{ ... } graph term
t1.{ l = t2 } updates node l in t1 to be t2
t.l gets the value of node l in t
t.{ l1 -> l2 } renames l1 to l2 in t
brendanzab / ddl-experiment.makam
Last active May 11, 2020
A dependently typed binary data description language, prototyped in Makam!
View ddl-experiment.makam
% Copyright 2020 YesLogic Pty. Ltd.
% Licensed under the Apache License, Version 2.0 (the "License");
% you may not use this file except in compliance with the License.
% You may obtain a copy of the License at
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS,
brendanzab /
Last active Apr 20, 2020
Probably a terrible idea

Combining Pi and Sigma types?

-- id : forall a. a -> a
-- id x = x

id : type [
    in A : Type, 
    in a : A, 
    out a' : A,