Skip to content

Instantly share code, notes, and snippets.

View L-as's full-sized avatar

Las L-as

111 followers · 14 following
View GitHub Profile
@L-as
L-as / Sound_lazy.hs
Last active July 7, 2025 20:11
Haskell version of Oleg Kiselyov's sound_lazy.ml from https://okmij.org/ftp/ML/generalization.html rewritten mechanically, big differences being much of the code here is lazy, we use STRef, and global variables are put into a record.
{-# LANGUAGE GHC2021, NamedFieldPuns, LambdaCase, RebindableSyntax, RecordWildCards, BlockArguments, MagicHash #-}
{-# OPTIONS_GHC -Wall -Wno-name-shadowing -Wno-missing-signatures #-}
module Sound_lazy where
import Data.STRef
import Control.Monad.ST
import Prelude hiding (negate)
import Data.Char
import Control.Monad
@L-as
L-as / Sorted.hs
Created July 6, 2025 00:26
{-# LANGUAGE GHC2021, TypeData, GADTs, UndecidableInstances #-}
module Sorted where
data SortedList a rel head where
SortedNil :: SortedList a rel top
SortedCons :: rel x top -> a x -> SortedList a rel top -> SortedList a rel x
class Rel rel x y where
rel :: rel x y
@L-as
L-as / type_arith.idr
Created July 2, 2025 18:33
(+) : Type -> Type -> Type
a + b = Either a b
record Iso (a : Type) (b : Type) where
constructor MkIso
to : a -> b
from : b -> a
leftInv : (x : a) -> from (to x) = x
rightInv : (y : b) -> to (from y) = y
@L-as
L-as / seccomp-tioscti-filter.c
Created May 2, 2024 10:55
#include <unistd.h>
#include <stdio.h>
#include <stdlib.h>
#include <seccomp.h>
#include <linux/seccomp.h>
#include <poll.h>
#include <sched.h>
#include <pwd.h>
#include <grp.h>
#include <sys/mount.h>