Hidenori Azuma as-capabl

as-capabl / 1-intro.hs

Last active August 29, 2015 14:02

	{-# Language Arrows #-}

	import Control.Arrow
	import Control.Monad (forever)
	import Control.Monad.Trans (lift)
	import qualified Control.Arrow.Machine as P
	import qualified Data.Machine as Mc
	import Data.Machine ((<~))

as-capabl / objpipe.hs

Last active August 29, 2015 14:13

	{-# Language GADTs #-}
	{-# Language RankNTypes #-}
	{-# Language TypeOperators #-}
	{-# Language GeneralizedNewtypeDeriving #-}
	{-# Language MultiParamTypeClasses #-}
	{-# Language FlexibleInstances #-}
	{-# Language LambdaCase #-}

	module
	Main

as-capabl / freemonoid.v

Created March 1, 2015 10:36

List as free monoid.

	Require Import List.

	Section Monoid.
	Class Monoid {A:Type} (dot : A -> A -> A) (unit : A) : Prop :=
	{
	dot_assoc :
	forall x y z:A,
	dot x (dot y z) = dot (dot x y) z;
	unit_left :
	forall x, dot unit x = x;

as-capabl / filter.hs

Last active August 29, 2015 14:18

A filter implementation on objective

as-capabl / benchmark.hs

Last active August 29, 2015 14:18

	{-# LANGUAGE Arrows #-}

	module Main where

	import Prelude hiding (filter, id, (.), unzip, mapM_)
	import Control.Category
	import Control.Arrow
	import Criterion
	import Criterion.Main (defaultMain)
	import Data.Time

as-capabl / ReaderTImpl.v

Created June 27, 2016 13:17

やりたいこと：Coq上でReaderTを実装し、Haskellコードに変換してHaskell側から使う

	(* やりたいこと：Coq上でReaderTを実装し、
	Haskellコードに変換してHaskell側から使う *)
	Require Import Coq.Logic.FunctionalExtensionality.

	Section Monad_Definition.
	(* Reserved Notation "c >>= f"
	(at level 42, left associativity). *)

	(* Monadの宣言 *)
	Class Monad {T : Type -> Type} (returns : forall {A : Type}, A -> T A)

as-capabl / simplex_category.v

Created January 16, 2017 15:21

Simplex Category


	Require Import Relation_Definitions.
	Require Import SetoidClass.
	Require Import VectorDef.
	Require Import Morphisms.
	Require Import COC.Base.Main.


	Set Implicit Arguments.

as-capabl / lens-prism.hs

Created February 21, 2017 08:59

LensとPrismで解きたい問題

	-- 与えるもの：あるレコード型とその上のLens
	data Hoge = Hoge { _hoge1 :: ..., _hoge2 :: ..., ... }
	makeLenses ''Hoge -- hoge1, hoge2, ...が定義される

	-- ↓ ここからTemplate Haskellで生成するか、あるいは...

	-- 欲しいもの1：直和型とその上のPrism
	data CoHoge = CoHoge1 ... \| CoHoge2 ...
	makePrisms ''CoHoge -- _CoHoge1, _CoHoge2, ...が定義される
	-- CoHogeのコンストラクタはなくてもいい。型とPrismが必要

as-capabl / builder.hs

Created May 10, 2017 03:10

Writerっぽくリスト作れて、遅延評価とかfoldr/buildとか効くヤツ

	module Main where

	import Control.Monad.Free.Church
	import GHC.Exts (build)
	import Control.Monad (forever)

	type Builder b = F ((,) b)

	putB :: b -> Builder b ()
	putB x = liftF (x, ())

as-capabl / sumeven.hs

Created August 4, 2017 03:54