Skip to content

Instantly share code, notes, and snippets.

View jiribenes's full-sized avatar

Jiří Beneš jiribenes

View GitHub Profile
@pchiusano
pchiusano / monads.u
Last active April 21, 2024 07:40
Converting between algebraic effects and monads
-- This gist shows how we can use abilities to provide nicer syntax for any monad.
-- We can view abilities as "just" providing nicer syntax for working with the
-- free monad.
ability Monadic f where
eval : f a -> a
-- Here's a monad, encoded as a first-class value with
-- two polymorphic functions, `pure` and `bind`
type Monad f = Monad (forall a . a -> f a) (forall a b . f a -> (a -> f b) -> f b)
@JamesMGreene
JamesMGreene / gitflow-breakdown.md
Last active April 16, 2024 16:36
`git flow` vs. `git`: A comparison of using `git flow` commands versus raw `git` commands.

Initialize

gitflow git
git flow init git init
  git commit --allow-empty -m "Initial commit"
  git checkout -b develop master

Connect to the remote repository

@AndrasKovacs
AndrasKovacs / ZeroCostGC.md
Last active April 6, 2024 17:07
Garbage collection with zero-cost at non-GC time

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

@cgsdev0
cgsdev0 / house_builder.sh
Created February 3, 2024 16:07
house builder pattern in bash
#!/usr/bin/env bash
function house_builder() {
# floors,rooms,has_garage
echo "0,0,0"
}
function set_field() {
local f r g
IFS=, read f r g
@CodaFi
CodaFi / AlgorithmW.swift
Last active March 31, 2024 23:25
A Swift Playground containing Martin Grabmüller's "Algorithm W Step-by-Step"
/// Playground - noun: a place where people can play
/// I am the very model of a modern Judgement General
//: # Algorithm W
//: In this playground we develop a complete implementation of the classic
//: algorithm W for Hindley-Milner polymorphic type inference in Swift.
//: ## Introduction

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.

@AndrasKovacs
AndrasKovacs / HOASOnly.hs
Last active February 27, 2024 15:50
HOAS-only lambda calculus
{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}
{-|
Minimal dependent lambda caluclus with:
- HOAS-only representation
- Lossless printing
- Bidirectional checking
- Efficient evaluation & conversion checking
Inspired by https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196
@rygorous
rygorous / gist:e0f055bfb74e3d5f0af20690759de5a7
Created May 8, 2016 06:54
A bit of background on compilers exploiting signed overflow
Why do compilers even bother with exploiting undefinedness signed overflow? And what are those
mysterious cases where it helps?
A lot of people (myself included) are against transforms that aggressively exploit undefined behavior, but
I think it's useful to know what compiler writers are accomplishing by this.
TL;DR: C doesn't work very well if int!=register width, but (for backwards compat) int is 32-bit on all
major 64-bit targets, and this causes quite hairy problems for code generation and optimization in some
fairly common cases. The signed overflow UB exploitation is an attempt to work around this.
@rntz
rntz / MinimalNBE.hs
Last active November 21, 2023 15:17
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.

Program Analysis, a Big Happy Family

The idea behind program analysis is simple, right? You just want to know stuff about your program before it runs, usually because you don't want unexpected problems to arise (those are better in movies.) Then why looking at Wikipedia gives you headaches? Just so many approaches, tools, languages 🤯

In this article I would like to give a glimpse of an overarching approach to program analysis, based on ideas from abstract interpretation. My goal is not to pinpoint a specific technique, but rather show how they have common core concepts, the differences being due mostly to algorithmic challenges. In other words, static analysis have a shared goal, but it's a challenge to make them precise and performant.

Code is meant to be executed by a computer. Take the following very simple function:

fun cantulupe(x) = {