Skip to content

Instantly share code, notes, and snippets.

@cheery
cheery / study.py
Created January 25, 2024 15:12
Carnivore mortality study on NHANES I dataset.
is_carnivore_in_1971 = {}
is_alive_in_1992 = {}
age_of_death = {}
with open('nhanes/DU4701.txt', 'r') as fd:
rows = fd.readlines()
for row in rows:
sample = row[0:5]
meat_freq = int(row[224:228])
diet = [0, 0, 0]
@cheery
cheery / Structures.agda
Created December 20, 2023 06:21
Tree editing scaffolds
module Structures where
open import Data.Unit
open import Data.Product
open import Data.Empty
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Maybe
open import Data.List
@cheery
cheery / Simple.hs
Created December 6, 2023 15:59
Extension to cubical (WIP)
module Simple where
import Bwd -- https://gist.github.com/cheery/eb515304a0a7bcf524cb89ccf53266c2
data Interval
= I0
| I1
| In Int
deriving (Show, Eq)
@cheery
cheery / Bwd.hs
Created December 5, 2023 13:11
Simple dependently typed evaluator
module Bwd where
data Bwd a = Empty
| Bwd a :> a
instance Functor Bwd where
fmap f Empty = Empty
fmap f (xs :> x) = fmap f xs :> f x
instance Eq a => Eq (Bwd a) where
@cheery
cheery / catpu.hs
Created November 22, 2023 12:11
Pattern unification
module CatPu where
import Control.Applicative (Alternative (..))
import Control.Monad (MonadPlus (..), foldM, forM)
import Control.Monad.State
import Control.Monad.Except
import Data.List (intersect, elemIndex)
type Goal = SolverState -> Stream SolverState
@cheery
cheery / hedberg.agda
Created February 9, 2023 16:36
Hedberg's theorem
{-# 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
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.
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
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
{-# 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₁