ファミコンのゲームはたのしい。このゲームでは、フルーツショップのお姉さんがすごい魅力的な気がする。魅力的な人の写真は載せない。

http://www.cs.chalmers.se/~nordland/ohaskell/survey.html data BW = Black | White data Color > BW = Red | Orange | Yellow | Green | Blue | Violet このColor > BWっていうのは、というか、'>'わりと気に食わない記号だけれども兎も角拡張したいなー…

というわけで私の3ヶ月(なんだっけ7月から?)が楽しかったのは、敷居の住人という漫画による所が大きいワケです。アイドルは活力なんですが、原動力にならない所とかあって、まぁ私はダメですから。従ってダメです。 今日一日遅れで、5巻と6巻(こっち最終巻)…

LandinのThe Next 700 Programming Language( http://portal.acm.org/citation.cfm?id=365257 )は1966年のCACMに載っていた話なんですけれども、今読んでいるAn Algorithm for Type-Checking Dependent Types ( http://www.cs.chalmers.se/~coquand/type.ps …

Inductive Bool : Set := true : Bool | false : Bool. Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a. Definition f (arg : Ty true) := match arg with | ty true => true end. これで、fをCheckすると f : Ty true -> match true with | true …

髪の毛が乾くまで暇なので書く。 data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : (Ty unit) -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty x) = unit この型チェックエラーメッセージ fの型チェッ…

data D : Set0 -> Set0 where nat : D Nat bool : D Bool f : {A : Set0} -> A -> D A -> Unit f (zero) (nat) = unit Cannot split on argument of non-datatype @0 when checking the definition of f これは、Agda2のnotesディレクトリの中、"inductive-f…

data Nat : Set0 where zero : Nat succ : Nat -> Nat data Ty {A : Set0} : A -> Set0 where ty : (a : A) -> Ty a f : Ty zero -> Nat f (ty .zero) = zero {- f (ty zero) = zeroだとすると a != zero of type Nat when checking that the pattern ty zer…

昨日のアレはMLで質問してみました http://thread.gmane.org/gmane.comp.lang.agda/1015すると、Wouterさんが、 http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.DatatypeAndFunctionDefinitions ここにdot patternがあるからそれを使えば良いんじゃね…

data Unit : Set0 where unit : Unit data Ty : Unit -> Set0 where ty : (u : Unit) -> Ty u f : Ty unit -> Unit f (ty unit) = unit g : Ty unit -> Unit g (ty a) = agがあれだよなー a != unit of type Unit when checking that the pattern ty a has t…

module what_happen where data Unit : Set0 where unit : Unit {- data X : Set0 -> Set0 where 要素(canonical element)が無いというコレでも -} data X : Set0 -> Set0 where x : X Unit -- xは定義したものの意味は無い nonsense : X -> Unit -- nonsens…

ranha 10月10日ぐらいに、簡単に定理証明系で殴り合うみたいなイベント無いかなぁ。メジャーな○○の使い方も、各々異なる所があるので、やってる人が個別にスタイルを教えてくれたりすると手っ取り早くて良いかなーとか。Proof Generalというかtacticalな証明…

Haskellの話じゃなくて、またもAgda2の話です。具体的には data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Boolとかでまぁ、データ型を定義して、その上で次のような関数 nonsense : Set0 -> Nat nonsense…

分からなくなるもなにも、最初から何も知らん！！！！！！！ data Bool :: * where true :: Bool false :: Bool みたいな事を書いた時、このtrueとかfalseさんて一体何者なんだろうっていう雰囲気。例えば、 data Bool :: * where true :: Nat false :: Nat …