notogawa

-- 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

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

-- 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

{-# 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

{-# 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

{-# 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

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
import Prelude hiding ( (+) )
import qualified Prelude as P

class FuzzyAddable a b c where
    (+) :: a -> b -> c
instance FuzzyAddable String Int String where
    a + b = a ++ show b
instance Num a => FuzzyAddable a a a where

notogawa

-- 各データ型に対する帰納法の定義を考えると，
-- ≡の定義の仕方(parameter1つとindex1つ/index2つ)による差がわかる
module Ind where

-- ℕ
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

-- ℕに関する帰納法

notogawa

module Test where

open import Relation.Binary.PropositionalEquality

postulate
  extensionality : ∀ {a} {b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

covariant : {B : Set} → (B → B → B) → {A : Set} → (A → B) → (A → B) → (A → B)
covariant _⊕_ f g = λ x → f x ⊕ g x

notogawa

open import Category.Monad

module DoLikeNotation {l M} (monad : RawMonad {l} M) where

open RawMonad monad

bind-syntax = _>>=_

syntax bind-syntax F (λ x → G) = ∣ x ← F ∣ G