Skip to content

Instantly share code, notes, and snippets.

View jiribenes's full-sized avatar

Jiří Beneš jiribenes

View GitHub Profile
cgsdev0 /
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
AndrasKovacs /
Last active May 29, 2024 02:20
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

neel-krishnaswami /
Last active September 6, 2023 13:43
A linear-time parser combinator library in Ocaml
module C : sig
type t
val empty : t
val one : char -> t
val union : t -> t -> t
val inter : t -> t -> t
val top : t
val mem : char -> t -> bool
val make : (char -> bool) -> t
val equal : t -> t -> bool
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
AndrasKovacs / NbESharedQuote.hs
Last active May 10, 2024 07:34
NbE with implicit sharing in quotation
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:
"A simple and efficient implementation of strong call by need by an abstract machine"
This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.
brendanzab /
Last active September 13, 2022 06:12
Elaboration with Singletons and Record patching
(** {0 Elaboration with Record Patching and Singleton Types}
This is a small implementation of a dependently typed language with
dependent record types, with some additional features intended to make it
more convenient to use records as first-class modules. It was originally
ported from {{:}
a gist by mb64}.
The type system is implemented in terms of an ‘elaborator’, which type
checks and tanslates a user-friendly surface language into a simpler and
mb64 /
Last active November 7, 2023 16:26
Bidirectional typechecking for higher-rank polymorphism in OCaml, without polymorphic subtyping
(* Compile with:
$ ocamlfind ocamlc -package angstrom,stdio -linkpkg -o tychk
Example use:
$ ./tychk <<EOF
> let f = (fun x -> x) : forall a. a -> a
> in f f
input : forall a. a -> a
sjoerdvisscher / CalcComp.hs
Created August 25, 2021 12:20
Calculating Dependently-Typed Compilers
{-# LANGUAGE GADTs, DataKinds, TypeOperators, TypeFamilies, TypeApplications, KindSignatures, ScopedTypeVariables #-}
import Control.Applicative
import Data.Kind
import Data.Type.Equality
type family (a :: Bool) || (b :: Bool) :: Bool where
'False || b = b
'True || b = 'True
robrix / FoldsAndUnfolds.hs
Created March 31, 2021 22:44
Recursion schemes over lists, in contrast with foldr/unfoldr
module FoldsAndUnfolds where
import Data.List -- for unfoldr
class Functor f => Recursive f t | t -> f where
project :: t -> f t
cata :: (f a -> a) -> t -> a
cata alg = go where go = alg . fmap go . project

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) = {