FOP/ex12.2 - 大久保弘崇

12.7

compress RDyn (Dyn ra a) = compressRep (Rep ra) ++ compress ra a
uncompress′RDyn ks = case uncompressRep′ks of
  (Rep ra, ks′) → case uncompress′ra ks′of
    (t, ks′′) → (Dyn ra t, ks′′)
 

ただし Dynamic 型の値はまだ Show できないので結果が表示できない。次の問題の結果を利用する。

12.8×

prettyもparseも趣味のレベルなのでパス。
上の問題の結果が確認できるよう、単純な文字列表示の関数を代わりに作る。

toString :: Type t → t → String
toString RInt i = typeName RInt + + show i
toString RChar c = typeName RChar + + show c
toString (RList RChar) s = typeName (RList RChar) + + show s
toString (RList ra) [ ] = typeName (RList ra) + + ”[]”
toString (RList ra) (a : as) = typeName (RList ra) + + ”[ ” + + toString ra a + + inner as where
  inner [ ] = ”]”
  inner (a : as) = ”, ” + + toString ra a + + inner as
toString (RPair ra rb) (a,b) = typeName (RPair ra rb) + + ”(” + + toString ra a + + ”, ” + + toString rb b + + ”)”
toString RDyn (Dyn ra a) = typeName RDyn + + toString ra a
 
typeName :: Type t → String
typeName RInt = ”RInt ”
typeName RChar = ”RChar ”
typeName (RList RChar) = ”rString ”
typeName (RList ra) = ”(RList ” + + typeName ra + + ”)”
typeName (RPair ra rb) = ”(RPair ” + + typeName ra + + typeName rb + + ”) ”
typeName RDyn = ”Dyn ”
 

12.9

tequal は「型の」同値性検査 (をしたあとに id を返すもの) であって値の同値性検査ではないので、関数型を含めろと言われても恐くない。

data Type t where
  -- 略
  RFunc :: Type a → Type b → Type (a → b)
tequal (RFunc ra1 rb1) (RFunc ra2 rb2) = liftM2 func (tequal ra2 ra1) (tequal rb1 rb2)
tequal (RDyn) (RDyn) = return id
func :: (b → a) → (c → d) → (a → c) → (b → d)
func eq1 eq2 = λ f → eq2 ◦ f ◦ eq1
 

12.10△

Type τの構成子に対する場合分けで両方の式を証明する。
特に難しいところはない。

後半は

がいえるかということ。
一見成り立ちそうに見える(成り立たない反例が思い当たらない)。
ならば前半と同様に証明することになるが、大変そうなのでパス。

12.11

icrush, everything, everything′:: ∀ t . (t → t → t) → t → Query t → Query t
icrush op i f (RInt) a = i
icrush op i f (RChar) a = i
icrush op i f (RList ra) [ ] = i
icrush op i f (RList ra) (a : as) = f ra a ‘op‘ f (RList ra) as
icrush op i f (RPair ra rb) (a,b) = f ra a ‘op‘ f rb b
icrush op i f (RPerson) (Person n a) = f rString n ‘op‘ f RInt a
icrush op i f (RDyn) (Dyn ra a) = f ra a
everything op i f rt t = f rt t ‘op‘ icrush op i (everything op i f ) rt t
everything′op i f rt t = icrush op i (everything op i f ) rt t ‘op‘ f rt t
 

12.12

ラムダ抽象Funを表示するときに、抽象変数に名前をつけなければならない。
これをどこまで消費したかをタプリングで持ち回す。

instance Show (Term t) where show t = fst $ show’ t vars
 
show’ :: Term t → [String] → (String, [String])
show’ (Var n)   vs = (n, vs)
show’ (App a b) vs = ("(App " + + sa + + " " + + sb + + ")", vb) where
  (sa, va) = show’ a vs
  (sb, vb) = show’ b va
show’ (Fun f) (v:vs) = ("Fun (\\ " + + v + + " -> " + + sfv + + ")", vfv) where
  (sfv, vfv) = show’ (f (Var v)) vs
 
vars = [ c:[] | c ← chars ] + + [ cs + + c:[] | cs ← vars, c ← chars ] where chars = [’a’..’z’]
 

コメント