haskell-jp / questions #53

Map.insert k v <$> buildMap (ks, vs)


これはbuildMapが全部返ってきてからMaybeでパターンマッチする形になるから、確かにスタック積み上がりそう。こういう所はHaskellでも末尾再帰気にしないといけないんですね
ここのfromListはなんかinsertじゃない処理やっているような……?
http://hackage.haskell.org/package/containers-0.6.0.1/docs/src/Data.Map.Internal.html#fromList
foldr なのは,キーリストとかバリューリストにNothingがあったときのショートカット用です.
あ、自分の見てたcontainersのバージョンが古かったようです。
でもソートされていないリストに対しては
やっぱりinsertで実装されてますね
確かに、たまたま先頭が昇順になってた場合だけ違う処理してるのか
末尾再帰については、集積引数を増やして積んでも結局変わらないですね…速度的にも、二回に分けるのが実は正解なのではと思い始める
いや、速度測ってないけど、変わらなくはない(リスト末尾にpushするつもりでO(N^2)と見積もってたけど、insertで直接マップ作るならO(N log N)だ)
@99fabianb has joined the channel
等式論証って何ですか?ググってもわからず。
@ryenana has joined the channel
data Hoge = II
huga x = x

main = do
    i <- huga II
    putStrLn "hello, world"

を実行すると、
    • Couldn't match expected type 'IO a0' with actual type 'Hoge'
    • In a stmt of a 'do' block: i <- huga II
      In the expression:
        do i <- huga II
           putStrLn "hello, world"
      In an equation for 'main':
          main
            = do i <- huga II
                 putStrLn "hello, world"
  |
5 |     i <- huga II 
  |          ^^^^^^^

とエラーが出ます。iはtype ‘IO a0’を期待していますが。
data Hoge = II
huga x = x

main = do
    i <- return II
    putStrLn "hello, world"


として、iはmonado typeを受けていますが。これは、type ‘IO a0’じゃないですが、なぜいいんでしょう?
あと、type ‘IO a0’とはなんでしょう?
IOなのはわかっているんですが。
data Hoge = II
huga x = x

main = do
    i <- return II
    putStrLn "hello, world"

type Hogeはmonadのインスタンスではないのに、returnできるのはなぜでしょう?
ただの値だからでは...?
まずiに期待されている型はIO a0じゃないですね...それはi <-の右側の式に期待されている型です

質問を理解するために質問したいのですが,”モナド型”を受けるとはなんでしょうか...
あとhugaは純粋な関数なのでそこに書く必要はなさそうです.純粋な式はletで束縛するとよいと思います.
そして後者の型はIO ?? の形になってます.return で包んでいるので.
return の型は Monad m => a -> m a であり、引数の型 (ここでは a という型変数で表されています) が Monad のインスタンスかどうかを気にしないからです…というのではどうでしょう?
一つ前の質問とまとめて回答します。

まず、IOモナドの do記法で
i <- e

( eはなんらかの式)と書くと、 eIO a型、 ia型に推論されます。一つ目のプログラムでは
huga IIHoge型であり、`IO a`型とマッチできないので型エラーが発生しています。
一方、二つ目のプログラムでは
return IIMonad m => m Hogeという型に推論されます。これを IO a型とマッチさせると、 m = IO, a = Hogeという解が見つかるのでエラーは発生しません。
data Fool where
  Fool :: ('True ~ 'False) => Fool
theFool  :: Fool
theFool = ???
main :: IO ()
main = case theFool of
  Fool -> pure () 

としてunsafeな関数を使っても良いので`Fool`型の値を得ることってできますか?(mainを実行時エラー起こさずに実行したい)
Fool 型の値は得られない(Emptyである)ことが証明できるので,得られません.
theFool :: Fool
theFool = case refl of {} where
  refl :: (a ~ b) => a :~: b
  refl = Refl
これが得られるようになるレベルのunsafeとは「任意の型の値が作成できる」という度合いのunsafeさであり,型による安全性を投げ捨てることになります.
実行時エラーを起こさないというのを文字通りに取れば theFool = theFool も要件を満たしますがそういうことではないですよね。
theFool = unsafeCoerce $ \_ -> () とか。
引数は使われないので unsafeCoerce () でも動くと思いますが Fool のarityは1になると思うので const () の方が良いかもしれません。
`Fool` 型の値は得られない(Emptyである)ことが証明できるので,得られません.

実際にやりたいのは True ~ Falseほど邪悪なのではなくて、 SomeConstraint :: * -> Constraint をtype familyとして、
data Cert a where
  Cert :: SomeConstraint a => Cert a

みたいなことです。 aがコンパイル時に分かっている場合には SomeConstraint aが簡約できてうまくいくんですが、 aが実行時にしかわからないケースもサポートしたくて、動的に SomeConstraint相当のチェックをしてから Certの値を作りたいという状況です。

引数は使われないので `unsafeCoerce ()` でも動くと思いますが `Fool` のarityは1になると思うので `const ()` の方が良いかもしれません。
やはり unsafeCoerceを使うのが無難そうですね。
@momiimt has joined the channel
これのGADTの節みたいな感じでしょうか https://propella.hatenablog.com/entry/20101218/p1
data Cert a where ... ではなく data Cert where にして、あとはtheFoolにあたる関数theCertの型を theCert :: SomeConstraint a => a -> Cert とするイメージかなと思います
@autotaker さんの回答よくわかりました。
returnの型はわかるんですが、本体はどこにあるのでしょう?
http://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:return
ですね。もう少し細かいことを言うと、GHCが提供する標準ライブラリの中にあり、管理の都合上 GHC.Base モジュールで定義されていて、それをHaskellを書く際暗黙で import される Prelude モジュールが含んでいる形になります
@autotaker なぜm = IOになるのでしょう。これは、monado IOのreturnを使っているからだと思うのですが、なぜmonad IOなのでしょう?(これは、型推論….?
あと、IO a0のa0って何ですか?
なぜ、 i <- e とかくとeはIO aに推論されるのでしょう?mainがIOのため?
そうです,型推論により m = IO となります.Haskell では,
do
  i <- e
  …

は,
e >>= \i -> ...

の略記法になります.ここで, >>=https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:-62--62--61- の型を持つ型クラスのメソッドになります.今回は putStrLn "Hello World!" :: IO () が続くのでここから
1. (>>=) :: m a -> (a -> m b) -> m bm b の部分が IO () と一致すると判定され m = IO / b = () となります
2. m = IO から return II :: m Hoge の部分の mm = IO と推論されます
型エラーにおいて表示されている IO a0a0 は例えば
f :: Maybe a -> ()
f _ = ()

g :: Maybe a -> ()
g _ = ()

h = f (g ())

というようなプログラムにおいて, f の引数における型変数 a のことなのか, g の引数における型変数 a のことなのか分からなくなることを避けるため,番号を暗黙に振り分けるということが内部で行われている結果です.確かに,少し分かりにくいですね.
@mizunashi-mana なるほど。わかりやすい説明ありがとうございます。
あと、質問なのですが、 (>>=) :: m a -> (a -> m b) -> m bma(a -> mb)の二つ引数をとるのに、`e
= \i -> ...` だと e 一つしか引数に取らないように見えますがどうなんでしょう?
あ、もしかして、>>=の右側が第二引数…
はい. Haskell では記号の関数か文字の関数かで演算子かどうかが分かれていて,記号の関数はデフォルトで二項演算子になります
了解です。あざす
別スレッドで、解決しました。返答していただき、ありがとうございました。
@yki0311hiro has joined the channel
doは>>=のシンタックスシュガーのため、do構文で書いたものは、それなしに書きかえれますよね?
以下のは書きかえれますかね?
data Hoge = II deriving (Show)
huga x = x

main = do
    i <- return 3
    let x = huga i
    print $ 1
できます。
https://en.wikibooks.org/wiki/Haskell/do_notation が参考になるかと思います。 <->>= とラムダ式に、 letlet ... in ... に、逐次処理は >> でつなげばよい感じです。
できたけど、in …が余分…
data Hoge = II deriving (Show)
huga x = x

main =
    return 3 >>= (\i -> let x = huga in return 1 ) >> print $ 1
do 構文の変換の覚え方でオススメは

do
  v <- e1
  e2
==>
e1 >>= \v -> e2


do
  e1
  e2
==>
do
  _ <- e1
  e2


do
  let v1 = e1
        ...
        vN = eN
  e
==>
let v1 = e1
      ...
      vN = eN
in e


do
  e
==>
e


do
  line1
  line2
  …
  lineN
==>
do
  line1
  do
    line2
    ...
    lineN


この5つによる変換ですね.
(厳密にはパフォーマンスを考慮してもっと良い変換( >> を使った変換)が行われたり, p <- ep の部分にパターンが使われると fail という関数を使った変換が行われたりするのですが,厳密さを求めないなら大体は上の変換を想定してもらえば大丈夫だと思います)

今回の例では
do
  i <- return 3
  let x = huga i
  print $ 1
==>
do
  i <- return 3
  do
    let x = huga i
    print $ 1
==>
return 3 >>= \i -> do
  let x = huga i
  print $ 1
==>
return 3 >>= \i ->
  let x = huga i
  in print $ 1

みたいな感じです
ありがとうございます
(ちょっと変換の仕方を修正しました.基本的には3行以上のものは do をネストさせて2行に書き直せて,2行の do は >>= で書き直せる感じですね)
main = print 1

でよいのでは:neutral_face:
@tom.lpsd has joined the channel