myuon’s gists

myuon / StateBench.hs

Last active August 29, 2015 14:05

benchmark

	{-# LANGUAGE FlexibleContexts, TypeOperators #-}
	import qualified Control.Monad.State.Strict as SS
	import qualified CState as CS
	import qualified Control.Eff.State.Strict as ES
	import Criterion.Main
	import Control.Monad
	import Control.Monad.State.Class
	import Data.Functor.Identity
	import Control.Eff
	import Data.Typeable

myuon / While.hs

Created August 27, 2014 10:02

https://www.hackerrank.com/challenges/while-language-fp

	import Control.Applicative
	import Control.Monad.State
	import Text.ParserCombinators.Parsec hiding ((<\|>), State)
	import qualified Data.Map as M

	data OpA = (:+:) \| (:-:) \| (:*:) \| (:/:) deriving (Eq,Show)
	data OpB = And \| Or deriving (Eq,Show)
	data OpR = (:>) \| (:<) deriving (Eq,Show)
	newtype Var = Var String deriving (Eq,Ord,Show)
	data AExp = VarExp Var \| Numeral Integer \| ApplyA OpA AExp AExp

myuon / q.hs

Created September 21, 2014 05:38

Q

	{-# LANGUAGE ExistentialQuantification, PackageImports #-}
	{-# LANGUAGE GeneralizedNewtypeDeriving #-}
	import Control.Applicative
	import Text.Trifecta
	import "mtl" Control.Monad.State
	import qualified Data.Map as M
	import Data.Monoid
	import Data.Ratio

	newtype Var = Var String deriving (Eq, Ord, Show)

myuon / H.v

Last active August 29, 2015 14:06

Monad of Identity, Maybe, List

	Require Import ssreflect.

	Class Monad (M : Type -> Type) :=
	{
	mreturn : forall {A}, A -> M A
	; mbind : forall {A B}, M A -> (A -> M B) -> M B

	; left_return : forall A B (a : A) (k : A -> M B), mbind (mreturn a) k = k a
	; right_return : forall A (m : M A), mbind m mreturn = m
	; composite : forall A B (m : M A) (k : A -> M A) (h : A -> M B),

myuon / Yoneda.v

Created October 2, 2014 12:10

To defined hom functor...?

	Require Import FunctionalExtensionality.

	Module Category.

	Axiom proof_irrelevance : forall (P : Prop) (u v : P), u = v.

	Reserved Notation "a ~> b" (at level 90).
	Reserved Notation "a o; b" (at level 45, right associativity).

	Class Category : Type :=

myuon / Yoneda.agda

Last active August 29, 2015 14:07

Yoneda Lemma

	module CatScratch where

	open import Function hiding (_∘_; id)
	open import Level
	open import Data.Product
	open import Relation.Binary
	open import Relation.Binary.Core using (_≡_)
	open import Relation.Binary.PropositionalEquality using (setoid)
	import Relation.Binary.EqReasoning as EqR
	import Relation.Binary.SetoidReasoning as SetR

myuon / set.agda

Created October 12, 2014 11:51

no good

myuon / Set-2.agda

Last active September 17, 2015 02:43

	infix 4 _∈_ _∉_
	data _∈_ {f} {A : Set f} (x : A) (B : Set f) : Set (suc f) where
	in-eq : A ≡ B → x ∈ B

	_∉_ : {B : Set} → B → Set → Set₁
	X ∉ A = (X ∈ A) → ⊥

	module elem-lemmas where
	elem-∈ : {A B : Set} → ∀{x : B} → x ∈ A → A
	elem-∈ {x = x} (in-eq ≡-refl) = x

myuon / Codensity.agda

Last active August 29, 2015 14:08

http://myuon-myon.hatenablog.com/entry/2014/11/03/183032

	module Codensity where

	open import Level
	open import Function
	open import Category.Functor
	open import Category.Monad
	open import Relation.Binary.PropositionalEquality

	record Functor {a b} (F : Set a → Set b) : Set (suc (a ⊔ b)) where
	field

myuon / CommRing.thy

Created November 7, 2014 01:53

	import Control.Applicative
	import Control.Monad.State
	import Text.ParserCombinators.Parsec hiding ((<\|>), State)
	import qualified Data.Map as M

	data OpA = (:+:) \| (:-:) \| (:*:) \| (:/:) deriving (Eq,Show)
	data OpB = And \| Or deriving (Eq,Show)
	data OpR = (:>) \| (:<) deriving (Eq,Show)
	newtype Var = Var String deriving (Eq,Ord,Show)
	data AExp = VarExp Var \| Numeral Integer \| ApplyA OpA AExp AExp

myuon myuon