日々の流転

λ. 継続操作を持つEDSLをHaskell上で実装する

ranhaさんが Yet Another Ranha (2010-01-01), Yet Another Ranha (2010-01-04) あたりで悩んでいた話を言語雑談会で少し聞いた。 何をやりたかったのかイマイチ良くわかっていないけど、とりあえず↓みたいな感じだろうか。しかし、継続モナドでいいじゃんという気も。

{-# LANGUAGE EmptyDataDecls, GADTs, TypeFamilies #-}

data Void
type Not a = a -> Void
type T a = Not (Not a)

data Exp t where
   Lam :: (Exp a -> Exp b) -> Exp (a -> b)
   App :: Exp (a -> b) -> Exp a -> Exp b
   A :: Exp Void -> Exp a
   C :: Exp (T a) -> Exp a
   Wrap :: Star a -> Exp a

type family Star t
type instance Star Void = Void
type instance Star Int = Int
type instance Star (a -> b) = Star a -> T (Star b)

cps :: Exp t -> T (Star t)
cps (Lam f) k = k (\a -> cps (f (Wrap a)))
cps (App e1 e2) k = cps e1 (\f -> cps e2 (\a -> f a k))
cps (A e) k = cps e id
cps (C e) k = cps e (\f -> f (\v _ -> k v) id)
cps (Wrap v) k = k v

限定継続なし版 - Yet Another Ranha (2010-01-27) に続く。

追記

しかし、これが型付けできるってのには結構驚いた。

これと同じようなことを class Star t t' | t -> t' みたいな型クラスを使ってやろうとすると、App構成子に文脈をつける必要があるはず。 でないと、e1 :: Exp (a -> b), e2 :: Exp a としたときに、cps関数のAppの場合の定義で、Star b b' の文脈だけからは Star a a' を導けなくて困ったことになってしまう。

型クラス+関数従属性で表現できるのは型上の部分関数であって、インスタンス宣言しているところにだけ定義されるのに対して、型族は型上の全域関数であって、インスタンス宣言は具体的な表現に触るときにだけ必要ということか。 型族は型クラスの関数従属性の置き換えとして紹介されることが多いけど、実際の使い方はずいぶん違うように感じるなぁ。

関連

• @keigoi
  • <URL:http://twitter.com/keigoi/status/8329484270>
  • <URL:http://twitter.com/keigoi/status/8341823894>
  • <URL:http://twitter.com/keigoi/status/8342082624>
  • <URL:http://twitter.com/keigoi/status/8342427877>
  • <URL:http://twitter.com/keigoi/status/8342751070>
• @ranha
  • <URL:http://twitter.com/ranha/status/8353039440>
  • <URL:http://twitter.com/ranha/status/8353067468>
  • <URL:http://twitter.com/ranha/status/8353102433>

λ. 結合的でない二項演算

言語雑談会で、圏の公理から射の合成の結合律を取り除いたらという話が出たのだけど、例を考えるのに苦労していたので、Alloyで結合的でない二項演算を適当にでっち上げてみた。

• (2・1)・2 = 1・2 = 0
• 2・(1・2) = 2・0 = 2

モノイドは対象が一個だけの圏なので、この例も対象が一個だけだと思えば、射の合成の結合律を除く圏の公理は満たす。 まあ、特に面白い例ではないけど。