Skip to content

Instantly share code, notes, and snippets.

View mb64's full-sized avatar

Mark Barbone mb64

66 followers · 7 following
View GitHub Profile
@mb64
mb64 / DerivingEq.idr
Created July 10, 2020 03:34
Deriving equality with Idris 2's new reflection -- strange bug where it doesn't work from a different module
module DerivingEq
import Language.Reflection
%language ElabReflection
public export
countArgs : (ty : TTImp) -> Nat
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy
@mb64
mb64 / Bidir.idr
Created August 6, 2020 06:39
An attempt at a well-typed implementation of Complete+Easy. Needless to say, it does not work.
module Bidir
Ident : Type
Ident = String
mutual
BaseCtx' : Type
Ctx' : BaseCtx' -> Type
CtxItem' : (b : BaseCtx') -> (c : Ctx' b) -> Type
@mb64
mb64 / Makefile
Created October 17, 2020 23:59
GCC vs repne scasl: wstrlen bench
.PHONY: all bench
all: bench
bench: main_c main_asm
@echo "Running the C version..."
@bash -c 'time ./main_c'
@echo
@echo "Running the asm version..."
@bash -c 'time ./main_asm'
@mb64
mb64 / flat_tree.c
Created October 31, 2020 08:42
Flat trees in ATS and C
/* A flat representation of
* data Tree = Leaf Int | Node Tree Tree
*
* Either:
* - *ft is LEAF and a single int follows
* - *ft is NODE and two subtrees follow
*/
#define LEAF 0
#define NODE 1
@mb64
mb64 / Nat.agda
Created October 5, 2020 05:52
An attempt to prove that the free semigroup on one generator is commutative.
{-# OPTIONS --cubical --safe #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism using (Iso; isoToPath)
data N : Set where
one : N
_+_ : N → N → N
assoc : (a b c : N) → (a + b) + c ≡ a + (b + c)
@mb64
mb64 / .bashrc
Created December 9, 2020 07:10
reMarkable 2 dotfiles
umask 022
declare -x PAGER='less'
declare -x EDITOR='vim'
declare -x VISUAL="${EDITOR}"
declare -x FCEDIT="${EDITOR}"
declare -x LS_COLORS='no=01;37:fi=01;37:di=01;34:ln=01;36:pi=01;32:so=01;35:do=01;35:bd=01;33:cd=01;33:ex=01;31:mi=00;37:or=00;36:'
declare -x HISTCONTROL=ignoreboth:erasedups
@mb64
mb64 / heap_bench.sml
Created March 13, 2021 00:27
Heap benchmarks in MLton
(** A small benchmark for heap implementations
*
* Task: (mutably) sort an array, using heap sort
* Implementations:
* - BinaryHeap, a simple binary heap implemented with mutable array operations
* - PairingHeap, Okazaki's strict amortized pairing heap
* - SplayHeap, Okazaki's strict amortized splay heap
* - BinomialHeap, Okazaki's strict amortized binomial heap
* - LeftistHeap, Okazaki's strict rank-based leftist heap
*
@mb64
mb64 / PowerSeries.agda
Last active April 7, 2021 23:00
A proof that formal power series over an arbitrary commutative ring form a commutative ring, formalized in Agda using guarded coinduction.
{-# OPTIONS --guardedness --safe #-}
open import Data.Product
open import Function using (_$_)
open import Relation.Binary using (IsEquivalence)
open import Algebra
open import Relation.Binary.Definitions
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open import Tactic.RingSolver using (solve-∀)
@mb64
mb64 / t.elpi
Last active October 12, 2021 21:03
"complete and easy" (mostly), in ELPI
kind ty type.
type tunit ty.
type tfun ty -> ty -> ty.
type tall (ty -> ty) -> ty.
kind tm type.
type unit tm.
type app tm -> tm -> tm.
@mb64
mb64 / generate.sh
Created November 21, 2021 06:10
All the responses to the free-response parts of the Haskell survey
#!/bin/bash
# Source: https://taylor.fausak.me/2021/11/16/haskell-survey-results
wget https://taylor.fausak.me/static/pages/2021-state-of-haskell-survey-results.json.zip
unzip 2021-state-of-haskell-survey-results.json.zip
echo "Question: If you wanted to convince someone to use Haskell, what would you say?" > q1-convince.txt
echo "---" >> q1-convince.txt
jq -r 'map(.s9q0 | .[]?) | join("\n---\n")' < 2021-state-of-haskell-survey-results.json >> q1-convince.txt