Skip to content

Instantly share code, notes, and snippets.


Max Heiber mheiber

View GitHub Profile

Slogans about Mainstream Dependent Types

I find it can be hard for programmers to talk about dependent types, since we don't always have the same idea of what they are and they have a reputation of being hard to understand and implement. I want to share these slogans to (hopefully) make the conversation easier.

I wrote this in a hurry and would welcome comments with examples of "mainstream dependent types" - and any relevant corrections and links.

Note: "mainstream" is a moving target

  1. "A dependent type is a type whose definition depends on a value."
View dubstep.v
Ltac dubstep_goal F :=
unfold F; fold F.
Ltac dubstep_in F H :=
unfold F in H; fold F in H.
Tactic Notation "dubstep" constr(F) := (dubstep_goal F).
Tactic Notation "dubstep" constr(F) "in" hyp(H) := (dubstep_in F H).
View gist:3ff8ff01224820249c34e2092f88181d
set nocompatible
filetype off " required for Vundle
:set suffixesadd+=.js
nnoremap <leader><space> :noh<return>
nnoremap <leader><leader> :b#<CR>
nnoremap <leader>s :source ~/.vimrc<CR>
nnoremap <leader>q :xall<CR>
nnoremap <right> <C-w>10>
nnoremap <left> <C-w>10<
nnoremap <up> :resize -5<Cr>
mheiber / count.erl
Created May 23, 2020, count.erl
View count.erl
main(FileName) ->
{ok, Device} = file:open(FileName, [read]),
Cnt = device_counts(Device, maps:new()),
io:format("~p", [Cnt]).
device_counts(Device, Map) ->
case io:get_line(Device, "") of
View Equality: prior

Equality: Prior Art in Programming Languages

This document contains notes on how equality works in different programming languages, with a focus on immutable data types in functional languages.


OCaml and Reason

OCaml has two equality primitives:


Should this error?

class Parent {
  copy(instance) {
    this.#foo =;
class Child extends Parent {}
mheiber / TypeScript's Type System as a Little
Last active Apr 28, 2019
2019 Conference Talk: TypeScript's Type System as a Little Language
View TypeScript's Type System as a Little

TypeScript's Type System as a Little Language

Theme: Thinking of type-level TS as a programming language

It has all the pieces!

  • data:
    • objects, arrays, and tuples
  • functions
  • structured programming: