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

こわいはなし

{-# LANGUAGE TypeFamilies , ScopedTypeVariables #-} type family TF a f :: TF a -> Int f (v :: TF a) = 0 ghciに投げ込むと /Users/ranha/Haskell/proghost% ghci kowai.hs GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help Loading pac…

最底辺ICFPC参加者のメモ

初日 21時に問題がオープンになって、訳し始める。訳してる時はまぁこれから72時間頑張ろうみたいな感じだったけれども、翻訳してる時が、一番楽しい時間だった。取りあえず翻訳し終わって、どうしようみたいな感じに。取りあえず回路読めないと話がはじまら…

分数の応用問題

最初に思い浮かんだものとしては a - b = c -> c <= a ... (1) ただしaとbは小学4年生の学習指導要領及びドリルなどに出てくる程度の分数を表す。この式(1)が、小学4年生の範囲で常に成り立つ事は明らかに思えます。けれども、この画像の女の子(緑ちゃん！)…

メモ

{-# LANGUAGE GADTs #-} data Ident a where Ident :: a -> Ident a instance Functor Ident where -- fmap :: (a -> b) -> Ident a -> Ident b fmap f (Ident a) = Ident (f a) in1 :: Ident () -> () in1 = const () in2 :: Ident Bool -> Bool in2 (Ident…

突発鎌倉への旅

発端 http://twitter.com/ranha/status/13193995157http://twitter.com/ranha/status/13224615165という事で鎌倉に行って来ました！！以下未来の私の為に時系列順 + 写真 品川 品川駅の横須賀線乗り場に到着したのが、9時少し過ぎ。横須賀線で鎌倉へ向かう。…

Generic Programmingおよび、C++のConceptに関する話

http://ranha.kerox.info/nandemo/?Comparative+StudyなぜかWikiを建てたので、埋まってない所を勝手に埋めたり、分からない所はとことんコメントを書いたりしてください。 OCamlの所が完全に人間足りてない感じです。あとC#

Olegさんから話を聞く会

前編 4/24土曜は、Olegさんの話を聞く会を聞く為に東京に来ました。 朝方までPS2でパチンコのようなものをやった挙げ句、全然大学で眠れなかったとかいうのもあって、ただでさえ辛い早起きがウルトラ辛かったような気がします。取りあえず最初の話は、Abstra…

Why fail apply?

Signature File sig lc. kind tm,ty type. type c tm. type app tm -> tm -> tm. type abs (tm -> tm) -> tm. type top ty. type arrow ty -> ty -> ty. type ty ty -> o. type of tm -> ty -> o. type step tm -> tm -> o.Module File module lc. ty top. t…

fresh vs forall

tm : type. step : tm -> tm -> type. sn : tm -> type. sn_ : ({U:tm} step T U -> sn U) -> sn T. lem : (sn T) -> (step T U) -> (sn U) -> type. %mode lem +D1 +D2 -D3. lem_pr : lem (sn_ Pred : sn T) (StepTU : step T U) (Pred U StepTU). %termina…

お知らせ

http://atnd.org/events/4060 要旨 去年に引き続いての開催。 どういう人が、どういう内容物であの入試をくぐり抜けて来たのかというのを肌で感じよう、というのが目的です。 特に ●大学に入学して/入学するまでに何をしたか、をスライドにし他人に発表して…

合成に合成を適用以下略

{- 1個の時 _1 a1 a2 a3 = a1 (a2 a3) -} {- 2個の時 Prelude> :t (.)(.) (.)(.) :: (a1 -> b -> c) -> a1 -> (a -> b) -> a -> c (.) a1 a2 a3 = a1 (a2 a3) (.)(.) a2 a3 = (.) (a2 a3) = (\a4 a5 -> (a2 a3) (a4 a5)) _2 a1 a2 a3 a4 = (a1 a2) (a3 a4) P…

定義が良く分からないので...

ここ3日ぐらいちょいちょいと読んでいるRalph Matthesさんの論文全然分からない所があるのではてなさんに纏めてみます。 つまりぼくでは分からない過ぎるので、分かる人に教えて貰いたいという事なのですが...。MatthesさんのInductive Typesを扱った論文で…

早起きは三文の得

http://togetter.com/li/11331折角なのでtogetterさんを使ってみました。何か纏める意味はないよなーと思われたものの、幾つかの場所でPropとSet0の違い論争は起こるので他の人がググった時に何か出て来てもしかしたら役に立ってくれるのではないかしらとい…

Immutable Object読書会

今日手元に本が届いたので開催されることが確実になったのでこちらでも告知というか何か... 既に殆ど埋まっていますが。http://atnd.org/events/3612Immutable Objectというそれらしい本を読みつつ、本の内容に期待出来ない可能性が大いにあるので、Immutabl…

ProofParty第2回目の話

http://atnd.org/events/29893/13日にProofPartyの第2回目がありました。今回の内容は、 「ハノイの塔では最短手数が(2^n)-1となることを証明する」 「例の採用問題でLv4になる」 の2つがメインでした。結果としては、前者がまだ書けていない、後者は既にyos…

ProofPartyのリマインダ

試験の準備などで殆ど頭から忘れ去られていたのですが、http://atnd.org/events/29893/13の13:00〜20:00でコレがあります。場所は、今の所大久保です。 取りあえずそういう中でリマインダとしてこのエントリを書いておきます。10人ぐらいなら他に、こういう…

C++のためのろじっくぱらだいむ

2010年の5月にBoostConがあるというのは良く知られた話らしいです。2009年のBoostConでは、Andrei Alexandrescuさんによる"Iterators Must Go"をはじめとする発表が行われたようです。 (私はAlexandrescuさんの発表でBoostConの存在を知りましたが...。 それ…

JFlow、Jifでthisがcovariant parameterになっている事が分かる感じのセット

class C[covariant label L1,covariant label L2] { } class Tester[label l1,label l2,label l3,label l4,label l5,label l6] { void test() { C[l1,l3]{l5} c1 = null; C[l2,l4]{l6} c2 = null; if(l1 <= l2 && l3 <= l4 && l5 <= l6){ c2 = c1; } } } thi…

あっそしあてぃぶでないだいすうけい？

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20100124#p02この話も雑談会の時に私が出しちゃって、うーんでも何か納得行く系のヤツが無いんだよなぁと思っていたら、先日買った数学の視点 (math stories)作者: 上野健爾出版社/メーカー: 東京図書発売日: …

くらっかーぼんぼん

http://ranha.kerox.info/crackerbonbon/うちの大学多分こういうの無いので、例によって勝手に作りました！！！うおおおおおおおおおやりました！！！！！！俺のPOPL力とかICFP力を見てくれ！！という人は発表してくださいお願いします・・・。私は取りあえ…

AURA語

CACMのType Theory Comes of Age HTML : http://cacm.acm.org/magazines/2010/2/69367-type-theory-comes-of-age/fulltext PDF : http://cacm.acm.org/magazines/2010/2/69367-type-theory-comes-of-age/pdf を丁度先週ぐらいに読みました。話の内容としては…

計算機言語で定理証明 第2回

ATNDにページを作っておきました。http://atnd.org/events/2989恐らく今回の問題とかはWikiの方に書く(もしくは参加する人がガンガン書き込んでください)ので、興味の有る方はそちらも見てください。 (ATNDの参考URLにWikiのURLがあります)

限定継続なし版

http://www.tom.sfc.keio.ac.jp/~sakai/d/?date=20100124#p01 特に何がやりたい、とかは無かったんですけど限定継続の型がどないや！！っていうのを埋め込んで調べてみたかったのでというのがありました。 それでつまらない事を雑談会の時に話してしまったの…

ぼくもしゅうしょくしないと

金曜日ぐらいから採用試験の問題を考えていたのですが、自分のPCに溜め込んでいてもどうにもならないので折角だから書いてみます。いやそれよりも、MacBookさんの容量が大変です・・・どうしてこうなった。 あとプリンスオブペルシャのPS3版はちょっとうーん…

メモ

POPL2010論文読み会(http://www.cse.psu.edu/popl/10/program.html) [私は気になった∧読めるやつだけ] Verified Compilerな話が多い Verified Just-In-Time Compiler on x86 (http://lambda-the-ultimate.org/node/3768) A Verified Compiler for an Impure …

ぷちます、買いました??

-- "A Tutorial on [Co-]Inductive Types in Coq" -- 3.4 Case Analysis and Logical Paradoxes の Agda2版です。 -- Strictly Positiveが要請される１つの理由 module Paradox where open import Data.String data False : Set0 where data Nat : Set0 wher…

これはもうだめです

{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiPa…

小さい例(解決)

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FunctionalDependencies #-} class Nons nons_a nons_b | nons_a ->…

実装したい(2)

GHCのバージョンは6.10.4です。 {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInst…

継続操作を持つ言語をHaskell上で実装したい(1)

(そもそもEDSLって言うのかなぁ) (DomainにSpecificじゃないですし、なんというか、簡単な言語をHaskell上で表現する、encode、まぁ埋め込むでも良いんですがなんと言えばしっくりくるのか) {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} da…