Skip to content

Instantly share code, notes, and snippets.

Avatar
🏠
Working from home

Hiromi Ishii konn

🏠
Working from home
View GitHub Profile
View line-breaks-in-proof-stdja.saty
@require: stdjareport
@require: math
document (|
title = {あああああ};
author = {mr_konn};
date = {2022/04/23};
|) '<
+chapter{あああああ}<
+proof{
ううううううう
View stack-verbose.log
$ stack ghci --verbose
Version 2.5.1, Git revision d6ab861544918185236cf826cb2028abb266d6d5 x86_64 hpack-0.33.0
2021-01-29 22:44:07.844116: [debug] Checking for project config at: /Users/hiromi/Documents/Programming/Haskell/git/hls-conditional-modules/stack.yaml
2021-01-29 22:44:07.844573: [debug] Loading project config file stack.yaml
2021-01-29 22:44:07.849169: [debug] (SQL) SELECT COUNT(*) FROM "last_performed" WHERE ("action"=?) AND ("timestamp">=?); [PersistInt64 1,PersistUTCTime 2021-01-28 13:44:07.849126 UTC]
2021-01-29 22:44:07.850659: [debug] Using package location completions from a lock file
2021-01-29 22:44:07.852246: [debug] Loaded snapshot from Pantry database.
2021-01-29 22:44:08.007014: [debug] RawSnapshotLayer {rslParent = RSLCompiler (WCGhc (mkVersion [8,10,3])), rslCompiler = Nothing, rslLocations = [RPLIHackage AC-Angle-1.0@sha256:e1ffee97819283b714598b947de323254e368f6ae7d4db1d3618fa933f80f065,544 (Just (TreeKey 7edd1f1a6228af27c0f0ae53e73468c1d7ac26166f2cb386962db7ff021a2714,210)),RPLIHa
@konn
konn / JSaddleCompat.hs
Last active Oct 4, 2020
JSaddle (Miso) and custom Backend Server, running on the same host & port
View JSaddleCompat.hs
{-# LANGUAGE DuplicateRecordFields, OverloadedStrings, RecordWildCards #-}
module JSaddleCompat (runApp, App(..)) where
import qualified Language.Javascript.JSaddle.Warp as JSaddle
import Miso (startApp, syncPoint)
import qualified Miso as Miso
import Network.HTTP.Client.Conduit (Manager, newManager)
import Network.HTTP.ReverseProxy (WaiProxyResponse (..),
defaultOnExc, waiProxyTo)
import Network.Wai (Application, pathInfo)
import qualified Network.Wai.Handler.Warp as Warp
View HKDOpts.hs
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, PolyKinds #-}
{-# LANGUAGE RankNTypes, RecordWildCards, StandaloneDeriving, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Lib where
import Data.Functor.Identity
import Options.Applicative
someFunc :: IO ()
someFunc = putStrLn "someFunc"
View Explosion.hs
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs, DeriveDataTypeable, TypeApplications #-}
data Foo (a :: Maybe b) where { Any :: Foo a; Bang :: Foo (Just t) }
newtype F a (t :: Maybe s) (u :: Foo t)
= F { runF :: a} deriving (Show, Eq, Ord, Typeable)
main :: IO ()
main = print $ typeRep $ Proxy @(F Int ('Just ()) Any)
-- ~> No instance for (Typeable (F2 Int ('Just ())))
@konn
konn / monoid.prl
Created Nov 8, 2018
Monoids in RedPRL
View monoid.prl
define IsSemigroup(#ty, #mul) =
(record
[assoc:
(->
[a b c: #ty]
(= #ty
($ #mul a ($ #mul b c))
($ #mul ($ #mul a b) c)
)
)
View ConstraintUnion.hs
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms, RankNTypes, ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies, TypeOperators, TypeSynonymInstances #-}
module ConstraintUnion where
import Data.Kind
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Ord
import Data.Type.Equality
import GHC.TypeNats
@konn
konn / lib.rs
Last active Aug 29, 2018
Type-level Peano numerals and sized vectors in Rust (Just for fun)
View lib.rs
use std::marker::PhantomData;
pub trait Nat {
type Eval;
fn as_int() -> usize;
}
#[derive(Debug)]
pub struct Zero {}
@konn
konn / cacher.rs
Last active Aug 17, 2018
Generic Cacher without Clone
View cacher.rs
use std::collections::hash_map::Entry;
use std::collections::HashMap;
use std::hash::Hash;
use std::ops::Fn;
struct Cacher<'a, T, A, B>
where
T: 'a + Fn(&A) -> B,
A: 'a,
B: 'a,
@konn
konn / Cell.hs
Created Jul 18, 2018
Akari (美術館) Solver using SAT solvers
View Cell.hs
{-# LANGUAGE DeriveAnyClass, DeriveDataTypeable, DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies, FlexibleInstances, MultiWayIf #-}
{-# LANGUAGE TypeFamilies #-}
module Cell where
import Control.Applicative (empty)
import Data.Typeable (Typeable)
import Data.Word
import Ersatz
import GHC.Generics (Generic)