haskell-jp / questions #66

型の上で計算するだけで終わりにしていいのならそのように大概のことはできるんですが,今やろうとしているのは証明であり,値レベルで云々する(≒singletonsとかでゴニョゴニョする)必要があります.たとえば,
sNatToNat' :: Sing n -> Sing (ConvertNat n)
sNat'ToNat :: Sing (ConvertNat n) -> Sing n

みたいな部品が必要になると思いますが,コレを定義してやろうとすると正攻法では詰むと思います.
@shunkichi.sato has joined the channel
@woodsondelhia88 has joined the channel
@ogahiro0720 has joined the channel
@yama_aoi has joined the channel
@cj.bc-sd has joined the channel
@wuthering1118 has joined the channel
@k.kent8192 has joined the channel
@drmaruyama has joined the channel
質問です :raising_hand:
cassavaを使ってCSV をパースした結果をextensibleのRecordにしようとしてるのですが
readCSV :: WrapForall Csv.FromField Vector xs => FilePath -> IO (RecordOf Vector xs)
readCSV filepath = do
    csvBs <- BL.readFile filepath
    case Csv.decode Csv.HasHeader csvBs :: Either String (Vector (Record xs)) of
        Left reason -> error reason
        Right vs -> undefined

以下のような感じでカインドが合わないと怒られてしまいます…
....hs:36:82: error:
    • Expected kind '[membership-0:Type.Membership.Internal.Assoc
                        k0 *]',
        but 'xs' has kind '[*]'
    • In the second argument of 'RecordOf', namely 'xs'
      In the first argument of 'IO', namely '(RecordOf Vector xs)'
      In the type signature:
        readCSV :: WrapForall Csv.FromField Vector xs =>
                   FilePath -> IO (RecordOf Vector xs)
   |
36 | readCSV :: WrapForall Csv.FromField Vector xs => FilePath -> IO (RecordOf Vector xs)
   |   

どなたか対処方法を教えていただけませんでしょうか :bow:
@igrep
{-# LANGUAGE PolyKinds #-}

試したけどできず…
WrapForall Csv.FromField Vectorがxsの種を [*] に固定する原因となっています。 Forall (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xsとしてはどうでしょう
@fumieval ありがとうございます!今度は以下のようなエラーメッセージになりました:bow:
....hs:30:125: error:
    • Expected kind '[membership-0:Type.Membership.Internal.Assoc
                        * *]',
        but 'xs' has kind '[membership-0:Type.Membership.Internal.Assoc
                              ghc-prim-0.5.3:GHC.Types.Symbol *]'
    • In the first argument of 'DataFrame', namely 'xs'
      In the first argument of 'IO', namely '(DataFrame xs)'
      In the type signature:
        readCSV :: Forall (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs =>
                   FilePath -> IO (DataFrame xs)
今度こそPolyKinds事案に見えますね… :thinking_face:
PolyKindsを入れたらエラーが変わりました…! :pray:
readCSV :: Forall (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs => FilePath -> IO (RecordOf Vector xs)
readCSV filepath = do
    csvBs <- BL.readFile filepath
    case Csv.decode Csv.HasHeader csvBs :: Either String (Vector (Record xs)) of
        Left reason -> error reason
        Right vs -> undefined


...hs:52:10: error:
    • Could not deduce (Forall
                          (Instance1 Csv.FromField (Field Identity)) xs1)
        arising from a use of 'Csv.decode'
      from the context: Forall
                          (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs
        bound by the type signature for:
                   readCSV :: forall (xs :: [membership-0:Type.Membership.Internal.Assoc
                                               ghc-prim-0.5.3:GHC.Types.Symbol *]).
                              Forall
                                (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs =>
                              FilePath -> IO (RecordOf Vector xs)
        at src/Data/Frame/Reader.hs:49:1-115
    • In the expression:
          Csv.decode Csv.HasHeader csvBs ::
            Either String (Vector (Record xs))
      In a stmt of a 'do' block:
        case  Csv.decode Csv.HasHeader csvBs ::
                Either String (Vector (Record xs))
        of
          Left reason -> error reason
          Right vs -> undefined
      In the expression:
        do csvBs <- BL.readFile filepath
           case  Csv.decode Csv.HasHeader csvBs ::
                   Either String (Vector (Record xs))
           of
             Left reason -> error reason
             Right vs -> undefined
   |
52 |     case Csv.decode Csv.HasHeader csvBs :: Either String (Vector (Record xs)) of
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
インスタンスの導出が出来てない… :thinking_face:
ScopedTypeVariablesとRankNTypesでxsを束縛していないような雰囲気…?
あ、LANGUAGEも含めて貼りますね :bow:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Data.Frame.Reader where

import qualified Data.ByteString.Lazy as BL

import qualified Data.Csv as Csv
import Data.Extensible 
import Data.Vector (Vector)

readCSV :: forall xs. Forall (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs => FilePath -> IO (RecordOf Vector xs)
readCSV filepath = do
    csvBs <- BL.readFile filepath
    case Csv.decode Csv.HasHeader csvBs :: Either String (Vector (Record xs)) of
        Left reason -> error reason
        Right vs -> undefined


.hs:19:10: error:
    • Could not deduce (Forall
                          (Instance1 Csv.FromField (Field Identity)) xs)
        arising from a use of 'Csv.decode'
      from the context: Forall
                          (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs
        bound by the type signature for:
                   readCSV :: forall (xs :: [Assoc
                                               ghc-prim-0.5.3:GHC.Types.Symbol *]).
                              Forall
                                (KeyValue KnownSymbol (Instance1 Csv.FromField Vector)) xs =>
                              FilePath -> IO (RecordOf Vector xs)
        at src/Data/Frame/Reader.hs:16:1-126
    • In the expression:
          Csv.decode Csv.HasHeader csvBs ::
            Either String (Vector (Record xs))
      In a stmt of a 'do' block:
        case  Csv.decode Csv.HasHeader csvBs ::
                Either String (Vector (Record xs))
        of
          Left reason -> error reason
          Right vs -> undefined
      In the expression:
        do csvBs <- BL.readFile filepath
           case  Csv.decode Csv.HasHeader csvBs ::
                   Either String (Vector (Record xs))
           of
             Left reason -> error reason
             Right vs -> undefined
現状このような感じです!
ああ、無名のレコードと互換性がないと言うだけのことでした!こんな感じにすると通ります
readCSV :: forall xs. Forall (KeyValue KnownSymbol (Instance1 Csv.FromField Identity)) xs => FilePath -> IO (RecordOf Vector xs)
readCSV filepath = do
    csvBs <- BL.readFile filepath
    case Csv.decodeByName csvBs :: Either String (Csv.Header, Vector (Record xs)) of
        Left reason -> error reason
        Right vs -> undefined
通りました!!
そうか、インスタンスにするべきは Vector じゃなくて Identity とだったんですね。
いただいたコードを参考にしながら勉強します :pray:
ありがとうございました :bow:
なるほど!
FromRecord と FromNamedRecord の差ですか…!
https://gyazo.com/59a3a33419ebec83181cf24c6d42c972

今パースしたいCSV、ヘッダーついてないんですよね… :sweat_smile:
CSVのByteStringの頭に無理やりヘッダー行追加するか :thinking_face:
なるほど…その場合こんな感じですかね ```readCSV :: forall xs. (Forall (Instance1 Csv.FromField (Field Identity)) xs) => FilePath -> IO (RecordOf Vector xs)
readCSV filepath = do
csvBs <- BL.readFile filepath
case Csv.decode Csv.HasHeader csvBs :: Either String (Vector (Record xs)) of
Left reason -> error reason
Right vs -> undefined
```
すごい!!出来るんですね!!
型クラス制約の定義読んで勉強します :sob: :arigatougozaimasu:
(手元でもコンパイル通りました!! :bow: )
@gan13027830 has joined the channel
@nnhixi has joined the channel
alliswellthatendswell
@alliswellthatendswell has joined the channel
定作用形についてブログ書くかと書いてたら分からなくなってきました
fact3 :: Int -> Integer
fact3 = (map fact' [0..] !!)
  where
    fact' 0 = 1
    fact' n = fromIntegral n * fact' (n-1)

fact3 はなんで CAF なんでしょう? map は定数でもなければコンビネーターでもない変数なような……
https://kakkun61.hatenablog.com/entry/2019/07/29/%E9%96%A2%E6%95%B0%E3%81%AE%E3%83%A1%E3%83%A2%E5%8C%96
@dusty.trombone has joined the channel
CAFかどうかと関係あるかわからない、かつ自信がないので元記事のコメントではなくここで。
ちょうど途中まで読んでたこの話 https://treszkai.github.io/2019/07/13/haskell-eval がすごく関係ありそうな気がします。
スーパーコンビネータは,一般の文脈では確かにコンビネータで部分項がスーパーコンビネータであるものを指しますが, CAF の文脈では,
• ラムダ式でない
• ローカル関数が全てグローバルに出しても問題ない定義になっている
だと思うのが良いと思います.厳密には,
https://gitlab.haskell.org/ghc/ghc/wikis/commentary/rts/storage/gc/CAFs
に書いてある通り,要はサンクとなる static closure のことを指しています.

ところでメモ化の要因は,確かに fact3 が CAF であることもありますが,一番の要因として, Core では関数適用の引数は let を通して変数に束縛されることになるので,実際にはこのプログラムは
fact3 = (!!) fact3'
   where
       fact3' = map fact' l
       l = [0..]
       fact' 0 = 1
       fact' n = ...

みたいなものと等価になります (厳密にはこれも怪しいですが) .で, fact3' が CAF となるからというのが大きいですね (なお実際 GHC 8.6.5 では fact3' が floating out されていて, fact3 自体は最終的に eta expand されて fact3 = \x -> (!!) fact3' x という形になっていました)
はっきりと質問というわけでもないですがrandomよりは質問よりなのでこちらで。 ghc でアノテーション(カスタムアノテーションも含む)が削除されるタイミングっていつなんですかね? Cmmの段階まで保持されるんですかね?
あ、これ色々質問が間違ってるや。 そもそも アノテーションではなくプラグマだし。 一般のプラグマに関しては言及不可なやつでしたね。。。すみません。 質問の意図としては。 たとえばLiquid Haskell を用いて ある評価木の一部(またはすべて)の範囲で値が一定の範囲収まるといった情報を知った上でレジスタの配置とかそういった最適化(?)みたいなのができるのかなと思い質問しました。
これをめっちゃざっくりJSで例えてみました。
https://gist.github.com/igrep/afcf4789d88da3b3995308e2e12c59df
要するに、メモ化に使うリストをラムダ式の中で定義するか、外で定義してキャッシュするか、という違いですよね?
:point_up: スレッドへの返信でGistを張っただけなのにこっちにも出てくるのか... 驚かせてたらすみません。 :bow:
違うような
(意味論上は同じにもかかわらず)中で定義しても、形によってキャッシュされたりされなかったりという違いかと
理論上は参照透過だから一度計算したものは全部保存してもいいんだけど、現実はメモリーの制約があるから基本的には捨てていて、ただ CAF の形式のときは保存している、という話だと認識している
すみません、付け加えた言葉がまずかった。「JavaScriptで強引に例えるならあたかも外で定義してキャッシュするかのように振る舞う(Haskellの場合実際には、最初に呼ばれたときにキャッシュされる)」みたいなことを言いたかった。
外で定義して、っていうか fact3 を定義したときに、というべきか。
少し修正して実態に近づけてみた
@niszet0016 has joined the channel
この辺の分かりやすい説明はHaskell High Perfomance Programmingのchaper 1に書いてあります.
blog記事にも出てたので持っている前提で書きますがp8です.

fib_memとfib_mem_argとを比較して
「map fib [0..]は引数に依存せずメモ化することが可能だけれど関数に引数を適用すると暗黙のうちに以前の関数適用からの式へのポインタを持つことができない新しい式を作ってしまうからです」
つまりwhereで定義しているローカル関数fibはfib_memにぶら下がっているのに対してfib_mem_argの方はfib_mem_arg n(というnに適用した式)に対してローカル関数fibがぶらさがっている.つまりnが適用される都度別のfibになるとみなすとよい(のかな).
結果としてmap fib [0..]のfibは毎度違ってしまう.
CAFsがポイントになるのは結局トップレベルにリフトできるからで,トップレベルから掴んでいられるから評価が進めばサンクが潰れて値に置き換わって再利用できるということで,fib_mem_argのようにトップレベルに着地できうに宙に浮いてしまってたら一度評価したものも失われるのでメモ化されない.
逆に言えばメモリを解放する手段がないわけだからメモリリーク(と言っていいのかどうかいまだに私は迷うのだけど)している.
なので速度は出るけどメモリは食い続ける一方でGCできないはず.
というわけで,やっぱりtabulationするのが一番いいんじゃないかと思うけどそれはまた別の話か.
https://wiki.haskell.org/Let_vs._Where
このページはテーマはlet vs whereですがlast sectionのProblem with whereで全く同じ話題を扱っていて,結論としてはh2p2の通りですが,whereをletで書き換えるとfib’が引数ごとにredefineされるのが分かるだろと解説してあって,これでも良いかもね.
CAFsだからキャシュしてるんじゃなく,サンクが評価されて値になるものは常に次アクセスされたらちゃんとキャッシュされた値が使われる.
CAFsになってればトップレベルにリフトしてくれて,そのためにキャッシュされた式にアクセスできるからキャッシュを効かせられる.
一方CAFsじゃないやつは毎回新しい式になるので以前の評価済みの式ではないから再評価する必要があって結果キャッシュを効かせられてない.
と言う説明になるんじゃないかな.
whereで定義しているローカル関数fibはfib_memにぶら下がっているのに対してfib_mem_argの方はfib_mem_arg nに対してローカル関数fibがぶらさがっている.
なるほどー これしっくりきました