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.
View study.py
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
View Structures.agda
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)
View Simple.hs
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
View Bwd.hs
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
View catpu.hs
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
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₁