Skip to content

Instantly share code, notes, and snippets.

@cheery
cheery / hedberg.agda
Created February 9, 2023 16:36
Hedberg's theorem
View hedberg.agda
{-# OPTIONS --cubical #-}
module hedberg where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
data Empty : Set where
absurd : {A : Set} → Empty → A
@cheery
cheery / newtry6.agda
Created January 26, 2023 16:29
Normalizer for lambda calculus
View newtry6.agda
module newtry6 where
-- derived from https://gist.github.com/rntz/2543cf9ef5ee4e3d990ce3485a0186e2
-- http://eprints.nottingham.ac.uk/41385/1/th.pdf
open import Level
open import Function using (id; _∘_)
infixr 5 _⇒_
data Ty : Set where
@cheery
cheery / newtry.agda
Created January 25, 2023 16:33
Preservation proof doesn't go through.
View newtry.agda
module newtry where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Data.Fin
open import Data.Nat
open import Data.Product
open import Data.Empty
@cheery
cheery / demo.agda
Created January 23, 2023 18:13
Failed normalization by evaluation
View demo.agda
module demo where
open import Agda.Builtin.Equality
open import Data.List
open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Data.Fin.Base
open import Data.Product
open import Data.Sum
@cheery
cheery / demo..agda
Created January 21, 2023 05:36
Functors in lambda calculus
View demo..agda
{-# OPTIONS --type-in-type #-}
module demo where
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Equality
data Unit₁ : Set₁ where
point : Unit₁
@cheery
cheery / demo.agda
Last active January 20, 2023 12:28
chu spaces
View demo.agda
{-# OPTIONS --guardedness #-}
module demo where
open import Data.Product
open import Data.Empty
open import Agda.Builtin.Equality
open import Agda.Primitive
sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
@cheery
cheery / SimplyDifficult.hs
Last active February 22, 2022 11:53
Dynamic pattern matching attempt
View SimplyDifficult.hs
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs, FlexibleContexts #-}
module SimplyDifficult where
-- This thing demonstrates dynamic pattern unification,
-- however the examples are too simple to verify that the unifier is
-- working correctly.
-- There were also a thing or two that were way too hard to implement.
-- I've omitted them.
View SimplyEasy.hs
module SimplyEasy where
-- From the paper: http://strictlypositive.org/Easy.pdf
-- An attempt to add case -statement.
-- Fails on typechecking a case.
data Name
= Const String
| Bound Int
| Unquoted Int
deriving (Show, Eq)
View continuations.py
from rpython.rlib.rstacklet import StackletThread
from rpython.rlib.objectmodel import specialize
import core
class SThread(StackletThread):
def __init__(self, config):
StackletThread.__init__(self, config)
self.cont = None
def get_sthread():
@cheery
cheery / ukanren.py
Last active January 29, 2022 20:21
ukanren with untested CHR
View ukanren.py
# -*- encoding: utf-8 -*-
class TermOrVar(object):
def to_str(self, rbp=0):
assert False
class Term(TermOrVar):
def __init__(self, name, args):
self.name = name
self.args = args
for arg in args: