Skip to content

Instantly share code, notes, and snippets.

View jiribenes's full-sized avatar

Jiří Beneš jiribenes

View GitHub Profile
@AndrasKovacs
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"
https://dl.acm.org/doi/10.1145/3549822
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.
@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
@neel-krishnaswami
neel-krishnaswami / pcomb.ml
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
AndrasKovacs / ZeroCostGC.md
Last active May 16, 2024 12:19
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