Instantly share code, notes, and snippets.

# Philip Zucker philzook58

Last active April 12, 2024 07:27
theme class highlighter fonts
default
text-center
sans serif mono
sans-serif
serif
monospace
Last active October 12, 2023 09:09
A complete compiler for a simple language (in less than 150 LoC)

This project is a tiny compiler for a very simple language consisting of boolean expression.

The language has two constants: `1` for true and `0` for false, and 4 logic gates: `!` (not), `&` (and), `|` (or), and `^` (xor).

It can also use parentheses to manage priorities.

Here is its grammar in BNF format:

expr ::= "0" | "1"

Created July 5, 2021 19:14

Confluence. It's not just a place where you can complain about colleagues to other colleagues.

It's also a property that is quite useful in many areas of CS!

As a reminder, a (non-deterministic) reduction relation --> is confluent if for every (multi-step) "peak" `u *<-- t -->* v` (I use `-->*` for the multi-step version of `-->`) there is a corresponding "valley": `u -->* w *<-- v`.

This basically says that your computation can't be "too"

Created March 29, 2020 23:42

This post will discuss how to model Simplicial Sets (sSets) in Haskell, using their category-theoretic definition.

# Introduction

If you want to know what these are, a good primer is Friedman's introduction to simplicial sets. Another, more concrete perspective is provided by Sergeraert's introduction to combinatorial homotopy theory

Now why would we want to model this thing anyway, and why are we going to jump through categorical hoops to do so?

Well, we want to model sSets because they are a basic way in which people carry out homotopy theory, which in turn is about reducing the class of spaces (or shapes, if you prefer) into spaces modulo their continuous transformations into one another, thus giving us a way to talk about shapes/spaces ""in general"". Now in turn we need to represent shapes/spaces in a concrete way, and we do so by identifying them with certain decompositions of them

Last active June 16, 2024 19:07

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation `m >>= f`, then `f` is `m`’s continuation. It’s the function that is called with `m`’s result to continue execution after `m` returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

`m >>= f >>= g >>= h`

then the continuation of `m` is `f >=> g >=> h`. Likewise, the continuation of `m >>= f` is `g >=> h`.

Created November 12, 2019 00:25
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 # I am ashamed for writing this. import inspect; class Cin: """ time to whip out some python magic """ def __rshift__(self, other): # I don't want to require that "other" is declared global. cin = input();
Last active August 5, 2024 12:14
Program Analysis Resources (WIP draft)

# Program Analysis Resources

(draft; work in progress)

Last active May 23, 2024 04:02

# A series of reading lists mostly related to functional programming.

Last active January 23, 2020 20:31
Formalization of a small part of the Parametricity Tutorial blog post
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* Developed using Coq 8.4pl5 *) Require Import Coq.Setoids.Setoid. Require Import Coq.Logic.ProofIrrelevance. Require Import Coq.Logic.JMeq. Set Implicit Arguments. (* Auxiliary *)
Last active March 24, 2024 21:13
Statically Typed Lisp

Basic unit type:

```λ> replTy "()"
() :: ()```

Basic functions: