public

PatternCinnamons.hs

ownermangoivcreated17.09.2024uuidec04b5d7-be15-4296-9557-0e22f736b4dc
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeAbstractions #-}
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall -Wno-unrecognised-pragmas -fno-show-error-context #-}

module PatternCinnamons where

import Data.Char
import Data.Dynamic

type data N = Z | S N

data SN (n :: N) where SZ :: SN Z; SN :: SN n -> SN (S n)

data V (n :: N) a where
  Nil :: V Z a
  (:::) :: a -> V n a -> V (S n) a

pattern SV :: forall n a. forall. n ~ S Z => a -> V n a
pattern SV a <- a ::: Nil
  where
    SV a = a ::: Nil

x :: V n a -> SN n
x = \case
  Nil -> SZ
  SV _ -> (SN SZ)
  (_ ::: xs) -> SN (x xs)

pattern TypeIs :: forall b. Typeable b => forall a. a ~ b => a -> Dynamic
pattern TypeIs x <- (fromDynamic -> Just x)
  where
    TypeIs a = toDyn a

-- >>> y (toDyn False)
-- 0
-- >>> y (TypeIs (4 :: Int))
-- 4
-- >>> y (toDyn (Just 'x'))
-- 120
-- >>> y (toDyn (Nothing :: Maybe Char))
-- 9
-- >>> y (toDyn True)
-- 2
y :: Dynamic -> Int
y = \case
  TypeIs @Int a -> a
  TypeIs @Bool True -> 2
  TypeIs @(Maybe Char) (Just c) -> ord c
  TypeIs @(Maybe Char) Nothing -> 9
  _ -> 0
public

jobQ.hs

ownermangoivcreated07.09.2024uuid8fa0d4af-8db5-4af6-b334-6a39b1d0a77d
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}

module Main where

import UnliftIO
import UnliftIO.Concurrent

-- | @'pooledConcurrentlyCatchN' n jobs@ enqueues @n@ jobs at a time and returns a (potentially unordered) list of
-- results of these jobs running to end
pooledConcurrentlyCatchN :: (MonadUnliftIO m) => Int -> [m a] -> m [Either SomeException a]
pooledConcurrentlyCatchN n jobs = do
  sem <- newQSem n
  go sem [] jobs
 where
  go _ acc [] = traverse waitCatch acc
  go sem acc (job : jobs) = do
    as <- do
      waitQSem sem
      async do
        job `finally` signalQSem sem
    go sem (as : acc) jobs

-- | like 'pooledConcurrentlyCatchN' but rethrows the first exception to occur after running all jobs to end
pooledConcurrentlyN :: (MonadUnliftIO m) => Int -> [m a] -> m [a]
pooledConcurrentlyN n jobs =
  pooledConcurrentlyCatchN n jobs >>= traverse \case
    Left ex -> throwIO ex
    Right a -> pure a

-- | like 'pooledConcurrentlyCatchN' but uses exactly the amount of available capabilities
pooledConcurrentlyCatch :: (MonadUnliftIO m) => [m a] -> m [Either SomeException a]
pooledConcurrentlyCatch jobs = do
  caps <- getNumCapabilities
  pooledConcurrentlyCatchN caps jobs

-- | like 'pooledConcurrentlyN' but uses exactly the amount of available capabilities
pooledConcurrently :: (MonadUnliftIO m) => [m a] -> m [a]
pooledConcurrently jobs = do
  caps <- getNumCapabilities
  pooledConcurrentlyN caps jobs

-- example
main :: IO ()
main = do
  setNumCapabilities 2
  print =<< getNumCapabilities
  print =<< pooledConcurrentlyCatch (threads [n ^ 2 | n <- [10, 5, 1]])
 where
  threads = map \n -> do
    tid <- myThreadId
    let m = n * 100_000
    putStrLn (show tid <> ": sleeping " <> show m)
    threadDelay m
    putStrLn (show tid <> ": waking up")
    pure n
public

Eff.hs

ownermangoivcreated14.08.2024uuidad653409-2634-4c89-a57f-37f9cec670c4
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Algebra
import Control.Carrier.Reader
import Control.Monad (void)
import Control.Monad.IO.Class
import Data.Foldable (for_)
import Data.Kind
import UnliftIO

newtype LHEnv p = LHEnv {lhHandlers :: [p -> IO ()]}

data Log p m k where
  WithLogEnv :: (LHEnv p -> LHEnv p) -> m a -> Log p m a
  WriteLog :: p -> Log p m ()

withLogEnv :: (Has (Log p) sig m) => (LHEnv p -> LHEnv p) -> m a -> m a
withLogEnv f act = send (WithLogEnv f act)

writeLog :: (Has (Log p) sig m) => p -> m ()
writeLog i = send (WriteLog i)

newtype LogConcurrentlyC p m (a :: Type) = MkLogConcurrentlyC {runLogConcurrentlyC :: LHEnv p -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (LHEnv p) m

runLogConcurrently :: LHEnv p -> LogConcurrentlyC p m a -> m a
runLogConcurrently = flip runLogConcurrentlyC

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogConcurrentlyC p m) where
  alg hdl sig ctx = MkLogConcurrentlyC \env -> case sig of
    L (WithLogEnv f m) -> runLogConcurrently (f env) (hdl (m <$ ctx))
    L (WriteLog x) ->
      ctx <$ liftIO do
        void $ async $ forConcurrently_ env.lhHandlers \logger ->
          logger x
    R other -> alg (runLogConcurrently env . hdl) other ctx

newtype LogSyncC p m (a :: Type) = MkLogSyncC {runLogSyncC :: LHEnv p -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (LHEnv p) m

runLogSync :: LHEnv p -> LogSyncC p m a -> m a
runLogSync = flip runLogSyncC

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogSyncC p m) where
  alg hdl sig ctx = MkLogSyncC \env -> case sig of
    L (WithLogEnv f m) -> runLogSync (f env) (hdl (m <$ ctx))
    L (WriteLog x) ->
      ctx <$ liftIO do
        for_ env.lhHandlers \logger ->
          logger x
    R other -> alg (runLogSync env . hdl) other ctx

newtype LogRefC p m (a :: Type) = MkLogRefC {runLogRefC :: IORef [p] -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (IORef [p]) m

runLogRef :: (MonadIO m) => LogRefC p m a -> m ([p], a)
runLogRef act = do
  ref <- newIORef []
  res <- runLogRefC act ref
  logs <- reverse <$> readIORef ref
  pure (logs, res)

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogRefC p m) where
  alg hdl sig ctx = MkLogRefC \ref -> case sig of
    L (WithLogEnv _f m) -> runLogRefC (hdl (m <$ ctx)) ref
    L (WriteLog x) ->
      ctx <$ liftIO do modifyIORef ref (x :)
    R other -> alg (flip runLogRefC ref . hdl) other ctx
public

Corecords.hs

ownermangoivcreated19.07.2024uuid38f35132-d56e-4dbb-b705-ddb951da428b
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordUpdate #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Wno-unused-imports 
    -fno-show-error-context -fprint-explicit-kinds #-}

module Corecords where

import Data.Bool (Bool (True), bool)
import Data.Coerce (coerce)
import Data.Kind (Constraint, Type)
import Data.SOP (NP (..), Proxy (Proxy))
import GHC.TypeLits (Symbol)
import Prelude

type (:#) :: Type -> Symbol -> Type
newtype t :# s = Tag {unTag :: t}
  deriving stock (Eq, Ord, Show)

type NamedArgs :: Type -> [(Type, Symbol)]
type family NamedArgs f where
  -- we care about the arguents that have an annotation
  NamedArgs (typ :# s -> r) = '(typ, s) : NamedArgs r
  -- we don't care about the rest of the function
  NamedArgs (typ -> r) = NamedArgs r
  -- we have reached the tail which is not a function
  NamedArgs r = '[]

type RestOfFunction :: Type -> Type
type family RestOfFunction f where
  -- discard the named arg
  RestOfFunction (typ :# s -> r) = RestOfFunction r
  -- keep the unnamed args
  RestOfFunction (typ -> r) = typ -> RestOfFunction r
  -- reached the end
  RestOfFunction r = r

type family Snd tup where
  Snd '(a, b) = b

type family Fst tup where
  Fst '(a, b) = a

type Named :: (Type, Symbol) -> Type
newtype Named tup = MkNamed {unNamed :: Fst tup}

class RewriteToCurried a where
  collectNamedArgs :: a -> NP Named (NamedArgs a) -> RestOfFunction a

instance (RewriteToCurried r) => RewriteToCurried (typ :# s -> r) where
  collectNamedArgs f (x :* xs) = collectNamedArgs (f (coerce x)) xs

instance
  {-# OVERLAPPABLE #-}
  ( RewriteToCurried r
  , RestOfFunction (s -> r) ~ (s -> RestOfFunction r)
  , NamedArgs (s -> r) ~ NamedArgs r
  )
  => RewriteToCurried (s -> r)
  where
  collectNamedArgs f xs x = collectNamedArgs @r (f x) xs

instance
  {-# OVERLAPPABLE #-}
  ( NamedArgs r ~ '[] -- this is kinda suspicious, we don't need the fact that we're matching on Nil
  , RestOfFunction r ~ r
  )
  => RewriteToCurried r
  where
  collectNamedArgs f _ = f

type SetField :: Symbol -> Type -> [(Type, Symbol)] -> Constraint
class SetField name a xs | xs -> a name where
  setField' :: forall r. (NP Named xs -> r) -> a -> NP Named (Removed name a xs) -> r

type Removed :: Symbol -> Type -> [(Type, Symbol)] -> [(Type, Symbol)]
type family Removed name a xs where
  Removed name a '[] = '[]
  Removed name a ('(b, name) : xs) = xs
  Removed name a ('(b, other) : xs) = ('(b, other) : Removed name a xs)

instance {-# OVERLAPPING #-} (a ~ b) => SetField name a ('(b, name) : xs) where
  setField' f a xs = f (MkNamed a :* xs)

instance (SetField name a xs, Removed name a ('(b, other) : xs) ~ '(b, other) : Removed name a xs) => SetField name a ('(b, other) : xs) where
  setField' f a = \case
    (x :* xs) -> setField' @name @a @xs (\ys -> f (x :* ys)) a xs

class ExpandArgs xs r where
  type Expanded xs r :: Type
  expandArgs :: (NP Named xs -> r) -> Expanded xs r

instance ExpandArgs '[] r where
  type Expanded '[] r = r
  expandArgs f = f Nil

instance (ExpandArgs xs r) => ExpandArgs ('(typ, name) : xs) r where
  type Expanded ('(typ, name) : xs) r = typ :# name -> Expanded xs r
  expandArgs f n = expandArgs @xs @r \xs -> f (coerce n :* xs)

getField :: a
getField = undefined

setField
  :: forall name infn field
   . ( ExpandArgs (Removed name field (NamedArgs infn)) (RestOfFunction infn)
     , SetField name field (NamedArgs infn)
     , RewriteToCurried infn
     )
  => infn
  -> field
  -> Expanded (Removed name field (NamedArgs infn)) (RestOfFunction infn)
setField fn a = expandArgs (setField' @name (collectNamedArgs fn) a)

namedPlus3 :: Int -> Int :# "arg1" -> String -> Bool :# "arg2" -> Int :# "arg3" -> Int
namedPlus3 d a a' b c = fromIntegral $ unTag a + bool 42 69 (unTag b) - unTag c + length a' + d

np3 :: Int :# "arg1" -> Int -> [Char] -> Int
np3 = namedPlus3 {arg3 = 4, arg2 = True}

exp' :: Double :# "coefficient" -> Double :# "base" -> Int :# "exponent" -> Double
exp' a b x = unTag a * (unTag b ^ unTag x)

-- >>> ex
-- 65.7
ex :: Double
ex = exp' {base = 3, exponent = 2, coefficient = 7.3}
public

Parse.hs

ownermangoivcreated19.07.2024uuid6063831f-f1e7-4beb-9db6-52c7ecc94900
{-# LANGUAGE BlockArguments #-}

module Parse where

import Options.Applicative

main :: IO ()
main = do
  parsed :: Either () () <- execParser do
    let p = pure (Left ()) <|> subparser do command "bla" (info (pure (Right ())) briefDesc)
    info p briefDesc
  case parsed of
    Left _ -> putStrLn "no arg"
    Right _ -> putStrLn "had arg"
public

patch-neovim.nix

ownermangoivcreated17.05.2024uuidd98221a5-bc33-4ff9-b55f-a8011dd389a1
programs.neovim.package = pkgs.neovim-unwrapped.overrideAttrs (old: {
  patches = old.patches or [] ++ [
    (pkgs.fetchpatch {
      name = "strip-consecutive-white-spaces.patch"; 
      url = "https://github.com/mangoiv/neovim/commit/ea0a9163cb37e8444465b81abbed82c54134c12e.patch"; 
      hash = "sha256-LQwS+yJucin5AlXTPa3O95Zwjw4RerniPtNT8ctw0AU=";
    })
  ];
});
public

RecordUpdate.hs

ownermangoivcreated16.05.2024uuidf876d8ce-3a7a-4acf-9ce7-adb348d44b5b
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedRecordUpdate #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

module RecordUpdate where

import Data.Kind (Type)
import Data.Type.Bool (type (||))
import GHC.Generics
import GHC.TypeError (ErrorMessage (..), TypeError)
import GHC.TypeLits (Symbol)
import Prelude

class GHasField (name :: k) (recordRep :: Type -> Type) (field :: Type) | name recordRep -> field where
  gGetField :: recordRep a -> field
  gSetField :: recordRep a -> field -> recordRep a

--------------------------------------------------------------------------------
-- threading through constructors and type names
--------------------------------------------------------------------------------
instance (GHasField n k f) => GHasField n (C1 m k) f where
  gGetField = gGetField @_ @n . unM1
  gSetField x a = M1 $ gSetField @_ @n (unM1 x) a

instance (GHasField n k f) => GHasField n (D1 m k) f where
  gGetField = gGetField @_ @n . unM1
  gSetField x a = M1 $ gSetField @_ @n (unM1 x) a

--------------------------------------------------------------------------------
-- threading through sum and product
--------------------------------------------------------------------------------

-- this seems a bit wonky, perhaps could be improved
type IsInRemaining :: Symbol -> (Type -> Type) -> Bool
type family IsInRemaining n f where
  IsInRemaining n (k1 :*: k2) = CheckField n k1 || IsInRemaining n k2
  IsInRemaining n (M1 s m k) = CheckField n (M1 s m k)
  IsInRemaining n f = TypeError (Text "unexpected type " :<>: ShowType f :<>: Text "on lhs of IsInRemaining")

type CheckField :: Symbol -> (Type -> Type) -> Bool
type family CheckField n f where
  CheckField n (S1 (MetaSel (Just n) su ss l) a) = 'True
  CheckField n (S1 (MetaSel (Just n') su ss l) a) = 'False

class GHasField' b n t f | b n t -> f where
  gGetField' :: t a -> f
  gSetField' :: t a -> f -> t a

instance (GHasField n t f) => GHasField' False n (t :*: r) f where
  gGetField' (l :*: _r) = gGetField @_ @n l
  gSetField' (l :*: r) f = gSetField @_ @n l f :*: r

instance (GHasField n r f) => GHasField' True n (t :*: r) f where
  gGetField' (_l :*: r) = gGetField @_ @n r
  gSetField' (l :*: r) f = l :*: gSetField @_ @n r f

instance (GHasField' (IsInRemaining n r) n (t :*: r) f) => GHasField n (t :*: r) f where
  gGetField = gGetField' @(IsInRemaining n r) @n
  gSetField = gSetField' @(IsInRemaining n r) @n

--------------------------------------------------------------------------------
-- we want a nice error message if that didn't work out
--------------------------------------------------------------------------------
instance GHasField n (S1 (MetaSel (Just n) su ss l) (K1 i f)) f where
  gGetField = unK1 . unM1
  gSetField _x a = M1 $ K1 a

--------------------------------------------------------------------------------
-- the actual definitions
--------------------------------------------------------------------------------
getField :: forall {k} (name :: k) (record :: Type) (field :: Type). (Generic record, GHasField name (Rep record) field) => record -> field
getField rec = gGetField @k @name @(Rep record) @field (from @record rec)

setField :: forall {k} (name :: k) (record :: Type) (field :: Type). (Generic record, GHasField name (Rep record) field) => record -> field -> record
setField r = to . gSetField @k @name @(Rep record) @field (from r)

data A = MkA {b :: Bool, a :: Int}
  deriving stock (Eq, Ord, Show, Generic)

data B = MkB {b :: Bool, c :: Int, a :: Int}
  deriving stock (Eq, Ord, Show, Generic)

u :: B -> Int -> B
u a i = a {a = i}
public

GCurry.hs

ownermangoivcreated12.05.2024uuid36aaec4f-d579-45d0-8849-055f5c60085e
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module GCurry where

import Data.Kind (Type)
import Generics.SOP
import Prelude hiding (curry)

-- >>> curry (\(x, y, z) -> x + y + z) 5 6 7
-- 18
curry :: forall a xs b. (Generic a, Code a ~ '[xs]) => (a -> b) -> Curry xs b
curry f = mk (f . to . SOP . Z)
 where
  mk :: forall ys. (All Top ys) => (NP I ys -> b) -> Curry ys b
  mk g = case sList @ys of
    SNil -> g Nil
    SCons -> \x -> mk \rest -> g (I x :* rest)

type family Curry xs b where
  Curry '[] b = b
  Curry (x : xs) b = x -> Curry xs b
public

CheckInitialized.hs

ownermangoivcreated12.05.2024uuid690dda75-fc21-43ff-8c05-bca3f6a0e666
module CheckInitialized where

import Data.IORef
import System.IO.Unsafe (unsafePerformIO)

doInit :: IO ()
doInit = putStrLn "initializing"

{-# NOINLINE initStatus #-}
initStatus :: IORef Bool
initStatus = unsafePerformIO (newIORef False)

checkInit :: IO ()
checkInit = do
  initialized <- readIORef initStatus
  if initialized
    then putStrLn "already initialized"
    else doInit *> writeIORef initStatus True

-- this is some function in libsodium-bindings
fn :: IO ()
fn = do
  checkInit
  -- do something else

-- this is some downstream program using the bindings
main :: IO () 
main = do 
  fn 
  fn 
  fn