qexat’s gists

qexat / Nilable.ml

Last active November 14, 2025 21:21

this is the future jane street wants. #NoToNil #protest #Option4Ever #foryou #foryoupage

	type nil = Nil

	(* This version is unsafe because it makes the assumption that index >= 0. *)
	let rec get_unsafe : 'a. at:int -> from:'a list -> 'a \| nil =
	fun ~at:index ~from:list ->
	match list with
	\| [] -> Nil
	\| first :: _ when index = 0 -> first
	\| _ :: rest -> get_unsafe ~at:(index - 1) ~from:rest

qexat / substruct.ml

Last active November 1, 2025 13:35

	(* -- Interfaces -- *)

	module type ORDERED = sig
	type ('a, 'b) t
	end

	module type LINEAR = sig
	include ORDERED

	val exchange : 'a 'b. ('a, 'b) t -> ('b, 'a) t

qexat / deez_nats.py

Created October 31, 2025 11:06

oh my god lexa will you ever stop defining peano integers in every language on earth a thousand times AND differently every time like seriously im starting to get worried for your mental health i mean what even is your goal with that what do you gain from it because i dont see it and look im not trying to be dismissive or anything but you could …

	import enum
	import typing

	class Nat(enum.Enum):
	O = enum.auto()
	S = enum.auto()

	type nat = typing.Literal[Nat.O] \| tuple[typing.Literal[Nat.S], nat]

	O = Nat.O

qexat / Hoskaml.ml

Last active October 26, 2025 11:33

mmm... perform_io...

	module Util = struct
	let ( let*? ) = Option.bind
	let ( let*! ) = Result.bind
	let ( let@ ) = ( @@ )
	let ( *> ) f g x = g (f x)
	let curry = ( @@ )
	let curry2 f a b = f (a, b)
	let curry3 f a b c = f (a, b, c)
	let ( let\|> ) a k = a (curry k)
	let ( let\|\|> ) a k = a (curry2 k)

qexat / Or_gadt.ml

Created October 16, 2025 11:31

disjunction funsies with GADTs

	type left = private Left_tag
	type right = private Right_tag

	type ('ctr, 'left, 'right) t =
	\| Left : 'a 'b. 'a -> (left, 'a, 'b) t
	\| Right : 'a 'b. 'b -> (right, 'a, 'b) t

	let introduction_left : type a b. a -> (left, a, b) t =
	fun a -> Left a

qexat / ramblings.hs

Created October 7, 2025 07:45

functor ramblings in pseudo-haskell. unfortunately perfect parsing requires multicategories

	e ::= x
	\| '(' e ')'
	\| e e
	\| 'λ' x '.' e
	---------------------------------------------------------------
	_&>_ a b = a ∧ (a → b)

	or_elim = (a → c) → (b → c) → a ∨ b → c
	or_elim f _ (Left a) = f a
	or_elim _ g (Right b) = g b

qexat / README.md

Created September 26, 2025 07:21

static verification of equality in python! try it on a typechecker like pyright

use it in pyright: playground link

qexat / safeCoerce.hs

Created September 21, 2025 13:42

	{-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE UndecidableSuperClasses #-}

	import Data.Kind

	class (c a, c b) => SafeCoercible (c :: Type -> Constraint) a b \| c a -> b where
	safeCoerce :: a -> b

	instance SafeCoercible Num Int Float where

qexat / the_bug_fix_workflow.txt

Last active August 27, 2025 15:21

the bug fix workflow, using ribbon's project version control system

	%%%%%%%%%%%%%%%%%%%%%%%%
	% the bug fix workflow %
	%%%%%%%%%%%%%%%%%%%%%%%%

	=========================
	what does a bug fix have?
	=========================

	-> a name that can be referenced
	-> a description to use in commit & release

qexat / Refl.ml

Created August 21, 2025 18:07

equality and its negation!

	module False = struct
	(** This empty type represents falsehood. No proof (term) of
	it exists. *)
	type t = \|

	(** [ex_falso_quodlibet] states that if we have the proof of
	falsehood, then we can prove anything. *)
	let ex_falso_quodlibet : 'a. t -> 'a = function
	\| _ -> .
	end

lexa qexat