■

unsafePerformIOはよくわからん

import System.IO.Unsafe
main=
 do {c<-getChar;
    if (c ==':') 
     then (putChar '\n') 
     else (putChar c)>>main}

のつもりで、

import System.IO.Unsafe
main=
 let c = unsafePerformIO getChar
  in if (c ==':') 
      then (putChar '\n') 
      else (putChar c)>>main

と書いたら、main自身とmain内部で呼び出されてるmainで、変数cの値共有してんの？Schemeのletとは違うのかもしれない。初心者が、unsafePerformIOとか使うなって話か。

あと、ベクトルや行列を書こうとして、

(+) :: (Integer n) => (Vector n) -> (Vector n) -> (Vector n)
(+) :: (Integer n,Integer m) => (Matrix n m) -> (Matrix n m) -> (Matrix n m)

みたいなことがしたいと思った。依存型とかいうやつですか。一般の高階テンソルだと、

(+) :: ([Integer] c , [Integer] a) => (Tensor c a) -> (Tensor c a) -> (Tensor c a)

とか。C++ならできるよ！

Buchebergerアルゴリズムをfold尽くしで書くという話。inductiveなデータ型を定義すると、必ず付随してfold関数が定義できる(CoqでInductiveを使ってデータを作ると、必ず帰納法が生成されるのと同じ)。

以下、Haskellで。

--自然数型
data Nat = Zero | Suc Nat
fold_nat :: a -> (a -> a) -> Nat -> a
fold_nat init f x = case x of
  Zero  -> init
  (Suc n) -> (f (fold_nat init f n))

--リストの場合
data List2 t = Nil | Cons t (List2 t)
fold_list :: a -> (t -> a -> a) -> List2 t -> a
fold_list init f x = case x of
  Nil -> init
  (Cons x xs) -> (f x (fold_list init f xs))

--多項式
data Polynomial t = 
 Const t | Var String |PLUS (Polynomial t) (Polynomial t)|MULT (Polynomial t) (Polynomial t)

fold_polynomial const var plus mult expr = case expr of
 (Const x) -> (const x)
 (Var x) -> (var x)
 (PLUS x y) 
  -> plus (fold_polynomial const var plus mult x) (fold_polynomial const var plus mult y)
 (MULT x y)
  -> mult (fold_polynomial const var plus mult x) (fold_polynomial const var plus mult y)

fold_listは、通常と引数の順序が異なることを除けば、いわゆるfoldr。fold_natはfをinitにn回適用する関数。要するに、fold関数は、与えたデータの型構成子を別の値に置き換える。
fold_list init f (Cons 3 (Cons 2 (Cons 1 Nil))) = (f 3 (f 2 (f 1 init)))
という具合。fold_polynomialを使って、Buchbergerアルゴリズムって書けそうにないな

いつになったら、monadic semanticsに戻れるんだろう･･･