Skip to content

Instantly share code, notes, and snippets.

View msakai's full-sized avatar

Masahiro Sakai msakai

281 followers · 265 following
View GitHub Profile
@msakai
msakai / LinearDistributivity.als
Created November 14, 2024 00:11
sig E {
join, meet : E -> one E
}
one sig top, bot in E {}
fact {
all x, y, z : E {
-- commutativity
x.join[y] = y.join[x]
x.meet[y] = y.meet[x]
@msakai
msakai / ExtendedGroup.agda
Last active October 22, 2024 14:40
体 F が x + y = 1 かつ x y = 1 を満たすような元を持たない時、F ∪ {∞} は演算 x ⊛ y := (x y - 1) / (x + y - 1) に関して群になる
{-
体 F が x + y = 1 かつ x y = 1 を満たすような元を持たない時、F ∪ {∞} は
∞ ⊛ y = y
x ⊛ ∞ = x
x ⊛ y = (x y - 1) / (x + y - 1) if x + y ≠ 1
x ⊛ y = ∞ otherwise
で定義される演算によって群となる。
@msakai
msakai / Bug.hs
Last active July 7, 2024 16:20
GHC 9.6.6 fails with lookupIdSubst panic
module Bug where
import Control.Monad.Primitive
import qualified Data.HashTable.ST.Basic as H
data Symbol a = Symbol
data Node s a = Node
data Rule s a = Rule (Node s a)
@msakai
msakai / CohensKappa.hs
Last active June 8, 2024 16:36
module CohensKappa where
import Data.Hashable
import qualified Data.HashMap.Strict as HashMap
-- | Cohen's kappa coefficient (κ)
--
-- https://en.wikipedia.org/wiki/Cohen%27s_kappa
cohensKappa :: (Hashable c, Fractional a) => [(c,c)] -> a
cohensKappa xs = (po - pe) / (1 - pe)
@msakai
msakai / mypy_dependent_type.py
Created June 5, 2024 03:04
from typing import Literal, Optional, Tuple, overload
@overload
def f(with_extra_info: Literal[False]) -> Tuple[int, int]: ...
@overload
def f(with_extra_info: Literal[True]) -> Tuple[int, int, str]: ...
# This overload is necessafy for type checking the last `f(with_extra_info)`.
@overload
@msakai
msakai / OkapiBM25.hs
Created December 16, 2023 17:05
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- https://en.wikipedia.org/wiki/Okapi_BM25
module OkapiBM25
( Database
, mkDatabase
, query
) where
@msakai
msakai / test_psycopg2_isolation_level.py
Last active November 26, 2023 03:22
import psycopg2
dsn = "postgresql://user:password@localhost:5432/"
db_name = "test_db"
conn = psycopg2.connect(dsn)
try:
conn.set_isolation_level(psycopg2.extensions.ISOLATION_LEVEL_AUTOCOMMIT)
with conn.cursor() as cur:
@msakai
msakai / turtle_loop_vs_nondet.hs
Created August 16, 2023 01:59
import Control.Monad
import Turtle
main :: IO ()
main = sh $
forM_ [(1::Int)..2] $ \i -> do
j <- select [(1::Int)..3]
liftIO $ print (i, j)
{-
@msakai
msakai / QueryInterface.hs
Created May 28, 2023 01:28
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module QueryInterface where
-- Maybe (GHC.Exts.DictBox a)
data QueryIntefaceResult a where
@msakai
msakai / RWLock.hs
Last active May 5, 2023 02:45
{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module : RWLock
-- Copyright : (c) Masahiro Sakai 2023
-- License : BSD-3-Clause
--
-- Simple implement of various variants of RWLocks.
--