notogawa’s gists

notogawa / JQ.hs

Created April 24, 2015 08:58

	{-# LANGUAGE FlexibleContexts #-}
	module Data.JQ where

	import Control.Applicative ( Applicative, (<$>), (<*>) )
	import Control.Monad ( (>=>) )
	import Control.Monad.Reader.Class
	import qualified Data.Aeson as JSON
	import qualified Data.Aeson.Types as JSON
	import qualified Data.HashMap.Strict as HM
	import Data.List ( foldl1' )

notogawa / Python.hs

Created June 4, 2015 15:58

Call Python interpreter from Haskell using inline-c

	{-# LANGUAGE QuasiQuotes #-}
	{-# LANGUAGE TemplateHaskell #-}
	{-# LANGUAGE OverloadedStrings #-}
	module Main where

	import qualified Language.C.Inline as C
	import Foreign.C.Types
	import Foreign.C.String

	C.include "python2.7/Python.h"

notogawa / Flatten.hs

Created August 21, 2015 13:13

https://twitter.com/keizo_bookman/status/634688932916035584 これ?

	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
	module Flatten (flatten) where

	import Control.Monad

	class Flatten m x a where
	flatten :: x -> m a
	instance Monad m => Flatten m (m a) a where
	flatten = id

notogawa / uniq.agda

Last active August 31, 2015 00:35

	-- uniqコマンド
	--
	-- $ agda -c -i. -i/usr/share/agda-stdlib/ uniq.agda
	-- $ ./uniq
	--
	module uniq where

	module PartialityStream where

	open import IO using (IO; return; _>>=_)

notogawa / Dockerfile

Created November 15, 2015 13:55

example

	FROM debian
	MAINTAINER Noriyuki OHKAWA <[email protected]>

	RUN apt-get update
	RUN apt-get install --no-install-recommends -y tomcat8
	ADD openam/OpenAM-12.0.0.war /var/lib/tomcat8/webapps/openam.war

	EXPOSE 8080

	CMD /usr/lib/jvm/default-java/bin/java \

notogawa / FLOPS2016.agda

Last active March 13, 2016 01:15

FLOPS 2016 Agda Tutorial, Andreas Abel

	-- FLOPS 2016 Agda Tutorial
	module FLOPS2016 where

	-- 歴史の話
	-- ALF Half Agda1 ALFA AgdaLight Agda2

	-- Simply Typed Lambda Calculus
	-- Checking Inference Lookup Rules

	data ℕ : Set where

notogawa / HelloWorld.hs

Created April 19, 2016 14:14

Hello,World!

	module Main where

	import Network ( withSocketsDo, listenOn, PortID(PortNumber), connectTo )
	import Network.Socket ( accept, send, close, recvLen )
	import Control.Concurrent ( forkIO, threadDelay )
	import System.IO ( hClose )
	import Control.Monad ( void )
	import Control.Exception ( bracket )

	main :: IO ()

notogawa / MatrixProd.hs

Created October 19, 2016 09:46

	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE TypeInType #-}
	import Data.Kind
	import Data.Proxy
	import Data.Singletons
	import Data.Singletons.TypeLits
	import Data.Type.Equality
	import GHC.TypeLits

notogawa / ET.agda

Last active November 16, 2016 10:39

	module ET where

	open import Data.Maybe
	open import Data.Nat
	open import Data.Bool using (Bool; true)
	open import Data.Product using (∃; _,_; _×_)
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary using (Dec; yes; no)

	data TypeRep : Set where

notogawa / NumpyLike.hs

Last active November 19, 2016 05:43

https://twitter.com/notogawa/status/799529449498804224

	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE DataKinds #-}

	import Data.Singletons
	import Data.Singletons.Prelude.Enum
	import Data.Singletons.Prelude.List
	import Data.Singletons.Prelude.Num
	import GHC.TypeLits

notogawa notogawa