{{ message }}

Instantly share code, notes, and snippets.

日比野 啓 (Kei Hibino) khibino

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
Last active Aug 1, 2020
View galaxy.hs
 f1029 = [7, 123229502148636] f1030 = [2, 7] f1031 = [4, 21855] f1032 = [7, 560803991675135] f1034 = [5, 33554431]
Last active Jun 27, 2020
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
Last active Nov 24, 2019
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
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 に限定した場合の 米田の補題の証明 -}
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) }
Last active Aug 21, 2018
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
Created Jun 29, 2018
View Position.hs
 {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} module Position where import GHC.Generics (Generic) import Foreign.Ptr (Ptr ) import Data.Word (Word8)
Last active May 28, 2018
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 を実行すると、
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 ()