Skip to content

Instantly share code, notes, and snippets.

Avatar

日比野 啓 (Kei Hibino) khibino

View GitHub Profile
@khibino
khibino / MetaTheory.agda
Last active Oct 17, 2020
Meta-Theory à la Carte using Agda
View MetaTheory.agda
-- Example implementation for Meta-Theory à la Carte
-- data Fix (f : Set -> Set) : Set where
-- inF : f (Fix f) -> Fix f
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat
View galaxy.hs
f1029 = [7, 123229502148636]
f1030 = [2, 7]
f1031 = [4, 21855]
f1032 = [7, 560803991675135]
f1034 = [5, 33554431]
View 2natlist.hs
import Numeric.Natural (Natural)
type Nat = Natural
data NatListF a = Nil | Cons (Nat, a) deriving Show
newtype NatList = In (NatListF NatList) deriving Show
out :: NatList -> NatListF NatList
out (In x) = x
View CoYoneda.agda
module CoYoneda where
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Data.Product using (_×_; proj₁; proj₂; ∃; _,_)
pattern _⊢_⊗_ a k x = (a , k , x) -- ∃ (λ a → (a → r) × f a)
module CovariantMap
@khibino
khibino / Yoneda.agda
Last active Nov 19, 2019
Yoneda's Lemma under Haskell like Functor
View Yoneda.agda
module Yoneda where
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_)
{- 射を Haskell の関数に、
関手を Haskell の Functor に限定した場合の
米田の補題の証明 -}
@khibino
khibino / WithPlaceholder.hs
Created May 10, 2019
with placeholder example
View WithPlaceholder.hs
{-# LANGUAGE FlexibleInstances #-}
import Data.DList
import Control.Monad.Trans.Writer (Writer)
import Data.Functor.ProductIsomorphic
data PH a = PH
newtype WithPhT r a =
WithPhT { runWithPhT :: Writer (DList Int) (r a) }
View IpState.agda
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import RSC
-- Basic data-types
View Position.hs
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
module Position where
import GHC.Generics (Generic)
import Foreign.Ptr (Ptr )
import Data.Word (Word8)
View report.txt
Debian sid 上の groonga 8.0.2 および Debian jessie 上の groonga 8.0.1 で実験しました。
groonga に投入するクライアントプログラムを中断すると、
それとは関係のない別のクライアントで、JSON の解釈エラーが返ることがある問題があるようです。
問題を再現するスクリプト run.sh を作ることに成功したのでここに貼ります。
( 後輩の前角さんが協力してくれました。ありがとうございます。 )
実行に必要な Debian package は、
groonga, curl です。
run.sh を実行すると、
@khibino
khibino / name-config.hs
Created Mar 19, 2018
Name configuration example of Haskell Relational Record
View name-config.hs
import Language.Haskell.TH (nameBase)
import Language.Haskell.TH.Name.CamelCase (varCamelcaseName, varName)
import Database.Record.TH
customConfig :: NameConfig
customConfig =
defaultNameConfig
{ columnName = \tbl col -> varCamelcaseName $ tbl ++ "_" ++ col }
main :: IO ()