2009-01-01から1年間の記事一覧

今年のまとめ

自分のブログのログを見てみると、 2月 Webサーバ書く為にプロトコルスタック書く為にOS書いたような事をしてしまっている 3月 大阪さんとPrologみたいなことでATNDを使い始める この辺から、プログラムってそもそもどうなってるんだろう?とか型って...?みた…

高等魔術の教理と祭儀

http://ratiwo.blogspot.com/2009/12/reading-craft-of-prolog.html参加してきました。もひかんさんスライド作成本当にお疲れさまでした。スライドに疑惑の部分があって。 http://twitter.com/zick_minoh/status/7089081847 これは少し内包的な説明ですが、…

誰得

ですが、発表に使った資料をあげておきます。なぜなに依存型View more documents from ranha.

年始Haskell論文読み会

Type Checking with Open Type Functions ( http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html ) System F with Type Equality Coercions ( http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html ) Complete and Decidable Type Inference for GADTs ( …

atが書けないぴーーーーーーー

data Unit : Set0 where unit : Unit data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Bool _+_ : Nat -> Nat -> Nat zero + b = b (succ a) + b = succ (a + b) data Hold (T : Set0) : Set0 where hold :…

真ん中の気持ちです

期待でも諦めでもない真ん中の気持ち。 {-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} data …

手抜きした

{-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE FlexibleContexts #-} data Zero where Zero :: Zero data Succ a where S…

型付けされたTree とその上の関数

{-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE OverlappingInstances #-} {-…

良く型付けされたtake関数

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiParamTypeClasses , ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts , TypeSynonymInstances #-} {-# LANG…

12/13

http://atnd.org/events/2487Boost勉強会の翌日に何かこんなものがあるので、時間がある人はどうぞ。場所とかは完全に不定。 お店に迷惑をかけず隅の方でひっそりと何かしてはまた別の店に移るとかそういうスタイルです。っていうかちゃんとした場所今から探…

一応C++でもやってみましたが

http://twitter.com/zick_minoh/status/62235261562日近くも掛かってしまいました。ひーん。Haskell版をただ書き直しただけです。templateとかtypenameとかすぐ忘れてしまいますね。なんでやねん的なのが多かったです。 あと結局あちこちにapplyを書く事にな…

メモリたくさん欲しいです

http://blog.livedoor.jp/geek/archives/50888709.html萌え萌えウソつきッ娘論理パズルI作者: 小野田博一出版社/メーカー: イーグルパブリシング発売日: 2009/09/25メディア: 単行本(ソフトカバー)購入: 5人 クリック: 172回この商品を含むブログ (7件) を…

FunDepsやらHaskellのTips

完全にメモ書き conflictをなんとかしたい {-# LANGUAGE KindSignatures #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableIn…

たいぷしのにむで部分適用したい

けど出来ないので次のようになってしまう・・・。 {-# LANGUAGE KindSignatures, TypeFamilies, EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, FlexibleInstances #-} data Nil data Cons a b type…

w1 = (\x -> (\y -> f x y)) X と w2 = (\y -> f X y)が異なる時

http://twitter.com/ranha/status/6103936333 の弁明。 遠回り 先日のメモ化fib関数について色々弄っていたのでその過程の何ソレを書き出してみます。まず大元の定義は at :: ∀a.[a] → Int → a at (a : b) 0 = a at (a : b) (n + 1) = at b n map' :: ∀a b.(…

メモ

Data.MemoCombinatorsモジュールについて言及したblog http://www.amateurtopologist.com/2009/11/22/data-memocombinators-and-you/ を見つけて、何をどうしてCombinatorsというモジュール名にしたのかというのとどういう実装に成っているか知りたいので読…

Go言語ぽい不動点演算子

//cat paraY.go package main import "fmt" func p(v ...) { fmt.Println(v) } func Para(a func (),b func ()) { go a(); go b(); } func dummy(x int,c chan int) { p(x,"in dummy"); } func Y1(f func (func (int,chan int)) (func (int,chan int))) (fun…

チャネルを用いた計算

Goを使って普通なプログラムを書くべきで、ただ私みたいなうんこ野郎にはそんな事は出来ないというか、Concurrency使わないんだったらC++使うっていうそれなので、なんとかしてConcurrencyを使わなければ成りません。プログラムを書くといえば何か動くべきな…

Go言語は良い言語です

http://atnd.org/events/2115というイベントがありました。11月14日に、Google渋谷オフィスでありました。まずはじめに、Googleさんには場所を提供してもらった上にGoogleの中の人にも参加してもらって結果盛り上がったので本当にありがとうございましたとし…

Go言語

http://atnd.org/events/2115誰か来てください... 追記 グーグル渋谷オフィスをお借りする事になりました。どうしてこうなった・・・ありがとうございます。引き続き誰か来てください...

アジア地区予選参加記

11月7,8,9の3日間、ICPCアジア地区予選東京大会に参加して来ました。うちのチーム(UNK)は2問しか解けないとかいう、去年より酷いぞっていう感じで、2問ていうのは例えば、これは私にしか分かりませんが木曜日に惨劇が繰り広げられるレベルで酷いです。去年も…

たまには型のあるSchemeでも

目標 トリック オア トリート(Trick or Treat)に因んだ何かを証明してみる!!と題して(¬Treat -> Trick) -> (Trick ∨ Treat) [日本語訳 : お菓子をくれないなら悪戯しちゃうぞ -> 悪戯 か お菓子である!!] 今回はちょっと準備をします 今回はHaskellで証明…

あぐだちゃんがトリックを仕掛けて来たようです

data Bool : Set0 where true : Bool ; false : Bool data _∨_ (A : Set0) (B : Set0) : Set0 where intro1 : A -> A ∨ B intro2 : B -> A ∨ B data Id {A : Set0} : A -> A -> Set0 where refl : (a : A) -> Id a a -- Boolはなぁ・・・trueか、falseだけな…

これは買いたいなー

http://journal.mycom.co.jp/news/2009/10/30/087/index.htmlと思ったけど、PSPはついてないんですね。まぁPSP買っても良いかなーみたいなソレはどうしよう。12/3って確実に悲しい生活に陥ってるので何をやるにしても年末だよなぁみたいな。

C++0xにはdefault template parameterがあるらしいです

ので取りあえずソレを使ってみてかわいそうな事をしてみたのですが int main() { Or<A,B> o = or_intro1<A,B>(A()); C c = or_elim(o,impl_intro(f),impl_intro(g)); //↓だとオッケー //C c = or_elim(or_intro1<A,B>(A()),impl_intro(f),impl_intro(g)); } error: no match</a,b></a,b></a,b>…

計算機言語で定理証明#1

さる10月24日 土曜日に大久保で次のようなイベントがありました。http://atnd.org/events/1507ありましたもといやりましたもとい出来ました。何度かこのブログでも人が少ない困ったみたいな事を書いたのですが、当日は最終的に9人の参加になりました。すごい…

Haskell Not 98

{-# LANGUAGE GADTs #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} data Zero data Succ a data Plus a b data Id :: * -> * -> * where Refl :: a -> Id a a Symm :: (Id a b) -> Id b a Tran :: (Id a b) -> (Id b c) -> (Id a c)…

C++で証明のついったタイムラインまとめ

凄く見辛いですけど、タイムラインを纏めてみました。http://ranha.tumblr.com/day/2009/10/22/使ったのは、http://esuji.daa.jp/log/matome_st.php です。

宣伝2

http://atnd.org/events/1507twitterで#proofpartyを付けて事前活動をもそもそやった結果9人に!!ありがとうございます。定員を一応10人としていて後1人大丈夫です、ので画面の前のキミ。そうキmry 来てください。今週土曜日に下のエントリでC++使ってした…

お腹すいた...

ちゅらいね。この流れは...? //はてなのC++カラーリング指定子がcppになってるのどうにかしてくだち /* 取りあえずNat */ struct zero{}; template<typename>struct succ{}; template<typename N1,typename N2>struct add{}; template<typename N2> struct add<zero,N2> { typedef N2 val; }; template<typename N1,typename N2> struct add<succ<N1>,N2> </succ<n1></typename></zero,n2></typename></typename></typename>…