#format md
#acl +All:read

# Applicativeのこと少し
スライドに「Monadのような計算(の一部)を applicative style(要は普通の関数型言語の書き方)で書けるようにする」と書いていますが、ちょっと何を言っているのか分からないかもしれません。

pricesにくだものの名前と値段の連想リストが入っているとして、二つの果物を買うのに必要な値段は

    :::Haskell
    buy2 fruit1 fruit2 =
      lookup fruit1 prices >>= \pri1 ->
      lookup fruit2 prices >>= \pri2 ->
      return pri1 + pri2

と書けますが、もしlookupの返り値がMaybeでなければ

    :::Haskell
    buy2' fruit1 fruit2 = (lookup fruit1 prices) + (lookup fruit2 prices)

と書くところです。Maybeモナドの文脈で計算させたいだけなのに、余計なpri1とかpri2とかいう変数が出てきて、ちょっと気持ち悪いと思いませんか？

Applicativeスタイルで書くと以下のようになります。

    :::Haskell
    buy2 fruit1 fruit2 = (+) <$> lookup fruit1 prices <*> lookup fruit2 prices

Haskellでは二項演算子はただの関数で、演算子っぽい名前がついた関数は中置記法で書くことができるものの、(+)という風に括弧で括って使うと、普通の関数と全く同じように前置記法で適用できることに注意が必要です。

とりあえずこのコードでなぜうまくいくのかはすっ飛ばして、心眼で余計な演算子を消す（Lisperが括弧を消すようなもの）と、

    :::Haskell
    buy2' fruit1 fruit2 = (+) (lookup fruit1 prices) (lookup fruit2 prices)

と読むことができます。

つまりは

    :::Haskell
    buy2' fruit1 fruit2 = (lookup fruit1 prices) + (lookup fruit2 prices)

ですね。

読みにくいだけだと思うかもしれないですが、この例くらいなら慣れれば読みやすくなる、という感じですかね。Applicativeに限った話ではないですが、気持ち悪い見た目には現実問題として慣れるしかないものの、本来は言語とかライブラリとかを作った側の責任であって、読みづらいと感じる自分は無能だとか感じる必要はないと思います。

---- 
`<$>`および、`<*>`は何者かというと、

    :::Haskell
    (<$>) :: Applicative m => (a -> b) -> m a -> m b
    (<*>) :: Applicative m => m (a -> b) -> m a -> m b

です。

`<$>`は、ある関数を、mの中の値に対して適用できるように「持ち上げる（liftする）」関数です。listに対するmapを一般化した概念ともいえます（ある関数を、listの中の値に対して適用できるように持ち上げる）。一方、`<*>`は、既にmの中に入ったある関数を、mの中の別の値に対して適用してやる関数です。`<*>`が定義されているのはApplicativeであるための一番重要な条件なので、「適用的（Applicative）」という名前もしっくり来ます。

また、二引数を受け取る関数である`(+)`は、実際にはカリー化されていて、「まず一引数を受け取って別の一引数を受け取る関数を返す」関数として表現されていることが重要です。

Monadよりも力が限定されている分、Applicativeには無駄に混みいった制御構造を作ってしまいにくいというメリットがあります。Applicativeすごいんだよという話は[Applicative Programming with Effects](http://www.soi.city.ac.uk/~ross/papers/Applicative.html)に載っています（読んでません）。

# GADT
代数的データ型のコンストラクタの定義を、型を指定することによって行う機能です。代数的データ型ってのは中々に身構えてしまいそうなネーミングですが、OCamlのバリアントと同じようなものだし、あるいは情報論理のequational logicに出てきたtermみたいなものとも言えます。

`data Maybe a = Nothing | Just a`という代数的データ型の定義を例とします。Maybe型の値を作るためにプログラム中に`Nothing`とか`Just 1`とか書きますが、ここで現れる`Nothing`と`Just`は、それぞれ`Maybe a`や`a -> Maybe a`という型を持つ、普通の値や関数だとみなすことができます（実際は`Nothing`から作られる`a`はfreeなので、どんな型にも成り得る）。また、`Maybe a`型を持つ値は、かならず`Nothing`あるいは`Just x`（xはa型を持つ）とパターンマッチできます。`Nothing`や`Just`といったデータコンストラクタは、「引数をいくつ受け取るか」「受け取る引数の型は何か」という情報を持っていなければなりません。

逆に考えると、`Nothing`と`Just`という名前のデータコンストラクタが存在して、データコンストラクタを値や関数（実際は値は0引数の関数と同じ）とみなしたときにそれぞれ`Maybe a`や`a -> Maybe a`という型を持っている、ということを定義すれば、`Maybe a`型を定義するのに必要な情報は全て出揃うわけです。なので、

    :::Haskell
    data Maybe a where
      Nothing :: Maybe a
      Just a  :: a -> Maybe a

という形で代数的データ型が定義できたって構わないのです。これがGADTです。

## 言語内DSLに使う
じゃあ、なんでそんな妙ちくりんな定義をしたがる人がいるんでしょう？GADTの書き方をすると、`a`みたいな型変数として現れていない型を好き勝手に導入することが簡単になります。たとえば、

    :::Haskell
    data Exp a where
      EInt  :: Int  -> Exp Int
      EBool :: Bool -> Exp Bool

という宣言を考えます。これをGADTで無い形に書き直せるでしょうか？実は型変数に対して等価性の制約をすれば書き直せなくはないですが、少なくとも普通の定義の仕方では、

    :::Haskell
    data Exp = EInt Int | EBool Bool

という形になってしまって、うまく書き直せないかと思います。

GADTを使った定義の何がうれしいかというと、Expを作る元となった値の型が生き残っていることです。型が生き残っていれば、Haskellコンパイラが型を検査することができます。たとえば

    :::Haskell
    data Exp a where
      ...
      EAdd :: Exp Int -> Exp Int -> Exp Int

というデータコンストラクタを追加してやると、このEAddは`EBool True`といったExpを受け取らないので、おかしな式を作ることを防ぐことができます。なので、例外の扱いをしなくて良くなります。

## 関数をどうするか
GADTで問題になるのは関数の扱いです。

    :::Haskell
    data Exp a where
      ...
      EAbs  :: String -> Exp a -> Exp (b -> a)
      EApp  :: Exp (a -> b) -> Exp a -> Exp b
      EVar  :: String -> Exp a

という風に、これまでインタプリタを作るときに作ったようなデータ構造をそのまま作ってしまうと、引数はどんな型でないといけないかという情報が、`EAbs`を使うときに死んでしまいます。`(EAbs "x" (EAdd (EVar "x") (EInt 3))`という関数を作ったときに、`(EVar "x")`は`Exp Int`型でないといけないとは推論されますが、それは`EAbs`で関数抽象されてしまうと`Exp (b -> Int)`という型になってしまって、Intは無かったことにされて自由変数bにすりかえられています。

どうすればいいかというと、Haskellの型推論機に型の情報を伝えられるような形で関数を定義しないといけないので、それならHaskellの関数を`Exp`における関数ということにしてしまうしか無かろうということになります。これが、Higher-Order Abstract Syntaxです。

    :::Haskell
    data Exp a where
      ...
      EAbs   :: (Exp a -> Exp b) -> Exp (a -> b)
      EApp   :: Exp (a -> b) -> Exp a -> Exp b
      EPlace :: a -> Exp a -- スライドでの案2

    -- example
    plus3exp = EAbs (\x -> EAdd x (EInt 3))

しかし、この定義では以下の問題が発生します。

1.  EPlaceを使えば好きな型の値を作れてしまう
2.  関数を文字列として出力できない

後者の問題ですが、まあそもそもHaskellでは一般の関数を文字列として出力するなんてことはできません。じゃあどうするかというと、例えば適当な値を勝手に作って`EAbs`の元となる関数に渡してやって、生成された新しいExpを調べれば良さそうという気がします。たとえば、`(\x -> EAdd x (EInt 3))`に`EInt 1234`を適用してやれば`EAdd (EInt 1234) (EInt 3)`になるので、`EInt 1234`を適当な変数名に置き換えてやれば良さそうです。なおxという変数名は無くなってしまいますが、それはどうしたって諦めざるを得ません。

でも、実際はこれでは良くないのです。

-   引数に対してパターンマッチを行って中身を取り出して、中身に応じて処理するような関数を書かれているかもしれない
-   適当に作った値が他の値と被るかもしれない
-   Exp a型（aは任意の型に成り得る）を持つ値を生成することができない

という問題が存在します。個別の問題についてちゃんと書こうと思ったのですが、疲れるので飛ばします、すみません。

## PHOAS
ここで颯爽と登場するのがParametric Higher-Order Abstract Syntax(PHOAS)です。そういうことらしいです。Coqでプログラム変換が型を保持することを示すのに便利ということで論文が書かれていて、Haskellでも実装できるよというメールがHaskell-Cafeというメーリングリストに流れたらしいです（参考<http://d.hatena.ne.jp/keigoi/20081225/p1>）。完全に趣味ですね…。

以下、pprを実現する方法をネタバレするので、ネタバレ嫌な人は読まないでください。

    :::Haskell
    data Exp p a where
      EInt :: Int -> Exp p Int
      ...
      EAbs :: (p a -> Exp p b) -> Exp p (a -> b)
      EVar :: p a -> Exp p a
      ELet :: Exp p a -> (p a -> Exp p b) -> Exp p b

    type WFExp a = forall p. Exp p a

    newtype Identity a = Identity a
    runIdentity (Identity a) = a

    eval :: Exp Identity a -> a
    eval (EApp f e) = eval f (eval e)
    eval (EAbs f)   = eval . f . Identity
    eval (EVar v)   = runIdentity v

    -- 以下ppr関連
    -- この「適当な文字列だけを保持して、aに対しては何の制約もかけない型」を使うのが本質
    newtype Name a = Name String

    runName :: Name a -> String
    runName (Name s) = s

    -- NameGenの定義は手元で試していないのでtypoなどあるかもしれません。
    -- Intの値を状態として使うようなモナドです。
    newtype NameGen a = NameGen (Int -> (Int, a))
    instance Monad NameGen where
       m >>= a  = 略
       return a = 略

    runNameGen :: NameGen a -> a
    runNameGen (NameGen f) = f 0

    -- これだと変数名が数字になってしまって醜いので、ちゃんと文字列に変換する関数を定義したほうがいい
    -- NameGenが初めからIntでなくStringを保持するような実装でも当然問題ないし、inits (repeat ['a'..'z']) >>= sequence みたいなことして先に変数名の無限リスト作る感じでも問題ない
    fresh :: NameGen String
    fresh = NameGen (\i -> (i+1, show i))

    ppr :: Exp Name a -> String
    ppr = runNameGen . pprDo

    pprDo :: Exp Name a -> NameGen String
    pprDo (EAbs f) = do
      fv <- fresh
      argStr <- pprDo (EVar fv)
      expStr <- pprDo (f fv)
      return ("(lambda " ++ argStr ++ " " ++ expStr ++ ")") -- 慣れてる人は括弧でなく$使おう
    pprDo (EVar v) = return (runName v)

    -- example
    plus3exp :: WFExp Int
    plus3exp = EAbs (\x -> EAdd (EVar x) (EInt 3))

PHOASが普通のHOASと違うのは、`p`なる型変数が出てきたことです。`p`は、Expを構築する段階では、どんな具体的な型と同一化されることもありません。というか同一化されてはなりません。`WFExp`というのは、そのことを明示しやすくするために定義されている名前です（多分）。`forall`は「`p`はどんな型にも成り得る」くらいの意味で読めば良いです。ある式が`WFExp a`という型を持たなければいけないと指定することで`p`は具体的な型で置き換えられていないことを示すことができます。

---

捕捉、適当にマージしてもらってもいいです -- [[alpicola]] <<DateTime(2013-07-01T18:58:23+0900)>>

#### pprで`p`を`newtype P a = P String`のようなPhantom Typeにする理由

`EAbs`の整形というのは、仮引数を表す変数名と関数本体の式を出力すればよさそうですが、`EAbs`を構成している`f`は型`p a -> Exp p b`なので関数本体の式`Exp p b`を取りだすためには`f`に`p a`型を引数に与える必要があります。しかし、整形するときに引数になる具体的な`p a`型の値は、(実引数が与えられてくるevalのときと違って)普通に考えると与えることができないはずです。すなわち、`p a`型は`a`型の具体的な値なしに作れる値でなくてはなりません。これは型変数`a`をデータ構築子に用いないPhantom Typeにすれば解決します。 

----

続きの予定（ちゃんと書く気力があれば書く）

*   pに対して多相的なExpしか許さないことで任意の関数を書かせない
    *   引数は必ずEVarを使って導入される
*   pのkindは\*->*、要はpに入るのはパラメタライズされる前の型。で、EVarはp a型の値を受け取る。ppt関数の中でのpは、保持する値は実は変数を表示するために割り振るStringであるものの、形式的にどんな型でもパラメタライズされ得るようにしておけば、関数のpretty print可能。
*   

----
[[FLProgClassCategory]]