PPL2009 のみかいにて

Haskell OCaml

マジメな話は省略、主に自分の話だけメモ

飲み会は2日目だけ参加しました。

  • kinabaさん→id:osiire さん、 「リストの重複を省く関数(多相的)を作るときに Setモジュールが使えない」
    • OCaml の Set モジュールが多相的に使えない問題。
let uniq xs cmp = 
  let module ASet = Set.Make (
    struct
      type t = 'a (* 'a is unbound *)
      let compare = cmp
    end)
  in ASet.elements (List.fold_right ASet.add xs ASet.empty);;
  • OCaml には scoped type variable がないから駄目なんじゃね？
    • class の 型引数を scoped type variable として使えない？
    • ムリポ
class ['a] dummy =
  object 
    method uniq xs cmp = 
      let module ASet = Set.Make (
        struct
          type t = 'a (* 'a is still unbound *)
          let compare = cmp
        end)
      in ASet.elements (List.fold_right ASet.add xs ASet.empty)
  end;;
  • 私のスライドの未発表部分についてkinabaさん、東大の人たちとさかいさんに披露した。反応：
    • こういう型クラスを使ったテクニックはやっぱり黒魔術
    • type class の型プログラミングは Prolog っぽいのに微妙に異なるところがあり使いにくい
    • FunDepsはうまく型を refineしてくれないことがあるよね (以下さかいさんより)
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}
class F x y | x -> y
instance F Int Int

t :: F Int x => x
t = 0 :: Int

-- fundeptest.hs:6:4:
--     Couldn't match expected type `x' against inferred type `Int'
--       `x' is a rigid type variable bound by
--           the type signature for `t' at fundeptest.hs:5:11
--     In the expression: 0 :: Int
--     In the definition of `t': t = 0 :: Int
  • 簡単な flow-sensitive な型を OCaml で 実装している ガリグ先生の caml-list への投稿 ... を Haskell でまねしようとした。
    • Ch (Cons a tl, Cons b tl) (a,b) みたいな型を書いたら、さかいさんに「(HListを)空気のように使いこなしてますね」と呆れられた。
    • だいたいは同じように実装できそうだったが最後の最後で show . read の問題みたいな型エラー。 Haskell チーム敗北。 ガリグ先生の笑いがこだまする中、私の意識は眠りへと沈みゆくのであった。
{-# LANGUAGE NoMonomorphismRestriction, EmptyDataDecls, FlexibleInstances #-}

-- type level list
data Nil
data Cons a ts

-- state
data Closed
data Input; data Output

data M i i' a -- indexed monad

-- channel type
data Ch a b

class AllClosed ts
instance AllClosed Nil
instance AllClosed ts => AllClosed (Cons Closed ts)

class Active a
instance Active Input
instance Active Output

-- channel constant
ch1 :: Ch (Cons a tl, Cons b tl) (a,b)
ch1 = undefined

-- create a new channel (statically)
succ_ :: Ch (a, b) c -> Ch (Cons d a, Cons d b) c
succ_ = undefined

ch2 = succ_ ch1

open_in :: Ch (x,y) (Closed,Input) -> String -> M x y ()
open_in = undefined

input :: Ch (x,y) (Input,Input) -> M x y String
input = undefined

close :: Active a => Ch (x,y) (a,Closed) -> M x y ()
close = undefined

bind :: M x y a -> (a -> M y z b) -> M x z b
bind = undefined

($$) :: M x y a -> M y z b -> M x z b
($$) = undefined

run ::  (AllClosed x) => M x x a -> IO a
run = undefined

start :: AllClosed x => M x x a
start = undefined 

test =
  open_in ch1 "hoge.txt" $$ input ch1 $$ close ch1

-- cannot be typed!
-- _ = run test
-- 
-- haskell-io-spec.hs:55:8:
--     Ambiguous type variable `x' in the constraint:
--       `AllClosed x'
--         arising from a use of `test' at haskell-io-spec.hs:55:8-11
--     Probable fix: add a type signature that fixes these type variable(s)
-- Failed, modules loaded: none.