Skip to content

Instantly share code, notes, and snippets.

View viercc's full-sized avatar

Koji Miyazato viercc

17 followers · 8 following
View GitHub Profile
@viercc
viercc / DistAct.hs
Last active August 22, 2026 12:16
Distributive law for Act comonad
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE BlockArguments #-}
module DistAct where
import Data.Functor ((<&>))
import Control.Comonad
import Control.Comonad.Store (Store)
import qualified Control.Comonad.Store as Store
@viercc
viercc / FFreeDup.hs
Created June 12, 2026 01:38
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE UndecidableInstances #-}
module FFreeDup where
import Data.Bifunctor
import Control.Monad (ap)
type f ~> g = forall x. f x -> g x
@viercc
viercc / abc070-killer.hs
Created March 30, 2025 05:54
Generate (somewhat hard) test cases for ABC070 D
-- Generate (somewhat hard) test cases for ABC070 D
-- https://atcoder.jp/contests/abc070/tasks/abc070_d
module Main (main) where
type Input = (Int, [(Int, Int, Int)], Int, [(Int, Int)])
main :: IO ()
main = do
writeInputTo "abc070-d-10k-path.txt" (largePathGraph 10000)
writeInputTo "abc070-d-20k-path.txt" (largePathGraph 20000)
@viercc
viercc / from-cofree.md
Last active June 25, 2026 12:17

Note: Calculation on types

Goal

Let DD be the following type.

type DD = forall w. Comonad w => w A -> w B
@viercc
viercc / proof.md
Last active December 9, 2024 15:35
My PGP fingerprint

openpgp4fpr:B2E1DC9AF16599BD2D873A227BABC58075EC4EE6

@viercc
viercc / coyoneda-dinat.md
Created July 8, 2024 10:47 
type A :: Type
type X :: Type
type F :: Type -> Type
instance Functor F

p :: forall x. (F x, x -> A) -> X

newtype H a = H { runH :: (a -&gt; A) -&gt; X }
@viercc
viercc / sequenceA-eq-distribute.md
Last active October 20, 2024 02:24
sequenceA == distribute?

https://twitter.com/lotz84_/status/1787796266484908211

lotz @lotz84_

これを書いていて Vector n a 同士の sequenceA が distribute のように振る舞うのが気になった👀 一般に Traversable の distribute が Distributive の sequenceA に一致することが則を使って言えないだろうか？🤔 QuickCheck で少し探してみたけど反例はなさそう

大枠

@viercc
viercc / Isomorphisms2.hs
Created March 5, 2024 10:53
-- Overkilling a cute li'l exercise
-- https://www.reddit.com/r/haskell/comments/v0mfkl/cute_lil_exercise/
{-# LANGUAGE UnicodeSyntax, TypeOperators, ScopedTypeVariables, RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- (this time without ImpredicativeTypes, but I'm not sure it's better or not)
module Isomorphisms2(goal, to, from) where
import Prelude hiding (id, (.))
import Control.Category
@viercc
viercc / functioncapture.hs
Created February 23, 2024 06:53
-- https://twitter.com/mi12cp/status/1753203763211571656
-- https://twitter.com/rsk0315_h4x/status/1753233137629646938
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Data.IORef
-- trait Fn()
@viercc
viercc / PolymorphicState.hs
Last active December 24, 2023 09:20
{-# LANGUAGE RankNTypes #-}
module PolymorphicState where
{-
-- https://twitter.com/Kory__3/status/1737757423673413635
> forall s, a. Monad (a =>> s -> (s, a)) の値って一意なのでしょうか
-}