日々の流転

λ. Haskell で始めたプログラマに C を教えるには…

• Haskell で始めたプログラマに C を教えるには…
  • FFI からアセンブラが分かるはずだから、Monad -> FFI 経由で教えるのがいい？

FFI からアセンブラが分かる……

　　 ／￣￣￣￣￣ ミ
　 /　　 ,————-ミ
　/　　／　 ／　　 ＼ |
　|　 /　　　,（・）　（・） |
　 (6　　　　　　 つ　　|
　 |　　　　　　＿＿_　 |　　 ／￣￣￣￣￣￣￣￣￣￣
　 | 　　　　 /＿＿/ ／　 ＜　なわけねぇだろ！
／|　　　　　　　　 ／＼　　 ＼＿＿＿＿＿＿＿＿＿＿

λ. monadic catamorphisms

僕の知っている monadic catamorphism は、以下のfoldWithM*1を使って書かれるようなもの*2なのだけど、これは 横山さんの日記 に出てきているものと同じものなのだろうか。

import Control.Recursion
import Control.Monad
 
foldWithM :: (Fixpoint f t, Monad m) => (forall a. f (m a) -> m (f a)) ->
             (f x -> m x) -> (t -> m x)
foldWithM k phi = fold (\x -> k x >>= phi)

λ. OCaml入門 (3): 多相バリアント(polymorphic variant)

Haskellの代数的データ型やMLのバリアントはデータ構築子がその型に結び付けられてしまうけど、似たようなデータ型が複数あるときには、データ構築子を共有したいこともある。そんなときにOCamlでは多相バリアントというのを使うことが出来るそうだ。

多相バリアントのデータ構築子は、バッククォート「`」で始まる名前で、データ型を定義せずに使うことが出来る。`Aまたは`Bで構築された値の型は [> `A | `B] となる一方、`Aまたは`Bで構築された値だけを受け取る関数の引数の型は [< `A | `B] となるようだ。

試しにλ式をSKIコンビネータに翻訳するコードを書いてみる。

# let (@) a b = `App (a,b) ;;
val ( @ ) : 'a -> 'b -> [> `App of 'a * 'b ] = <fun>
# let rec ski x t =
    match t with
      `Var y when (x==y) -> `I
    | `App (y,z) -> (`S @ ski x y) @ ski x z
    | `Lam (y,z) -> ski x (ski y z)
    | _          -> `K @ t
;;
val ski :
  'a ->
  ([> `App of 'b * 'b | `I | `K | `Lam of 'a * 'b | `S | `Var of 'a ] as 'b) ->
  'b = <fun>
# let test1 = `Lam (0, `Var 0) @ `Hoge ;;
val test1 : [> `App of [> `Lam of int * [> `Var of int ] ] * [> `Hoge ] ] =
  `App (`Lam (0, `Var 0), `Hoge)
# let test2 = ski 0 test1 ;;
val test2 :
  [> `App of 'a * 'a | `Hoge | `I | `K | `Lam of int * 'a | `S | `Var of int ]
  as 'a = `App (`App (`S, `App (`K, `I)), `App (`K, `Hoge))
# 

skiは `Var, `App, `Lam 以外のデータ構築子で構築された値も受け取れるので、skiの引数の型は [< `App of ... | ...] という形ではなく、[> `App of ... ] という形になっている。

使ってみた感じでは、ちと強力すぎる気がする。もう少し制限された形でも十分ではないか?

あと、asを使って循環的な型を書けるというのに少し驚いた。infinite unification?　単にoccurs-checkをしなければ良い?　infinite unification で検索したら、An Overview of the Theory of Relaxed Unification, Tony Abou-Assaleh, Nick Cercone, and Vlado Kešelj というのを発見。

λ. 『常識としての軍事学』, 潮 匡人

を読んだ。