myuon

definition (in Category) Iso where
  "Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))"

definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where
  "𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)"

record 'c setmap =
  setdom :: "'c set"
  setcod :: "'c set"
  setfunction :: "'c ⇒ 'c"

myuon

{-# LANGUAGE DeriveFunctor #-}

import Control.Applicative
import Control.Arrow
import qualified Control.Category as C
import Control.Monad

data Process m a b = Process { runProcess :: a -> m (b, Process m a b) }
                   deriving (Functor)

myuon

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts, RankNTypes, ConstraintKinds #-}
import GHC.TypeLits
import GHC.Prim (Constraint)
import Control.Monad.State

data SList (k :: Symbol -> Constraint) (a :: Symbol -> *) where
  Nil :: SList k a
  Cons :: k s => a s -> SList k a -> SList k a

myuon

theory MonMonoid
imports Main
begin

locale Monad =
  fixes mreturn and mbind (infixl ">>-" 60)
  assumes left_return: "mreturn a >>- f = f a"
  and     right_return: "m >>- mreturn = m"
  and     assoc: "(m >>- f) >>- g = m >>- (λx. f x >>- g)"

myuon

D-Island

ようこそ "D-Island" へ！ あなたはとても楽しいゲームに参加する権利を得た幸運な人です. ゲームは簡単, 相手を欺いて生き残るだけです. さらに幸運なことに, あなたには特別な武器まで差し上げます. もちろん, たださし上げるだけでは面白くありませんから, キチンと条件もつけておいてあげます. あなたほどの人なら, ペナルティなど受けるはずもありませんね.

そうそう, まだ不確定な情報なのですが, 手違いでゲームにはミュータント(突然変異種)が紛れ込んでいるようです. くれぐれもお気をつけて.

myuon

	Sun Feb 22 21:07 2015 Time and Allocation Profiling Report  (Final)

	   main +RTS -p -RTS

	total time  =       43.20 secs   (43204 ticks @ 1000 us, 1 processor)
	total alloc = 17,430,883,416 bytes  (excludes profiling overheads)

COST CENTRE       MODULE                    %time %alloc

main.paintOf.area Main                       33.6    0.8

myuon

module HitBlow where

import System.Random
import Control.Monad
import Data.List

decideNums :: IO [Int]
decideNums = do
  ixs <- forM [0..3] $ \i -> randomRIO (0,9-i)
  return $ fst $ foldl (\(a,a') i -> ((a'!!i):a,delete i a')) ([],[0..9]) ixs

myuon

{-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies, UndecidableInstances, PartialTypeSignatures #-}

-- Nat

data Zero
data Succ n
data Nat n where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

myuon

{-# LANGUAGE DataKinds, GADTs, EmptyCase, ViewPatterns, TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

import Control.Monad
import Test.QuickCheck
import Debug.Trace

data Nat = Z | S Nat deriving (Show)
type N0 = Z
type N1 = S N0

myuon

theory Lambda
imports Main
begin

section {* Lambda Calculus *}
subsection {* Definitions *}

type_synonym var = nat
datatype lambda_p = Var var | Abs' var lambda_p | App' lambda_p lambda_p