Hatena::Grouphaskell

[ pred x | x <- "Ibtlfmm!ojllj" ] RSSフィード

2012-07-10

型システム 08:19

http://www.cafepress.com/skicalc.6225368

Haskellの型システムはHindley-Milner型システムというものに型クラスを加えて拡張したものだそうだ。

一つの式は一つの静的な型を持つ。

GHCだと高階型(複数回ポリモーフする型)や暗黙引数や複数引数型クラスやGADTなどが加わってとても手に負えない有様になっている。

とりあえずHindley-Milnerというものを覚えることにした。

Haskellによる実装があるこの論文をもとにちょこちょこ検索しながら調べる。

出てくる式のようなものは自分の解釈で歪んでいる。記号で書いた日本語として適当に読んでほしい。

推論規則

例によってラムダ計算の式を考える。式の形は「変数参照」と「関数適用」と「関数作成」の3種類。

型システムというのは、下のような論理規則のこと。

[VAR] ((Γ ∪ {var : t}) |- var : t)
[APP] (Γ |- func : a → b) ∧ (Γ |- arg : a) ⇒ (Γ |- (func arg) : b)
[ABS] ((Γ ∪ {arg : a}) |- expr : b) ⇒ (Γ |- (λarg. expr) : a → b)

(Γ |- e : t) は「環境Γ下で式eが型tを持つ」という意味の述語。
Γは { foo : Int, sin : Real -> Real, True : Bool, False : Bool } のような変数名と型を対応づける辞書。
型は (型名) か (型) → (型) のどちらかの形。

これをそのまま実装しても 式 → 型 → Bool のようなチェックする関数が出来上がるだけで、型推論にはならない。

式から型を求めるアルゴリズムは別にあり、広義にはそれも含めてHindley-Milnerと呼ぶ。

let多相

上に載せた規則は不完全で、式も環境もすべて具体型ならいいのだが、id :: a -> a のような多相型(不確定な変数の残っている型)が作れない。

上に[LET]という規則を加えて色々拡張するとHindley-Milnerになる。*1

型ρは単相型τと多相型σのどちらか。
単相型τ は (型名) か τ → ρ のどちらかの形。
多相型 は ∀(型変数名). ρ の形。
関数の型は、引数の方は必ず単相だが、結果のほうの型は多相の可能性がある。

[LET] ((Γ ∪ {generic : σ}) |- expr : τ) ∧ (Γ |poly- generic : σ) ⇒ (Γ |- let generic = expr in body : τ)


ここで Γ |poly- expr : σ というのは |- と別の述語で、単相型ではなく多相型を決める。
|- のほうは単相型を扱う。

規則VARを多相に対応させるため拡張する。

[VAR'] (Γ ⊂ {var : σ}) ∧ (σ ≦ ρ) ⇒ (Γ |- var : ρ)

σ≦ρは「σはρと同じかそれ以上に多相である」ことを表す。

|poly- の定義は以下のとおり。

[SKOL] τ ≦ τ
[SPEC] (substitute(α, τ, σ1) ≦ σ2) ⇒  (∀α. σ1) ≦ σ2
[MONO] τ ≦ τ

[GEN] (α = freetypevariables(ρ) - freetypevariables(Γ))) ∧ (Γ |- expr : t) ⇒ (Γ |poly- expr : ∀α. t)
[INST] (Γ |- expr : ∀α. t) ∧ (τ is a monotype) ⇒ (Γ |- expr : substitute(α, τ, t))

freetypevariables(Γ) = ∪{ freetypevariables(t) | (x : t) ∈ Γ}
freetypevariables(∀α. τ) = freetypevariables(τ) - {α}
freetypevariables(τ) = τ (単相型)

substitute(α, τ, α) = τ
substitute(α, τ, β) = β
substitute(α, τ, x → y) = substitute(α, τ, x) → substitute(α, τ, y)

型の種類が増えて一気に複雑になった。よく見るとGENとINSTは無限ループできるので型推論がさらに難しくなる。

多相型(不確定な変数のある型)a -> aのことで、この規則では∀a. (a -> a)と書く。これは「1階の型」といって、aを与えるとそれが中に代入されて(substitute)0階の単相型になる。(このへんは暗黙)

*1ラムダ計算をSchemeから覚えた自分には「letは抽象+適用の構文糖のはずなのに?」と思えた。「副作用がないのでletをトップレベルdefineの代わりとして使っている」と考えると必要性がすこし飲み込みやすい

トラックバック - http://haskell.g.hatena.ne.jp/illillli/20120710

2012-07-07

19:40

またHaskellで遊びたくなったので再開します。

mtlが変わってる 01:21

Haskell Platformを入れてみたら、標準のモナドが様変わりしていた。

Control.Monad.Reader> Reader id
<interactive>:1:1: Not in scope: data constructor `Reader'

なんと、Reader、Writer、Stateすべてコンストラクタが軒並みなくなっている。

標準の同梱ライブラリ一覧のなかで、標準のモナドはこのあたり。

代わりになる関数はすべてクラスに取り込まれていた。

reader :: (MonadReader m r) => (r -> a) -> m a
writer :: (MonadWriter m w) => (a, w) -> m a
state :: (MonadState m s) => (s -> (a, s)) -> m a

ピュアな処理をモナドに入れるという変換に再解釈。

コンストラクタがなくなって、Stateなどのピュア版の定義はIdentityを使ったtypeエイリアスに置き換わった*1

type Reader r = ReaderT r Identity
type Writer w = WriterT w Identity
type State s = StateT s Identity
type Cont r = ContT r Identity

Contは半端にそのまま。

cont :: ((a -> r) -> r) -> Cont r a

ErrorTのピュア版のEitherは変化なし。

*1:typeは型引数残っててもよくなったのか

トラックバック - http://haskell.g.hatena.ne.jp/illillli/20120707

2009-06-13

WindowsのGHC 6.10.2でのGLUTバインディングのビルド 02:45

6.10になってからか、なぜかGHCOpenGLが付属しなくなった。

試してみたら(運よく)できたのでメモしておく。

clを使わなくともghcに付属のMinGW gccで出来ればいいと思うのだが、単純に試してもうまくいかなかった。

OpenGLバインディングをビルド

コマンドプロンプトでコンパイルする。

Platform SDKをC:\PROGRA~1\MIC977~1にインストールしたとする。

  • c:\program files\git\binにpathを通しておく
  • OpenGL.cabalに追記
extra-libraries: opengl32, glu32
extra-lib-dirs: C:\PROGRA~1\MIC977~1\Lib
extra-include-dirs: C:\PROGRA~1\MIC977~1\Include
  • runghc Setup.hs configure -p
  • runghc Setup.hs build
    • うまくいけばそれに越したことはない
  • buildがうまくいかなければ、include\HsOpenGLConfig.hに追記
    • 内容は検索して拾ってきたもの
#define HTYPE_GLBITFIELD Word32
#define HTYPE_GLBOOLEAN Word8
#define HTYPE_GLBYTE Int8
#define HTYPE_GLCLAMPD Double
#define HTYPE_GLCLAMPF Float
#define HTYPE_GLDOUBLE Double
#define HTYPE_GLENUM Word32
#define HTYPE_GLFLOAT Float
#define HTYPE_GLINT Int32
#define HTYPE_GLSHORT Int16
#define HTYPE_GLSIZEI Int32
#define HTYPE_GLUBYTE Word8
#define HTYPE_GLUINT Word32
#define HTYPE_GLUSHORT Word16
  • runghc Setup.hs install

GLUTバインディングをビルド

GLUTのバイナリはC:\local\glut-3.7.6-binに置いたものとする。

  • GLUT.cabalに追記 (行頭の空白含む)
  extra-libraries: glut32
  extra-lib-dirs: C:\local\glut-3.7.6-bin
  • runghc Setup.hs configure -p
  • runghc Setup.hs build
  • runghc Setup.hs install

うまくいってるか確認

GLUT-2.1.2.1\examples\RedBookにいろいろサンプルがあるのでrunghcしてみる。

トラックバック - http://haskell.g.hatena.ne.jp/illillli/20090613

2009-06-12

ベクトルの足し算をControl.Applicativeで 01:12

data Vector2 a = Vector2 a a deriving (Show, Eq)

こういう型をNumのinstanceにすることを考える。単純に書くとこうだ。

instance Num a => Num (Vector2 a) where
  Vector2 x y + Vector2 x' y' = Vector2 (x + x') (y + y')
  Vector2 x y - Vector2 x' y' = Vector2 (x - x') (y - y')
  Vector2 x y * Vector2 x' y' = Vector2 (x * x') (y * y')
  negate (Vector2 x y) = Vector2 (-x) (-y)
  abs (Vector2 x y) = Vector2 (abs x) (abs y)
  signum (Vector2 x y) = Vector2 (signum x) (signum y)
  fromInteger x = Vector2 (fromInteger x) (fromInteger x)

掛け算などの定義には突っ込まないでほしい。僕はVector 1 2 + Vector 3 4と書きたいだけなのだ。

上だけなら対した量ではないが、Vector3やVector4を実装するとなると、コピぺしていじる作業が辛くなってくる。

この状況を改善したい。

fmapを使う

fmapを使うとすこし楽になる。

instance Functor Vector2 where
  fmap f (Vector2 x y) = Vector2 (f x) (f y)

instance Num a => Num (Vector2 a) where
  Vector2 x y + Vector2 x' y' = Vector2 (x + x') (y + y')
  Vector2 x y - Vector2 x' y' = Vector2 (x - x') (y - y')
  Vector2 x y * Vector2 x' y' = Vector2 (x * x') (y * y')
  negate = fmap negate
  abs = fmap abs
  signum = fmap signum
  fromInteger x = fmap fromInteger (Vector2 x x)

とはいえ、足し算や引き算は変わらない。

fmap2がほしい

パターンはこうだ。

Vector2 x y `op` Vector2 x' y' = Vector2 (x `op` x') (y `op` y')

そのままこれを関数とするとこうなる。

op :: (a -> b -> c) -> Vector2 a -> Vector2 b -> Vector2 c
op f (Vector2 x y) (Vector2 x' y') = Vector2 (x `f` x') (y `f` y')

これを使うとこう定義できる。

instance Num a => Num (Vector2 a) where
  (+) = op (+)
  (-) = op (-)
  (*) = op (*)
  negate = fmap negate
  abs = fmap abs
  signum = fmap signum
  fromInteger x = fmap fromInteger (Vector2 x x)

opはfmapの二引数関数用と言ってもいい。こういうクラスと関数があってもいいはずだ。

class Functor2 f where
  fmap2 :: (a -> b -> c) -> f a -> f b -> f c

-- で

instance Functor2 Vector2 where
  fmap2 = op

instance Num a => Num (Vector2 a) where
  (+) = fmap2 (+)
  (-) = fmap2 (-)
  (*) = fmap2 (*)
  negate = fmap negate
  abs = fmap abs
  signum = fmap signum
  fromInteger x = fmap fromInteger (Vector2 x x)

fmap2は標準に含まれていない。

liftA2

fmap2は無いが、幸いなことにControl.Applicativeで用が足りる。

liftA2 :: (Applicative f) => (a -> b -> c) -> f a -> f b -> f c

つまり、Vector2をApplicativeのinstanceにすればこの関数が使える。


instance Applicative Vector2 where
  pure x = Vector2 x x
  Vector2 fx fy <*> Vector2 x y = Vector2 (fx x) (fy y)

instance Functor Vector2 where
  fmap = liftA

instance Num a => Num (Vector2 a) where
   (+) = liftA2 (+)
   (-) = liftA2 (-)
   (*) = liftA2 (*)
   negate = fmap negate
   abs = fmap abs
   signum = fmap signum
   fromInteger = pure . fromInteger

これで重複が少なくなり、コピペしやすいコードになった。(ついでにfromIntegerpureで書き換えた)

liftA2Fractionalの実装にもそのまま使える。

instance (Fractional a) => Fractional (Vector2 a) where
   (/) = liftA2 (/)
   recip = fmap recip
   fromRational = pure . fromRational

副産物

ここまで実装すると不思議なことが起こる。Vectorが割れるのだ。

GHCi, version 6.10.2: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( va.hs, interpreted )
Ok, modules loaded: Main.
*Main> Vector2 3 4 / 5
Vector2 0.6 0.8
*Main> Vector2 3 4 * 3
Vector2 9 12

これは数字リテラルがオーバーロードされていることによる。

*Main> :t 5
5 :: (Num t) => t
*Main> 5 :: Vector2 Int
Vector2 5 5

こちらはすこし気持ち悪いかもしれない。

*Main> Vector2 1.5 2 + (-3.2)
Vector2 (-1.7000000000000002) (-1.2000000000000002)
*Main> Vector2 (-3) 1.9 - 4
Vector2 (-7.0) (-2.1)
トラックバック - http://haskell.g.hatena.ne.jp/illillli/20090612

2009-06-07

Control.MonadをApplicativeで 16:50

d:id:Otter_O:20080301:1204363038を見て、Control.Monadにあるユーティリティ関数をApplicativeで書き換えてみた。

21個中15個を書き換えることが出来た。

(=<<) :: Monad m => (a -> m b) -> m a -> m b
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c
join :: Monad m => m (m a) -> m a
foldM :: Monad m => (a -> b -> m a) -> a -> [b] -> m a
foldM_ :: Monad m => (a -> b -> m a) -> a -> [b] -> m ()

これらは実行の結果を受け渡す機能が必要なので実装できなかった。

Otter_OOtter_O2009/06/09 15:15参考にしていただいて、ありがとうございます。

こうやって見るとMonadとApplicativeの違いが浮き彫りになるようにも見えますね…
クラスメソッドレベルではこうした違いが見えているのに、モナドのインスタンス型であるIO, Maybe, Listなどそれぞれ実はApplicativeのインスタンスであるところもなんだか不思議です。

Control.Monad.apがMonadな型のApplicative.<*>のインプリメンテーションに使われているので、Applicativeが要求しているのはモナドに格納されている中身の型のほうで、MonadとApplicaiveとの間では根本的な不適合は無いようにも見えますね…


これからもよろしくどうぞ。

illillliillillli2009/06/13 00:38いつも面白く読ませていただいています。

結局 join :: m (m a) -> m a があればApplicativeとモナドは同じ機能を持つことになりそうです。
公式のメーリングリストのほうで「最適化したいので *> :: f a -> f b -> f b をApplicativeのクラスメソッドに含めて欲しい」という話が出ていました。
モナドのほうでも最適化のために >> がクラスメソッドに含められているので、この点でも似ている/同じ使われ方をされているのだろうと思います。

トラックバック - http://haskell.g.hatena.ne.jp/illillli/20090607