haskell-jp / questions #28

:cry:

メモリエラーという事はスペースリークかもしれないので、ソース晒せば誰か直してくれるかも

あ、すでに晒してます https://haskell-jp.slack.com/files/U4L0B71L1/FD1666PLL/

こっちはTLEですね…リストとマップを配列とハッシュマップに直せば行けるのか、ロジック直さないと駄目なのか

リストとマップを配列とハッシュマップに直せば行けるのか、ロジック直さないと駄目なのか

そう ここが分かってない
競プロガチ勢なら制約とオーダーと制限時間見てこのアルゴリズムで行けるか分かるんでしょうけど

"Testcase 1" で Out of memory になるソースはこちらです　``` {-# LANGUAGE FlexibleInstances, UndecidableInstances, DuplicateRecordFields #-}
module Main where
import Control.Monad
import Data.Array
import Data.List
import System.Environment
import

substringDiff k s1 s2 = bsearch 1 (min n1 n2) f
where
n1 = length s1
n2 = length s2
ar1 = listArray (1,n1) s1
ar2 = listArray (1,n2) s2
ar = array ((0,0),(n1,n2)) $ ((0,0),0):
[((i,0),0) | i <- [1..n1]] ++ [((0,j),0) | j <- [1..n2]] ++
[((i,j),ar!(i-1,j-1) + if ar1!i == ar2!j then 0 else 1) | i <- [1..n1], j <- [1..n2]]
f x = or [ar!(i,j) - ar!(i-x,j-x) <= k | i <- [x..n1], j <- [x..n2], x <= min i j]

bsearch l r p
| l >= r = l
| p m = bsearch m r p
| otherwise = bsearch l (m-1) p
where m = (l+r+1) `div` 2

main :: IO()
main = do
stdout <- getEnv "OUTPUT_PATH"
fptr <- openFile stdout WriteMode
t <- readLn :: IO Int
forM_ [1..t] $ \t_itr -> do
kS1S2Temp <- getLine
let kS1S2 = words kS1S2Temp
let k = read (kS1S2 !! 0) :: Int
let s1 = kS1S2 !! 1
let s2 = kS1S2 !! 2
let result = substringDiff k s1 s2
hPutStrLn fptr $ show result
hFlush fptr
hClose fptr
```

@takumaw has joined the channel

[HERP]()
という会社がHaskellとYesod使っているということを知って興味を持ったので
月曜日に話を聞きに行く予定なのですが
haskell-jpのメンバーにここの社員居たりしますかね

プロファイル取ってみました。arのメモリ使用量削減が課題ですかね。

おもむろにUnboxed Arrayに変えてみたら、arの右辺でarを使う所で無限ループになりました。Mutable Arrayを使うか、kakkun61さんのようにMemoモナドを使う必要がある模様

これで18MBまで減りました。

もう終わった話題だったら申し訳ないんですが、kakkun61さんのコードもタプルをStrictなタプルに変えるとか、適当なところでBangPatternsを使うだけで大分改善されそうな気がします。
（ちょっと試せてないんですが、忘れないうちに。。。）

よくよく考えなおしたら　最長解の探索の時に　一つのづれ毎に　２次元テーブルの対角方向しか使っていないので　このテーブルは不要でした　下記のコードで AC になりました　as_capabl さんお勧めの Unboxed Array も使いました　皆さんありがとうございました　　``` {-# LANGUAGE FlexibleInstances, UndecidableInstances, DuplicateRecordFields #-}
module Main where
import Control.Monad
import
import Data.Array.Unboxed
import
import Data.List
import System.Environment
import

substringDiff k s1 s2 = maximum $ g <$> [1-n2..n1-1]
where
n1 = length s1
n2 = length s2
ar1 = listArray (1,n1) s1 :: UArray Int Char
ar2 = listArray (1,n2) s2 :: UArray Int Char
mn = min n1 n2
df = abs (n1-n2)
g y = bsearch 1 n f
where
(i,j) = (max 1 (1+y),max 1 (1-y))
n | n1>n2 = if y-df>0 then mn-y+df else mn+min 0 y
| n1<n2 = if y+df<0 then mn+y-df else mn-max 0 y
| True = mn - abs y
ar :: UArray Int Int
ar = runSTUArray $ do
arM <- newArray_ (0,n)
writeArray arM 0 0
forM_ [1..n] $ \x -> do
prev <- readArray arM (x-1)
writeArray arM x $ prev + if ar1!(i+x-1) == ar2!(j+x-1) then 0 else 1
return arM
f x = or [ar!i - ar!(i-x) <= k | i <- [x..n]]

bsearch l r p
| l >= r = l
| p m = bsearch m r p
| otherwise = bsearch l (m-1) p
where m = (l+r+1) `div` 2

main :: IO()
main = do
stdout <- getEnv "OUTPUT_PATH"
fptr <- openFile stdout WriteMode
t <- readLn :: IO Int
forM_ [1..t] $ \t_itr -> do
kS1S2Temp <- getLine
let kS1S2 = words kS1S2Temp
let k = read (kS1S2 !! 0) :: Int
let s1 = kS1S2 !! 1
let s2 = kS1S2 !! 2
let result = substringDiff k s1 s2
hPutStrLn fptr $ show result
hFlush fptr
hClose fptr
```

難しそうな質問ですみません。HIW 2018にあった
https://icfp18.sigplan.org/event/hiw-2018-papers-coercion-quantification
こちらの発表の内容を理解しようとしているんですが、
出てくる「homogeneous equality」「heterogeneous equality」というキーワードがさっぱりわからず、困っております。
既存の a ~ b ともまた違うっぽいんですが、どう違うんでしょうか？

homogeneous equality, which means equality is between types of a same kind

だから，同一kindでの関係か異なるkindでの関係かでは？

「異なるkindだけど等しい」という状態がどんな状態なのかちょっとイメージがわかないです。。。 :sweat:

依存型を用いて長さを型やら種レベルに持つコンテナ X があって，さらにそれに交換則を満たすような結合操作が入っているときに，実際に交換して結合した2つのコンテナの値(型)の型(種)は X (a+b) と X (b+a) みたいなものが出てきますが，たとえばこれらのequalityが扱えないことがあるみたいな話ではないですか．

http://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Equality.html ここにhomogeniousな :~: とheterogeniousな :~~: がそれぞれ定義されていますね。後者がなぜ必要なのか、私も理解できてないですが一応。

HReflでパターンマッチすれば同じ型(必然的に同じkind)になるけど、マッチ前は異なるkindの型を両辺に書ける、って感じなのか

https://icfp18.sigplan.org/event/hiw-2018-papers-coercion-quantification に張ってあるスライドの17ページに例がありました（スライドのPDFファイルへの直リンはしにくくなってますね。。。）
ややでっち上げた例のようにも感じられますが、

data Rep :: forall k. k -> Type where
  RepBool :: Rep Bool
  RepMaybe :: Rep Maybe

みたいな、任意のkindを内包できる型があった場合に、
Rep Bool と Rep Maybe の（型レベルでの）等値性を比較したい場合に kind errorになってしまう、という例です。

ちなみに、依存型の世界だと heterogenious equality (John Major’s equality) は K を含意するので、通常の homogeneous equality よりも真に強いです。

a :~: b -> a :: b が axiom K を含意する、の方が正確なような気がします

というか a :~: b -> a :~~: b は成り立つのに対して a :~~: b -> a :~: b は成り立たないので heterogenious equality のほうが弱い、といえると私は認識していたんですがこれであってますよね……？

ちょっと誤解していたんですが a :~~: b -> a :~: b が成り立たないのは Coq においてで、 Haskell では成り立つみたいです。ｽﾐﾏｾﾝ

自分の言っているのは体系の強さの意味です。
通常の除去規則(J)を持つ通常の homogeneous な propositional equality と、 John Major’s equality を比べると、後者を持つ体系で前者は自明に定義できて更にKやUIP(Uniqueness of identity proof)等を満たすのに対して、前者しかない体系で後者を定義することは出来ないです(ただしKもしくはUIPもしくは制限のないパターンマッチがあれば定義できる)。

CoqはKやUIPを前提としない体系(Agdaでの --without-K な状態)なので、 John Major’s equality は Axiom を使って定義されているはずです。 John Major’s equality の除去規則(とその計算規則?)を Axiom にすれば a :~~: b -> a :~: b は証明できるはずですが、何らかの事情で別の定義を使っているのかも知れません。

最近ちまちま読んでた論文にも、良く見るとその辺の話めっちゃ出てきてました。 https://arxiv.org/abs/1610.07978 モチベーションとして3.2節で　<@U4LGTMTMK> さんが挙げたような例が出てきて、論理的裏付けとして5章で @hexirp さんや @msakai さんが挙げてるような話が書いてあるっぽい

というか著者＝発表者だ

Haskell の話からはかなり脱線してしまいますが、 John Major’s equality の除去規則から 通常の propositional equality の K と UIP を示すのを Agda で書いてみました。 https://gist.github.com/msakai/b3f3003b1ec900b84c0e5c6e5315c90b

Haskell では homogeneous equality を表す型クラス a ~ b は heterogeneous equality を表す型クラス a ~~ b を使って class (a ~~ b) => (a :: k) ~ (b :: k) と定義されていますね。型クラスでは、もしインスタンスがあればそれは一意なので UIP は当然のことといえるかも？a :~: b と a :~~: b の間にはこういう関係はないです。

@Yugo Osano has joined the channel

仕様と、上手く動かなかったプログラムを添付します。どうしても回数が多いのでOverflowするのと、計算精度が良くないようで結果もおかしな感じとなります。すいませんが、ご教示お願い致します。

{-# LANGUAGE Strict #-}
import System.Environment

qnr :: Double -> Double -> Double -> Double
qnr n r 0 = 0
qnr n r p
  | n < r     = 0
  | n == r    = q
  | otherwise = q + (n-r)*(log(1-p)) + (foldl (+) 0 (map log [n-r+1..n])) - (foldl (+) 0 (map log [2..r]))
  where q = r * (log p)

exp_qnr :: Double -> Double -> Double -> Double
exp_qnr n r p = exp (qnr n r p)

pnr :: Double -> Double -> Double -> Double
pnr n r 0 = 0
pnr n r p
  | n < r     = 0
  | n == r    = exp q
  | otherwise = (pnr (n-1) r p) + (1 - (pnr (n-1) r p))*(exp_qnr n r p)
  where q = r * (log p)

main = do
  args <- getArgs
  (n,r,p) <- case args of
    n':r':p':_ -> (,,) <$> readIO n' <*> readIO r' <*> readIO p'
    _ -> return (6400, 64, 0.8)
  -- putStrLn $ "qnr " ++ show n ++ " " ++ show r ++ " " ++ show p ++ " = " ++ show (exp_qnr n r p)
  putStrLn $ "pnr " ++ show n ++ " " ++ show r ++ " " ++ show p ++ " = " ++ show (pnr n r p)

ソースコードの部分はバッククォート3つで囲っていただけると助かります！

こういう風に
  行頭の
  空白も保存されるので！

参考: https://get.slack.help/hc/ja/articles/202288908-%E3%83%A1%E3%83%83%E3%82%BB%E3%83%BC%E3%82%B8%E3%81%AE%E6%9B%B8%E5%BC%8F%E8%A8%AD%E5%AE%9A#u12452u12531u12521u12452u12531u12467u12540u12489

直観主義型理論でも、 propositional equality はデータ構築子が一つしかないにも関わらず、UIPは証明できないので、この場合もインスタンスの一意性があるからといって自明ではないような気はしますが……

ただ、Haskellでは以下の定義は通るようですね。 (Haskellの型レベルプログラミングに詳しくないので適当ですが)

type family UIP a (x :: a) (e :: x :~: x) :: e :~: Refl where
  UIP a x Refl = Refl

依存型を用いて長さを型やら種レベルに持つコンテナ X があって，

多次元配列の型付けで必要になる、お仕事っぽい話だ…… (^^;

引数の一部を整数にしてみました https://gist.github.com/naohaq/281aebb3f29378109bb4f866e5068ef8

漸化式を修正したバージョン https://gist.github.com/naohaq/281aebb3f29378109bb4f866e5068ef8/2c348a0056fa6977e681f2a31b5ccf5e905c5a89

:innocent:

この式は全然わからないけど、

(foldl (+) 0 (map log [n-r+1..n]))

これは次のように書くと計算量は減るんじゃないかな（あと正格foldlも使ってる

foldl' (\acc num -> log num + acc) 0 [n-r+1..n]

@algebroid has joined the channel

ghcで書いたプログラムを
pythonで動かしたいです
jsへのコンパイラはいろいろありますが
pythonに変換するものはありますか？

多分ないです。少なくとも私は聞いたことがありません。
そもそもどういう動機でPythonに変換したいんですか？AWS Lambdaで動かすとか？

動かしたいだけなら FFI で shared object に変換して，python側で import ctypes から呼び出すのがてっとり早いのではないかと思います．

pythonでグラフを表示したいのですが、
今はpythonからpopenしてhaskellで作ったコマンドを呼び出しています。（呼び出しスピードとか気にしてないです）
インストールが面倒でwheelに実行コマンドを含めようかと思ってました。
用途してはこれで十分なのですが、OS別にバイナリをつくるのがそれはそれで面倒で、どうしたものかと。
大したものではないのでpythonで書き直しも考えております。

Data.List.delete って、最初にマッチした要素しか消してくれないのですね。マッチする全部の要素を取り除く関数ってありませんか？

代わりに Data.List.filter を使うのはどうでしょう

それって filter のような気がしますが、汎用的ではない特定の要素を全消しする専用の関数を探しているということです？

あ、かぶった・・・

あー、filter でいいのか。ありがとうございます！