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
laMudri /
Last active May 13, 2020
A version of λR implemented in Prolog
% Database (algebra)
%! type ann := zero | one | omega.
%! zero(+X:ann) is semidet.
%! add(-X:ann, -Y:ann, +Z:ann) is nondet.
%! one(+X:ann) is semidet.
%! mult(+X:ann, -Y:ann, +Z:ann) is nondet.
mujjingun / PCP.cpp
Last active Apr 29, 2020
Undecidable C++ Grammar Example
View PCP.cpp
#include <algorithm>
#include <type_traits>
template <int... Ints>
struct Row {
constexpr static bool empty = (sizeof...(Ints) == 0);
template <typename Upper, typename Lower>
struct Domino {
View avril.tidal
-- happy avril 14th :)))))))))))))))))))))))))))))))))))))))
let bars = 4
key = "8"
righthand = "[[4 -3] [0 _ _ _ _ _ 0]] [[-3, -8] [7 5 4 0]]"
lefthand = "[0 9 12 16] [4 12 16 19] [5 12 17 19] [2 12 17 16]"
d1 $ slow bars
$ stack [
n (righthand + key + "<24 36>/2"),

In Agda, I can write many different records with a lookup field.

record DVec (n : ℕ) (A : Fin n  Set) : Set where
  constructor tabulate
  field lookup : (i : Fin n)  A i
open DVec public

record DMat (m n : ℕ) (A : Fin m  Fin n  Set) : Set where
  constructor tabulate
View futamura.hs
{-# LANGUAGE PartialTypeSignatures, ScopedTypeVariables #-}
-- A description of a program written in the implementation language which computes an `a`
newtype Quote a = Quote a
-- A description of a program written in the object language which computes an `a`
newtype OQuote a = OQuote a
-- For example: if you have a Python interpreter written in Lisp, then
-- x :: Quote Int is the AST for Lisp code which computes an Int
jborichevskiy /
Last active May 19, 2020
The daily template I use for Roam Research
  • Weekly Agenda (created on a different day, and embedded with /Block Reference)
  • [[Morning Questions]]
    • {{[[slider]]}} How many hours of sleep did I get?
    • What's one thing top of mind today?
    • What's the one thing I need to get done today to make progress?
    • Review #[[Index: Questions]] #values
  • Agenda
    • {{[[TODO]]}} Morning walk #goal-health #habit
    • {{[[TODO]]}} Check calendar for scheduled events
    • {{[[TODO]]}} Morning focus hour

How to deal with quotients or setoids?


Lean extends the Calculus of Inductive Constructions with quotient types, as discussed by Carneiro (2019, Sec 2.7.1). However, that and other choices break some metatheoretic properties of CIC (Carneiro, 2019, Sec. 3.1), properties that Coq developers care about; consistency is nevertheless preserved.


Coq does not add support for quotients; one must instead use setoids explicitly. By looking at Carneiro (2019), we can see the difference: unlike quotient A/R, a setoid (A, R) is not a standard type, and we must explicitly remember to use R instead of standard equality wherever needed. Both with setoids and quotients, we must ensure that functions respect the equivalence on their domain. However, when using quotients A/R, that must only be checked for functions that use A/R's eliminator, while with setoids we need more work. For example, take a function f : A/R -> B, and g : B -> C: we can

felko / Main.hs
Last active May 27, 2020
linear lambda calculus typechecker
View Main.hs
, OverloadedLists
, OverloadedStrings
, RecordWildCards
, BlockArguments
, DeriveFunctor
, TypeApplications
, GeneralizedNewtypeDeriving
View lispgraph.hs
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
module Main where
import Data.AttoLisp
import Data.Graph.Inductive.Graph
import Data.Graph.Inductive.PatriciaTree
import Data.GraphViz
sordina / gc.c
Last active Nov 15, 2019
Implementation of Baby's first Garbage Collector from
View gc.c
#define STACK_MAX 256
#include <stdio.h>
#include <stdlib.h>
void gc(); // Pre-Declared for co-recursive usage
You can’t perform that action at this time.